[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ Continuous (thickenedIndicatorAux δ E)
[PROOFSTEP]
unfold thickenedIndicatorAux
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ Continuous fun x => 1 - infEdist x E / ENNReal.ofReal δ
[PROOFSTEP]
let f := fun x : α => (⟨1, infEdist x E / ENNReal.ofReal δ⟩ : ℝ≥0 × ℝ≥0∞)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)
⊢ Continuous fun x => 1 - infEdist x E / ENNReal.ofReal δ
[PROOFSTEP]
let sub := fun p : ℝ≥0 × ℝ≥0∞ => (p.1 : ℝ≥0∞) - p.2
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.fst - p.snd
⊢ Continuous fun x => 1 - infEdist x E / ENNReal.ofReal δ
[PROOFSTEP]
rw [show (fun x : α => (1 : ℝ≥0∞) - infEdist x E / ENNReal.ofReal δ) = sub ∘ f by rfl]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.fst - p.snd
⊢ (fun x => 1 - infEdist x E / ENNReal.ofReal δ) = sub ∘ f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.fst - p.snd
⊢ Continuous (sub ∘ f)
[PROOFSTEP]
apply (@ENNReal.continuous_nnreal_sub 1).comp
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.fst - p.snd
⊢ Continuous fun x => (f x).snd
[PROOFSTEP]
apply (ENNReal.continuous_div_const (ENNReal.ofReal δ) _).comp continuous_infEdist
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.fst - p.snd
⊢ ENNReal.ofReal δ ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : α → ℝ≥0 × ℝ≥0∞ := fun x => (1, infEdist x E / ENNReal.ofReal δ)
sub : ℝ≥0 × ℝ≥0∞ → ℝ≥0∞ := fun p => ↑p.fst - p.snd
⊢ 0 < δ
[PROOFSTEP]
exact δ_pos
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
⊢ thickenedIndicatorAux δ E x ≤ 1
[PROOFSTEP]
apply @tsub_le_self _ _ _ _ (1 : ℝ≥0∞)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ thickenedIndicatorAux δ (closure E) = thickenedIndicatorAux δ E
[PROOFSTEP]
simp_rw [thickenedIndicatorAux, infEdist_closure]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
⊢ thickenedIndicatorAux δ E x = 1
[PROOFSTEP]
simp [thickenedIndicatorAux, infEdist_zero_of_mem x_in_E, tsub_zero]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_mem : x ∈ closure E
⊢ thickenedIndicatorAux δ E x = 1
[PROOFSTEP]
rw [← thickenedIndicatorAux_closure_eq, thickenedIndicatorAux_one δ (closure E) x_mem]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ¬x ∈ thickening δ E
⊢ thickenedIndicatorAux δ E x = 0
[PROOFSTEP]
rw [thickening, mem_setOf_eq, not_lt] at x_out
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ thickenedIndicatorAux δ E x = 0
[PROOFSTEP]
unfold thickenedIndicatorAux
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ 1 - infEdist x E / ENNReal.ofReal δ = 0
[PROOFSTEP]
apply le_antisymm _ bot_le
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥
[PROOFSTEP]
have key := tsub_le_tsub (@rfl _ (1 : ℝ≥0∞)).le (ENNReal.div_le_div x_out (@rfl _ (ENNReal.ofReal δ : ℝ≥0∞)).le)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
key : 1 - infEdist x E / ENNReal.ofReal δ ≤ 1 - ENNReal.ofReal δ / ENNReal.ofReal δ
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥
[PROOFSTEP]
rw [ENNReal.div_self (ne_of_gt (ENNReal.ofReal_pos.mpr δ_pos)) ofReal_ne_top] at key
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
key : 1 - infEdist x E / ENNReal.ofReal δ ≤ 1 - 1
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥
[PROOFSTEP]
simpa using key
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ (indicator E fun x => 1) ≤ thickenedIndicatorAux δ E
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
⊢ indicator E (fun x => 1) a ≤ thickenedIndicatorAux δ E a
[PROOFSTEP]
by_cases a ∈ E
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
⊢ indicator E (fun x => 1) a ≤ thickenedIndicatorAux δ E a
[PROOFSTEP]
by_cases a ∈ E
[GOAL]
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
h : a ∈ E
⊢ indicator E (fun x => 1) a ≤ thickenedIndicatorAux δ E a
[PROOFSTEP]
simp only [h, indicator_of_mem, thickenedIndicatorAux_one δ E h, le_refl]
[GOAL]
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
h : ¬a ∈ E
⊢ indicator E (fun x => 1) a ≤ thickenedIndicatorAux δ E a
[PROOFSTEP]
simp only [h, indicator_of_not_mem, not_false_iff, zero_le]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
⊢ Tendsto (fun n => thickenedIndicatorAux (δseq n) E) atTop (𝓝 (indicator (closure E) fun x => 1))
[PROOFSTEP]
rw [tendsto_pi_nhds]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
⊢ ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
[PROOFSTEP]
by_cases x_mem_closure : x ∈ closure E
[GOAL]
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
[PROOFSTEP]
simp_rw [thickenedIndicatorAux_one_of_mem_closure _ E x_mem_closure]
[GOAL]
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ Tendsto (fun i => 1) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
[PROOFSTEP]
rw [show (indicator (closure E) fun _ => (1 : ℝ≥0∞)) x = 1 by simp only [x_mem_closure, indicator_of_mem]]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ indicator (closure E) (fun x => 1) x = 1
[PROOFSTEP]
simp only [x_mem_closure, indicator_of_mem]
[GOAL]
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ Tendsto (fun i => 1) atTop (𝓝 1)
[PROOFSTEP]
exact tendsto_const_nhds
[GOAL]
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
[PROOFSTEP]
rw [show (closure E).indicator (fun _ => (1 : ℝ≥0∞)) x = 0 by
    simp only [x_mem_closure, indicator_of_not_mem, not_false_iff]]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
⊢ indicator (closure E) (fun x => 1) x = 0
[PROOFSTEP]
simp only [x_mem_closure, indicator_of_not_mem, not_false_iff]
[GOAL]
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
[PROOFSTEP]
rcases exists_real_pos_lt_infEdist_of_not_mem_closure x_mem_closure with ⟨ε, ⟨ε_pos, ε_lt⟩⟩
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
[PROOFSTEP]
rw [Metric.tendsto_nhds] at δseq_lim
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
[PROOFSTEP]
specialize δseq_lim ε ε_pos
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δseq_lim : ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
[PROOFSTEP]
simp only [dist_zero_right, Real.norm_eq_abs, eventually_atTop, ge_iff_le] at δseq_lim
[GOAL]
case neg.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
δseq_lim : ∃ a, ∀ (b : ℕ), a ≤ b → |δseq b| < ε
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
[PROOFSTEP]
rcases δseq_lim with ⟨N, hN⟩
[GOAL]
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
⊢ Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
[PROOFSTEP]
apply @tendsto_atTop_of_eventually_const _ _ _ _ _ _ _ N
[GOAL]
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
⊢ ∀ (i : ℕ), i ≥ N → thickenedIndicatorAux (δseq i) E x = 0
[PROOFSTEP]
intro n n_large
[GOAL]
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
n : ℕ
n_large : n ≥ N
⊢ thickenedIndicatorAux (δseq n) E x = 0
[PROOFSTEP]
have key : x ∉ thickening ε E := by simpa only [thickening, mem_setOf_eq, not_lt] using ε_lt.le
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
n : ℕ
n_large : n ≥ N
⊢ ¬x ∈ thickening ε E
[PROOFSTEP]
simpa only [thickening, mem_setOf_eq, not_lt] using ε_lt.le
[GOAL]
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
n : ℕ
n_large : n ≥ N
key : ¬x ∈ thickening ε E
⊢ thickenedIndicatorAux (δseq n) E x = 0
[PROOFSTEP]
refine' le_antisymm _ bot_le
[GOAL]
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
n : ℕ
n_large : n ≥ N
key : ¬x ∈ thickening ε E
⊢ thickenedIndicatorAux (δseq n) E x ≤ 0
[PROOFSTEP]
apply (thickenedIndicatorAux_mono (lt_of_abs_lt (hN n n_large)).le E x).trans
[GOAL]
case neg.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEdist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
n : ℕ
n_large : n ≥ N
key : ¬x ∈ thickening ε E
⊢ thickenedIndicatorAux ε E x ≤ 0
[PROOFSTEP]
exact (thickenedIndicatorAux_zero ε_pos E key).le
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ Continuous fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)
[PROOFSTEP]
apply ContinuousOn.comp_continuous continuousOn_toNNReal (continuous_thickenedIndicatorAux δ_pos E)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ ∀ (x : α), thickenedIndicatorAux δ E x ∈ {a | a ≠ ⊤}
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ thickenedIndicatorAux δ E x ∈ {a | a ≠ ⊤}
[PROOFSTEP]
exact (lt_of_le_of_lt (@thickenedIndicatorAux_le_one _ _ δ E x) one_lt_top).ne
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ ∃ C,
    ∀ (x y : α),
      dist (ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x)
          (ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y) ≤
        C
[PROOFSTEP]
use 2
[GOAL]
case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ ∀ (x y : α),
    dist (ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x)
        (ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y) ≤
      2
[PROOFSTEP]
intro x y
[GOAL]
case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ dist (ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x)
      (ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y) ≤
    2
[PROOFSTEP]
rw [NNReal.dist_eq]
[GOAL]
case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ |↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x) -
        ↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y)| ≤
    2
[PROOFSTEP]
apply (abs_sub _ _).trans
[GOAL]
case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ |↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x)| +
      |↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y)| ≤
    2
[PROOFSTEP]
rw [NNReal.abs_eq, NNReal.abs_eq, ← one_add_one_eq_two]
[GOAL]
case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ ↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x) +
      ↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y) ≤
    1 + 1
[PROOFSTEP]
have key := @thickenedIndicatorAux_le_one _ _ δ E
[GOAL]
case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ ↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x) +
      ↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y) ≤
    1 + 1
[PROOFSTEP]
apply add_le_add
[GOAL]
case h.h₁
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ ↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x) ≤ 1
[PROOFSTEP]
norm_cast
[GOAL]
case h.h₁
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) x ≤ 1
[PROOFSTEP]
refine' (toNNReal_le_toNNReal (lt_of_le_of_lt (key _) one_lt_top).ne one_ne_top).mpr (key _)
[GOAL]
case h.h₂
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ ↑(ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y) ≤ 1
[PROOFSTEP]
norm_cast
[GOAL]
case h.h₂
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ ContinuousMap.toFun (ContinuousMap.mk fun x => ENNReal.toNNReal (thickenedIndicatorAux δ E x)) y ≤ 1
[PROOFSTEP]
refine' (toNNReal_le_toNNReal (lt_of_le_of_lt (key _) one_lt_top).ne one_ne_top).mpr (key _)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ ↑(thickenedIndicator δ_pos E) x ≤ 1
[PROOFSTEP]
rw [thickenedIndicator.coeFn_eq_comp]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ (ENNReal.toNNReal ∘ thickenedIndicatorAux δ E) x ≤ 1
[PROOFSTEP]
simpa using (toNNReal_le_toNNReal thickenedIndicatorAux_lt_top.ne one_ne_top).mpr (thickenedIndicatorAux_le_one δ E x)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_mem : x ∈ closure E
⊢ ↑(thickenedIndicator δ_pos E) x = 1
[PROOFSTEP]
rw [thickenedIndicator_apply, thickenedIndicatorAux_one_of_mem_closure δ E x_mem, one_toNNReal]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ¬x ∈ thickening δ E
⊢ ↑(thickenedIndicator δ_pos E) x = 0
[PROOFSTEP]
rw [thickenedIndicator_apply, thickenedIndicatorAux_zero δ_pos E x_out, zero_toNNReal]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ (indicator E fun x => 1) ≤ ↑(thickenedIndicator δ_pos E)
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
⊢ indicator E (fun x => 1) a ≤ ↑(thickenedIndicator δ_pos E) a
[PROOFSTEP]
by_cases a ∈ E
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
⊢ indicator E (fun x => 1) a ≤ ↑(thickenedIndicator δ_pos E) a
[PROOFSTEP]
by_cases a ∈ E
[GOAL]
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : a ∈ E
⊢ indicator E (fun x => 1) a ≤ ↑(thickenedIndicator δ_pos E) a
[PROOFSTEP]
simp only [h, indicator_of_mem, thickenedIndicator_one δ_pos E h, le_refl]
[GOAL]
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : ¬a ∈ E
⊢ indicator E (fun x => 1) a ≤ ↑(thickenedIndicator δ_pos E) a
[PROOFSTEP]
simp only [h, indicator_of_not_mem, not_false_iff, zero_le]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
⊢ ↑(thickenedIndicator δ₁_pos E) ≤ ↑(thickenedIndicator δ₂_pos E)
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ ↑(thickenedIndicator δ₁_pos E) x ≤ ↑(thickenedIndicator δ₂_pos E) x
[PROOFSTEP]
apply (toNNReal_le_toNNReal thickenedIndicatorAux_lt_top.ne thickenedIndicatorAux_lt_top.ne).mpr
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ thickenedIndicatorAux δ₁ E x ≤ thickenedIndicatorAux δ₂ E x
[PROOFSTEP]
apply thickenedIndicatorAux_mono hle
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
⊢ Tendsto (fun n => ↑(thickenedIndicator (_ : 0 < δseq n) E)) atTop (𝓝 (indicator (closure E) fun x => 1))
[PROOFSTEP]
have key := thickenedIndicatorAux_tendsto_indicator_closure δseq_lim E
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : Tendsto (fun n => thickenedIndicatorAux (δseq n) E) atTop (𝓝 (indicator (closure E) fun x => 1))
⊢ Tendsto (fun n => ↑(thickenedIndicator (_ : 0 < δseq n) E)) atTop (𝓝 (indicator (closure E) fun x => 1))
[PROOFSTEP]
rw [tendsto_pi_nhds] at *
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
⊢ ∀ (x : α),
    Tendsto (fun i => ↑(thickenedIndicator (_ : 0 < δseq i) E) x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ Tendsto (fun i => ↑(thickenedIndicator (_ : 0 < δseq i) E) x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
[PROOFSTEP]
rw [show indicator (closure E) (fun _ => (1 : ℝ≥0)) x = (indicator (closure E) (fun _ => (1 : ℝ≥0∞)) x).toNNReal by
    refine' (congr_fun (comp_indicator_const 1 ENNReal.toNNReal zero_toNNReal) x).symm]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ indicator (closure E) (fun x => 1) x = ENNReal.toNNReal (indicator (closure E) (fun x => 1) x)
[PROOFSTEP]
refine' (congr_fun (comp_indicator_const 1 ENNReal.toNNReal zero_toNNReal) x).symm
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ Tendsto (fun i => ↑(thickenedIndicator (_ : 0 < δseq i) E) x) atTop
    (𝓝 (ENNReal.toNNReal (indicator (closure E) (fun x => 1) x)))
[PROOFSTEP]
refine' Tendsto.comp (tendsto_toNNReal _) (key x)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ indicator (closure E) (fun x => 1) x ≠ ⊤
[PROOFSTEP]
by_cases x_mem : x ∈ closure E
[GOAL]
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
x_mem : x ∈ closure E
⊢ indicator (closure E) (fun x => 1) x ≠ ⊤
[PROOFSTEP]
simp [x_mem]
[GOAL]
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
x_mem : ¬x ∈ closure E
⊢ indicator (closure E) (fun x => 1) x ≠ ⊤
[PROOFSTEP]
simp [x_mem]
[GOAL]
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
⊢ ∀ᶠ (δ : ℝ) in 𝓝[Ioi 0] 0, mulIndicator (thickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
by_cases x_mem_closure : x ∈ closure E
[GOAL]
case pos
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[Ioi 0] 0, mulIndicator (thickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin] with δ δ_pos
[GOAL]
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
δ : ℝ
δ_pos : δ ∈ Ioi 0
⊢ mulIndicator (thickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
simp only [closure_subset_thickening δ_pos E x_mem_closure, mulIndicator_of_mem, x_mem_closure]
[GOAL]
case neg
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[Ioi 0] 0, mulIndicator (thickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
have obs := eventually_not_mem_thickening_of_infEdist_pos x_mem_closure
[GOAL]
case neg
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
obs : ∀ᶠ (δ : ℝ) in 𝓝 0, ¬x ∈ thickening δ E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[Ioi 0] 0, mulIndicator (thickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
filter_upwards [mem_nhdsWithin_of_mem_nhds obs, self_mem_nhdsWithin] with δ x_notin_thE _
[GOAL]
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
obs : ∀ᶠ (δ : ℝ) in 𝓝 0, ¬x ∈ thickening δ E
δ : ℝ
x_notin_thE : ¬x ∈ thickening δ E
a✝ : δ ∈ Ioi 0
⊢ mulIndicator (thickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
simp only [x_notin_thE, not_false_eq_true, mulIndicator_of_not_mem, x_mem_closure]
[GOAL]
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, mulIndicator (cthickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
by_cases x_mem_closure : x ∈ closure E
[GOAL]
case pos
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, mulIndicator (cthickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
filter_upwards [univ_mem] with δ _
[GOAL]
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
δ : ℝ
a✝ : δ ∈ univ
⊢ mulIndicator (cthickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
have obs : x ∈ cthickening δ E := closure_subset_cthickening δ E x_mem_closure
[GOAL]
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure E
δ : ℝ
a✝ : δ ∈ univ
obs : x ∈ cthickening δ E
⊢ mulIndicator (cthickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
rw [mulIndicator_of_mem obs f, mulIndicator_of_mem x_mem_closure f]
[GOAL]
case neg
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, mulIndicator (cthickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
filter_upwards [eventually_not_mem_cthickening_of_infEdist_pos x_mem_closure] with δ hδ
[GOAL]
case h
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : ¬x ∈ closure E
δ : ℝ
hδ : ¬x ∈ cthickening δ E
⊢ mulIndicator (cthickening δ E) f x = mulIndicator (closure E) f x
[PROOFSTEP]
simp only [hδ, not_false_eq_true, mulIndicator_of_not_mem, x_mem_closure]
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ Tendsto (fun δ => mulIndicator (thickening δ E) f) (𝓝[Ioi 0] 0) (𝓝 (mulIndicator (closure E) f))
[PROOFSTEP]
rw [tendsto_pi_nhds]
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ ∀ (x : α), Tendsto (fun i => mulIndicator (thickening i E) f x) (𝓝[Ioi 0] 0) (𝓝 (mulIndicator (closure E) f x))
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun i => mulIndicator (thickening i E) f x) (𝓝[Ioi 0] 0) (𝓝 (mulIndicator (closure E) f x))
[PROOFSTEP]
rw [tendsto_congr' (mulIndicator_thickening_eventually_eq_mulIndicator_closure f E x)]
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun x_1 => mulIndicator (closure E) f x) (𝓝[Ioi 0] 0) (𝓝 (mulIndicator (closure E) f x))
[PROOFSTEP]
apply tendsto_const_nhds
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ Tendsto (fun δ => mulIndicator (cthickening δ E) f) (𝓝 0) (𝓝 (mulIndicator (closure E) f))
[PROOFSTEP]
rw [tendsto_pi_nhds]
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ ∀ (x : α), Tendsto (fun i => mulIndicator (cthickening i E) f x) (𝓝 0) (𝓝 (mulIndicator (closure E) f x))
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun i => mulIndicator (cthickening i E) f x) (𝓝 0) (𝓝 (mulIndicator (closure E) f x))
[PROOFSTEP]
rw [tendsto_congr' (mulIndicator_cthickening_eventually_eq_mulIndicator_closure f E x)]
[GOAL]
α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun x_1 => mulIndicator (closure E) f x) (𝓝 0) (𝓝 (mulIndicator (closure E) f x))
[PROOFSTEP]
apply tendsto_const_nhds


[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
⊢ a ∈ s
[PROOFSTEP]
let f := 𝓝[s] a
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
⊢ a ∈ s
[PROOFSTEP]
have : Cauchy f := cauchy_nhds.mono' ha inf_le_left
[GOAL]
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
⊢ a ∈ s
[PROOFSTEP]
rcases h f this inf_le_right with ⟨y, ys, fy⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : SeparatedSpace α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
y : α
ys : y ∈ s
fy : f ≤ 𝓝 y
⊢ a ∈ s
[PROOFSTEP]
rwa [(tendsto_nhds_unique' ha inf_le_left fy : a = y)]


[GOAL]
⊢ AbsoluteValue.uniformSpace AbsoluteValue.abs = PseudoMetricSpace.toUniformSpace
[PROOFSTEP]
ext s
[GOAL]
case a.a
s : Set (ℚ × ℚ)
⊢ s ∈ uniformity ℚ ↔ s ∈ uniformity ℚ
[PROOFSTEP]
rw [(AbsoluteValue.hasBasis_uniformity _).mem_iff, Metric.uniformity_basis_dist_rat.mem_iff]
[GOAL]
case a.a
s : Set (ℚ × ℚ)
⊢ (∃ i, 0 < i ∧ {p | ↑AbsoluteValue.abs (p.snd - p.fst) < i} ⊆ s) ↔ ∃ i, 0 < i ∧ {p | dist p.fst p.snd < ↑i} ⊆ s
[PROOFSTEP]
simp only [Rat.dist_eq, AbsoluteValue.abs_apply, ← Rat.cast_sub, ← Rat.cast_abs, Rat.cast_lt, abs_sub_comm]
[GOAL]
⊢ UniformSpace ℝ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ CompleteSpace ℝ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ SeparatedSpace ℝ
[PROOFSTEP]
infer_instance
[GOAL]
⊢ UniformInducing Rat.cast
[PROOFSTEP]
rw [Rat.uniformSpace_eq]
[GOAL]
⊢ UniformInducing Rat.cast
[PROOFSTEP]
exact Rat.uniformEmbedding_coe_real.toUniformInducing


[GOAL]
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ UniformSpace (m → n → 𝕜)
[PROOFSTEP]
infer_instance
[GOAL]
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ 𝓤 (Matrix m n 𝕜) = ⨅ (i : m) (j : n), Filter.comap (fun a => (Prod.fst a i j, Prod.snd a i j)) (𝓤 𝕜)
[PROOFSTEP]
erw [Pi.uniformity, Pi.uniformity]
[GOAL]
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ ⨅ (i : m),
      Filter.comap (fun a => (Prod.fst a i, Prod.snd a i))
        (⨅ (i : n), Filter.comap (fun a => (Prod.fst a i, Prod.snd a i)) (𝓤 𝕜)) =
    ⨅ (i : m) (j : n), Filter.comap (fun a => (Prod.fst a i j, Prod.snd a i j)) (𝓤 𝕜)
[PROOFSTEP]
simp_rw [Filter.comap_iInf, Filter.comap_comap]
[GOAL]
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ ⨅ (i : m) (i_1 : n),
      Filter.comap ((fun a => (Prod.fst a i_1, Prod.snd a i_1)) ∘ fun a => (Prod.fst a i, Prod.snd a i)) (𝓤 𝕜) =
    ⨅ (i : m) (j : n), Filter.comap (fun a => (Prod.fst a i j, Prod.snd a i j)) (𝓤 𝕜)
[PROOFSTEP]
rfl
[GOAL]
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ UniformContinuous f ↔ ∀ (i : m) (j : n), UniformContinuous fun x => f x i j
[PROOFSTEP]
simp only [UniformContinuous, Matrix.uniformity, Filter.tendsto_iInf, Filter.tendsto_comap_iff]
[GOAL]
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ (∀ (i : m) (i_1 : n),
      Filter.Tendsto ((fun a => (Prod.fst a i i_1, Prod.snd a i i_1)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 β) (𝓤 𝕜)) ↔
    ∀ (i : m) (j : n), Filter.Tendsto (fun x => (f x.fst i j, f x.snd i j)) (𝓤 β) (𝓤 𝕜)
[PROOFSTEP]
apply Iff.intro
[GOAL]
case mp
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ (∀ (i : m) (i_1 : n),
      Filter.Tendsto ((fun a => (Prod.fst a i i_1, Prod.snd a i i_1)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 β) (𝓤 𝕜)) →
    ∀ (i : m) (j : n), Filter.Tendsto (fun x => (f x.fst i j, f x.snd i j)) (𝓤 β) (𝓤 𝕜)
[PROOFSTEP]
intro a
[GOAL]
case mpr
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ (∀ (i : m) (j : n), Filter.Tendsto (fun x => (f x.fst i j, f x.snd i j)) (𝓤 β) (𝓤 𝕜)) →
    ∀ (i : m) (i_1 : n),
      Filter.Tendsto ((fun a => (Prod.fst a i i_1, Prod.snd a i i_1)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 β) (𝓤 𝕜)
[PROOFSTEP]
intro a
[GOAL]
case mp
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
a :
  ∀ (i : m) (i_1 : n),
    Filter.Tendsto ((fun a => (Prod.fst a i i_1, Prod.snd a i i_1)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 β) (𝓤 𝕜)
⊢ ∀ (i : m) (j : n), Filter.Tendsto (fun x => (f x.fst i j, f x.snd i j)) (𝓤 β) (𝓤 𝕜)
[PROOFSTEP]
apply a
[GOAL]
case mpr
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
a : ∀ (i : m) (j : n), Filter.Tendsto (fun x => (f x.fst i j, f x.snd i j)) (𝓤 β) (𝓤 𝕜)
⊢ ∀ (i : m) (i_1 : n),
    Filter.Tendsto ((fun a => (Prod.fst a i i_1, Prod.snd a i i_1)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 β) (𝓤 𝕜)
[PROOFSTEP]
apply a
[GOAL]
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
inst✝ : CompleteSpace 𝕜
⊢ CompleteSpace (m → n → 𝕜)
[PROOFSTEP]
infer_instance
[GOAL]
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
inst✝ : SeparatedSpace 𝕜
⊢ SeparatedSpace (m → n → 𝕜)
[PROOFSTEP]
infer_instance


[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ dist x x = 0
[PROOFSTEP]
refine' induction_on x _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ IsClosed {a | dist a a = 0}
[PROOFSTEP]
refine' isClosed_eq _ continuous_const
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ Continuous fun a => dist a a
[PROOFSTEP]
exact Completion.continuous_dist continuous_id continuous_id
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ ∀ (a : α), dist (↑α a) (↑α a) = 0
[PROOFSTEP]
intro a
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
a : α
⊢ dist (↑α a) (↑α a) = 0
[PROOFSTEP]
rw [Completion.dist_eq, dist_self]
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ dist x y = dist y x
[PROOFSTEP]
refine' induction_on₂ x y _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ IsClosed {x | dist x.fst x.snd = dist x.snd x.fst}
[PROOFSTEP]
exact
  isClosed_eq (Completion.continuous_dist continuous_fst continuous_snd)
    (Completion.continuous_dist continuous_snd continuous_fst)
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ ∀ (a b : α), dist (↑α a) (↑α b) = dist (↑α b) (↑α a)
[PROOFSTEP]
intro a b
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
a b : α
⊢ dist (↑α a) (↑α b) = dist (↑α b) (↑α a)
[PROOFSTEP]
rw [Completion.dist_eq, Completion.dist_eq, dist_comm]
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ dist x z ≤ dist x y + dist y z
[PROOFSTEP]
refine' induction_on₃ x y z _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ IsClosed {x | dist x.fst x.snd.snd ≤ dist x.fst x.snd.fst + dist x.snd.fst x.snd.snd}
[PROOFSTEP]
refine' isClosed_le _ (Continuous.add _ _)
[GOAL]
case refine'_1.refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x => dist x.fst x.snd.snd
[PROOFSTEP]
apply_rules [Completion.continuous_dist, Continuous.fst, Continuous.snd, continuous_id]
[GOAL]
case refine'_1.refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x => dist x.fst x.snd.fst
[PROOFSTEP]
apply_rules [Completion.continuous_dist, Continuous.fst, Continuous.snd, continuous_id]
[GOAL]
case refine'_1.refine'_3
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x => dist x.snd.fst x.snd.snd
[PROOFSTEP]
apply_rules [Completion.continuous_dist, Continuous.fst, Continuous.snd, continuous_id]
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ ∀ (a b c : α), dist (↑α a) (↑α c) ≤ dist (↑α a) (↑α b) + dist (↑α b) (↑α c)
[PROOFSTEP]
intro a b c
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist (↑α a) (↑α c) ≤ dist (↑α a) (↑α b) + dist (↑α b) (↑α c)
[PROOFSTEP]
rw [Completion.dist_eq, Completion.dist_eq, Completion.dist_eq]
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist a c ≤ dist a b + dist b c
[PROOFSTEP]
exact dist_triangle a b c
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ ∃ ε, ε > 0 ∧ ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) → ∃ ε, ε > 0 ∧ ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
intro hs
[GOAL]
case mp
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
⊢ ∃ ε, ε > 0 ∧ ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
rcases mem_uniformity_isClosed hs with ⟨t, ht, ⟨tclosed, ts⟩⟩
[GOAL]
case mp.intro.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
⊢ ∃ ε, ε > 0 ∧ ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
have A : {x : α × α | (↑x.1, ↑x.2) ∈ t} ∈ uniformity α := uniformContinuous_def.1 (uniformContinuous_coe α) t ht
[GOAL]
case mp.intro.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
⊢ ∃ ε, ε > 0 ∧ ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
rcases mem_uniformity_dist.1 A with ⟨ε, εpos, hε⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
⊢ ∃ ε, ε > 0 ∧ ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
refine' ⟨ε, εpos, @fun x y hxy ↦ _⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
⊢ (x, y) ∈ s
[PROOFSTEP]
have : ε ≤ dist x y ∨ (x, y) ∈ t := by
  refine' induction_on₂ x y _ _
  · have :
      {x : Completion α × Completion α | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} =
        {p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t :=
      by ext; simp
    rw [this]
    apply IsClosed.union _ tclosed
    exact isClosed_le continuous_const Completion.uniformContinuous_dist.continuous
  · intro x y
    rw [Completion.dist_eq]
    by_cases h : ε ≤ dist x y
    · exact Or.inl h
    · have Z := hε (not_le.1 h)
      simp only [Set.mem_setOf_eq] at Z
      exact Or.inr Z
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
⊢ ε ≤ dist x y ∨ (x, y) ∈ t
[PROOFSTEP]
refine' induction_on₂ x y _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
⊢ IsClosed {x | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t}
[PROOFSTEP]
have :
  {x : Completion α × Completion α | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} =
    {p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t :=
  by ext; simp
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
⊢ {x | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} = {p | ε ≤ dist p.fst p.snd} ∪ t
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
x✝ : Completion α × Completion α
⊢ x✝ ∈ {x | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} ↔ x✝ ∈ {p | ε ≤ dist p.fst p.snd} ∪ t
[PROOFSTEP]
simp
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
this : {x | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} = {p | ε ≤ dist p.fst p.snd} ∪ t
⊢ IsClosed {x | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t}
[PROOFSTEP]
rw [this]
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
this : {x | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} = {p | ε ≤ dist p.fst p.snd} ∪ t
⊢ IsClosed ({p | ε ≤ dist p.fst p.snd} ∪ t)
[PROOFSTEP]
apply IsClosed.union _ tclosed
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
this : {x | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} = {p | ε ≤ dist p.fst p.snd} ∪ t
⊢ IsClosed {p | ε ≤ dist p.fst p.snd}
[PROOFSTEP]
exact isClosed_le continuous_const Completion.uniformContinuous_dist.continuous
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
⊢ ∀ (a b : α), ε ≤ dist (↑α a) (↑α b) ∨ (↑α a, ↑α b) ∈ t
[PROOFSTEP]
intro x y
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
⊢ ε ≤ dist (↑α x) (↑α y) ∨ (↑α x, ↑α y) ∈ t
[PROOFSTEP]
rw [Completion.dist_eq]
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
⊢ ε ≤ dist x y ∨ (↑α x, ↑α y) ∈ t
[PROOFSTEP]
by_cases h : ε ≤ dist x y
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
h : ε ≤ dist x y
⊢ ε ≤ dist x y ∨ (↑α x, ↑α y) ∈ t
[PROOFSTEP]
exact Or.inl h
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
h : ¬ε ≤ dist x y
⊢ ε ≤ dist x y ∨ (↑α x, ↑α y) ∈ t
[PROOFSTEP]
have Z := hε (not_le.1 h)
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
h : ¬ε ≤ dist x y
Z : (x, y) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
⊢ ε ≤ dist x y ∨ (↑α x, ↑α y) ∈ t
[PROOFSTEP]
simp only [Set.mem_setOf_eq] at Z
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
h : ¬ε ≤ dist x y
Z : (↑α x, ↑α y) ∈ t
⊢ ε ≤ dist x y ∨ (↑α x, ↑α y) ∈ t
[PROOFSTEP]
exact Or.inr Z
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
this : ε ≤ dist x y ∨ (x, y) ∈ t
⊢ (x, y) ∈ s
[PROOFSTEP]
simp only [not_le.mpr hxy, false_or_iff, not_le] at this
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑α x.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
this : (x, y) ∈ t
⊢ (x, y) ∈ s
[PROOFSTEP]
exact ts this
[GOAL]
case mpr
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ (∃ ε, ε > 0 ∧ ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s) → s ∈ 𝓤 (Completion α)
[PROOFSTEP]
rintro ⟨ε, εpos, hε⟩
[GOAL]
case mpr.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
⊢ s ∈ 𝓤 (Completion α)
[PROOFSTEP]
let r : Set (ℝ × ℝ) := {p | dist p.1 p.2 < ε}
[GOAL]
case mpr.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
⊢ s ∈ 𝓤 (Completion α)
[PROOFSTEP]
have : r ∈ uniformity ℝ := Metric.dist_mem_uniformity εpos
[GOAL]
case mpr.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
⊢ s ∈ 𝓤 (Completion α)
[PROOFSTEP]
have T := uniformContinuous_def.1 (@Completion.uniformContinuous_dist α _) r this
[GOAL]
case mpr.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
T : {x | (dist x.fst.fst x.fst.snd, dist x.snd.fst x.snd.snd) ∈ r} ∈ 𝓤 (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α)
[PROOFSTEP]
simp only [uniformity_prod_eq_prod, mem_prod_iff, exists_prop, Filter.mem_map, Set.mem_setOf_eq] at T
[GOAL]
case mpr.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
T :
  ∃ t₁,
    t₁ ∈ 𝓤 (Completion α) ∧
      ∃ t₂,
        t₂ ∈ 𝓤 (Completion α) ∧
          t₁ ×ˢ t₂ ⊆
            (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
              {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
⊢ s ∈ 𝓤 (Completion α)
[PROOFSTEP]
rcases T with ⟨t1, ht1, t2, ht2, ht⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
⊢ s ∈ 𝓤 (Completion α)
[PROOFSTEP]
refine' mem_of_superset ht1 _
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
⊢ t1 ⊆ s
[PROOFSTEP]
have A : ∀ a b : Completion α, (a, b) ∈ t1 → dist a b < ε :=
  by
  intro a b hab
  have : ((a, b), (a, a)) ∈ t1 ×ˢ t2 := ⟨hab, refl_mem_uniformity ht2⟩
  have I := ht this
  simp [Completion.dist_self, Real.dist_eq, Completion.dist_comm] at I
  exact lt_of_le_of_lt (le_abs_self _) I
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
⊢ ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε
[PROOFSTEP]
intro a b hab
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
a b : Completion α
hab : (a, b) ∈ t1
⊢ dist a b < ε
[PROOFSTEP]
have : ((a, b), (a, a)) ∈ t1 ×ˢ t2 := ⟨hab, refl_mem_uniformity ht2⟩
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this✝ : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
a b : Completion α
hab : (a, b) ∈ t1
this : ((a, b), a, a) ∈ t1 ×ˢ t2
⊢ dist a b < ε
[PROOFSTEP]
have I := ht this
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this✝ : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
a b : Completion α
hab : (a, b) ∈ t1
this : ((a, b), a, a) ∈ t1 ×ˢ t2
I :
  ((a, b), a, a) ∈
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
⊢ dist a b < ε
[PROOFSTEP]
simp [Completion.dist_self, Real.dist_eq, Completion.dist_comm] at I
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this✝ : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
a b : Completion α
hab : (a, b) ∈ t1
this : ((a, b), a, a) ∈ t1 ×ˢ t2
I : |dist a b| < ε
⊢ dist a b < ε
[PROOFSTEP]
exact lt_of_le_of_lt (le_abs_self _) I
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
A : ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε
⊢ t1 ⊆ s
[PROOFSTEP]
show t1 ⊆ s
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
A : ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε
⊢ t1 ⊆ s
[PROOFSTEP]
rintro ⟨a, b⟩ hp
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.mk
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
A : ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε
a b : Completion α
hp : (a, b) ∈ t1
⊢ (a, b) ∈ s
[PROOFSTEP]
have : dist a b < ε := A a b hp
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.mk
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this✝ : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
A : ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε
a b : Completion α
hp : (a, b) ∈ t1
this : dist a b < ε
⊢ (a, b) ∈ s
[PROOFSTEP]
exact hε this
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
⊢ x = y
[PROOFSTEP]
have : SeparatedSpace (Completion α) := by infer_instance
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
⊢ SeparatedSpace (Completion α)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
⊢ x = y
[PROOFSTEP]
refine' separated_def.1 this x y fun s hs ↦ _
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
⊢ (x, y) ∈ s
[PROOFSTEP]
rcases(Completion.mem_uniformity_dist s).1 hs with ⟨ε, εpos, hε⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
⊢ (x, y) ∈ s
[PROOFSTEP]
rw [← h] at εpos
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
ε : ℝ
εpos : ε > dist x y
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
⊢ (x, y) ∈ s
[PROOFSTEP]
exact hε εpos
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
⊢ 𝓤 (Completion α) = ⨅ (ε : { ε // 0 < ε }), 𝓟 {p | dist p.fst p.snd < ↑ε}
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ s ∈ ⨅ (ε : { ε // 0 < ε }), 𝓟 {p | dist p.fst p.snd < ↑ε}
[PROOFSTEP]
rw [mem_iInf_of_directed]
[GOAL]
case a
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ ∃ i, s ∈ 𝓟 {p | dist p.fst p.snd < ↑i}
[PROOFSTEP]
simp [Completion.mem_uniformity_dist, subset_def]
[GOAL]
case a.h
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ Directed (fun x x_1 => x ≥ x_1) fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}
[PROOFSTEP]
rintro ⟨r, hr⟩ ⟨p, hp⟩
[GOAL]
case a.h.mk.mk
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
r : ℝ
hr : 0 < r
p : ℝ
hp : 0 < p
⊢ ∃ z,
    (fun x x_1 => x ≥ x_1) ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) { val := r, property := hr })
        ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) z) ∧
      (fun x x_1 => x ≥ x_1) ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) { val := p, property := hp })
        ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) z)
[PROOFSTEP]
use⟨min r p, lt_min hr hp⟩
[GOAL]
case h
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
r : ℝ
hr : 0 < r
p : ℝ
hp : 0 < p
⊢ (fun x x_1 => x ≥ x_1) ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) { val := r, property := hr })
      ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) { val := min r p, property := (_ : 0 < min r p) }) ∧
    (fun x x_1 => x ≥ x_1) ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) { val := p, property := hp })
      ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) { val := min r p, property := (_ : 0 < min r p) })
[PROOFSTEP]
simp (config := { contextual := true }) [lt_min_iff]
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
⊢ 𝓤 (Completion α) = ⨅ (ε : ℝ) (_ : ε > 0), 𝓟 {p | dist p.fst p.snd < ε}
[PROOFSTEP]
simpa [iInf_subtype] using @Completion.uniformity_dist' α _
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
⊢ UniformSpace (Completion α)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ Continuous fun x => dist (Completion.extension f x.fst) (Completion.extension f x.snd)
[PROOFSTEP]
continuity
[GOAL]
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ Continuous fun x => ↑K * dist x.fst x.snd
[PROOFSTEP]
continuity
[GOAL]
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ ∀ (a b : α), dist (Completion.extension f (↑α a)) (Completion.extension f (↑α b)) ≤ ↑K * dist (↑α a) (↑α b)
[PROOFSTEP]
simpa only [extension_coe h.uniformContinuous, Completion.dist_eq] using h.dist_le_mul
[GOAL]
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
h : Isometry f
x y : Completion α
⊢ Continuous fun x => dist (Completion.extension f x.fst) (Completion.extension f x.snd)
[PROOFSTEP]
continuity
[GOAL]
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
h : Isometry f
x y : Completion α
⊢ Continuous fun x => dist x.fst x.snd
[PROOFSTEP]
continuity
[GOAL]
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
h : Isometry f
x y : Completion α
x✝¹ x✝ : α
⊢ dist (Completion.extension f (↑α x✝¹)) (Completion.extension f (↑α x✝)) = dist (↑α x✝¹) (↑α x✝)
[PROOFSTEP]
simp only [extension_coe h.uniformContinuous, Completion.dist_eq, h.dist_eq]


[GOAL]
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring A
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Algebra R A
inst✝⁵ : Module R M₁
inst✝⁴ : Module A M₁
inst✝³ : SMulCommClass R A M₁
inst✝² : SMulCommClass A R M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ IsSymm (BilinForm.tmul B₁ B₂)
[PROOFSTEP]
rw [isSymm_iff_flip R]
[GOAL]
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring A
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Algebra R A
inst✝⁵ : Module R M₁
inst✝⁴ : Module A M₁
inst✝³ : SMulCommClass R A M₁
inst✝² : SMulCommClass A R M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ ↑(flipHom R) (BilinForm.tmul B₁ B₂) = BilinForm.tmul B₁ B₂
[PROOFSTEP]
apply toLin.injective
[GOAL]
case a
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring A
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Algebra R A
inst✝⁵ : Module R M₁
inst✝⁴ : Module A M₁
inst✝³ : SMulCommClass R A M₁
inst✝² : SMulCommClass A R M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
⊢ ↑toLin (↑(flipHom R) (BilinForm.tmul B₁ B₂)) = ↑toLin (BilinForm.tmul B₁ B₂)
[PROOFSTEP]
ext x₁ x₂ y₁ y₂
[GOAL]
case a.a.h.h.a.h.h
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring A
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Algebra R A
inst✝⁵ : Module R M₁
inst✝⁴ : Module A M₁
inst✝³ : SMulCommClass R A M₁
inst✝² : SMulCommClass A R M₁
inst✝¹ : IsScalarTower R A M₁
inst✝ : Module R M₂
B₁ : BilinForm A M₁
B₂ : BilinForm R M₂
hB₁ : IsSymm B₁
hB₂ : IsSymm B₂
x₁ : M₁
x₂ : M₂
y₁ : M₁
y₂ : M₂
⊢ ↑(↑(AlgebraTensorModule.curry (↑(↑(AlgebraTensorModule.curry (↑toLin (↑(flipHom R) (BilinForm.tmul B₁ B₂)))) x₁) x₂))
          y₁)
      y₂ =
    ↑(↑(AlgebraTensorModule.curry (↑(↑(AlgebraTensorModule.curry (↑toLin (BilinForm.tmul B₁ B₂))) x₁) x₂)) y₁) y₂
[PROOFSTEP]
exact (congr_arg₂ (HSMul.hSMul) (hB₂ x₂ y₂) (hB₁ x₁ y₁)).symm
[GOAL]
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module.Free R M₁
inst✝³ : Module.Finite R M₁
inst✝² : Module.Free R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Nontrivial R
⊢ ↑(tensorDistribEquiv R) = tensorDistrib R R
[PROOFSTEP]
ext B₁ B₂ : 3
[GOAL]
case a.h.h
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module.Free R M₁
inst✝³ : Module.Finite R M₁
inst✝² : Module.Free R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Nontrivial R
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
⊢ ↑(↑(AlgebraTensorModule.curry ↑(tensorDistribEquiv R)) B₁) B₂ =
    ↑(↑(AlgebraTensorModule.curry (tensorDistrib R R)) B₁) B₂
[PROOFSTEP]
apply toLin.injective
[GOAL]
case a.h.h.a
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module.Free R M₁
inst✝³ : Module.Finite R M₁
inst✝² : Module.Free R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Nontrivial R
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
⊢ ↑toLin (↑(↑(AlgebraTensorModule.curry ↑(tensorDistribEquiv R)) B₁) B₂) =
    ↑toLin (↑(↑(AlgebraTensorModule.curry (tensorDistrib R R)) B₁) B₂)
[PROOFSTEP]
ext
[GOAL]
case a.h.h.a.a.h.h.a.h.h
ι : Type uι
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module.Free R M₁
inst✝³ : Module.Finite R M₁
inst✝² : Module.Free R M₂
inst✝¹ : Module.Finite R M₂
inst✝ : Nontrivial R
B₁ : BilinForm R M₁
B₂ : BilinForm R M₂
x✝³ : M₁
x✝² : M₂
x✝¹ : M₁
x✝ : M₂
⊢ ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry (↑toLin (↑(↑(AlgebraTensorModule.curry ↑(tensorDistribEquiv R)) B₁) B₂)))
                    x✝³)
                x✝²))
          x✝¹)
      x✝ =
    ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry (↑toLin (↑(↑(AlgebraTensorModule.curry (tensorDistrib R R)) B₁) B₂))) x✝³)
                x✝²))
          x✝¹)
      x✝
[PROOFSTEP]
exact mul_comm _ _