[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : LinearOrder β
U : Filter (α × α)
z : β
D : α → α → β
H : ∀ (s : Set (α × α)), s ∈ U ↔ ∃ ε, ε > z ∧ ∀ {a b : α}, D a b < ε → (a, b) ∈ s
s : Set (α × α)
⊢ s ∈ U ↔ ∃ i, i > z ∧ {p | D p.fst p.snd < i} ⊆ s
[PROOFSTEP]
simp only [H, subset_def, Prod.forall, mem_setOf]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist z x + edist z y
[PROOFSTEP]
rw [edist_comm z]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist z y
[PROOFSTEP]
apply edist_triangle
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist y z
[PROOFSTEP]
rw [edist_comm y]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist z y
[PROOFSTEP]
apply edist_triangle
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z = edist y z
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist y z
[PROOFSTEP]
rw [← zero_add (edist y z), ← h]
[GOAL]
case a
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist x y + edist y z
[PROOFSTEP]
apply edist_triangle
[GOAL]
case a
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist y z ≤ edist x z
[PROOFSTEP]
rw [edist_comm] at h
[GOAL]
case a
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
⊢ edist y z ≤ edist x z
[PROOFSTEP]
rw [← zero_add (edist x z), ← h]
[GOAL]
case a
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
⊢ edist y z ≤ edist y x + edist x z
[PROOFSTEP]
apply edist_triangle
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist z x = edist z y
[PROOFSTEP]
rw [edist_comm z x, edist_comm z y]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z = edist y z
[PROOFSTEP]
apply edist_congr_right h
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
h : m ≤ n
⊢ edist (f m) (f n) ≤ ∑ i in Finset.Ico m n, edist (f i) (f (i + 1))
[PROOFSTEP]
induction n, h using Nat.le_induction
[GOAL]
case base
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
⊢ edist (f m) (f m) ≤ ∑ i in Finset.Ico m m, edist (f i) (f (i + 1))
case succ
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n n✝ : ℕ
hn✝ : m ≤ n✝
a✝ : edist (f m) (f n✝) ≤ ∑ i in Finset.Ico m n✝, edist (f i) (f (i + 1))
⊢ edist (f m) (f (n✝ + 1)) ≤ ∑ i in Finset.Ico m (n✝ + 1), edist (f i) (f (i + 1))
[PROOFSTEP]
case base => rw [Finset.Ico_self, Finset.sum_empty, edist_self]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
⊢ edist (f m) (f m) ≤ ∑ i in Finset.Ico m m, edist (f i) (f (i + 1))
[PROOFSTEP]
case base => rw [Finset.Ico_self, Finset.sum_empty, edist_self]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
⊢ edist (f m) (f m) ≤ ∑ i in Finset.Ico m m, edist (f i) (f (i + 1))
[PROOFSTEP]
rw [Finset.Ico_self, Finset.sum_empty, edist_self]
[GOAL]
case succ
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n n✝ : ℕ
hn✝ : m ≤ n✝
a✝ : edist (f m) (f n✝) ≤ ∑ i in Finset.Ico m n✝, edist (f i) (f (i + 1))
⊢ edist (f m) (f (n✝ + 1)) ≤ ∑ i in Finset.Ico m (n✝ + 1), edist (f i) (f (i + 1))
[PROOFSTEP]
case succ n hle ihn =>
  calc
    edist (f m) (f (n + 1)) ≤ edist (f m) (f n) + edist (f n) (f (n + 1)) := edist_triangle _ _ _
    _ ≤ (∑ i in Finset.Ico m n, _) + _ := (add_le_add ihn le_rfl)
    _ = ∑ i in Finset.Ico m (n + 1), _ := by {rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm];
      simp
    }
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i in Finset.Ico m n, edist (f i) (f (i + 1))
⊢ edist (f m) (f (n + 1)) ≤ ∑ i in Finset.Ico m (n + 1), edist (f i) (f (i + 1))
[PROOFSTEP]
case succ n hle ihn =>
  calc
    edist (f m) (f (n + 1)) ≤ edist (f m) (f n) + edist (f n) (f (n + 1)) := edist_triangle _ _ _
    _ ≤ (∑ i in Finset.Ico m n, _) + _ := (add_le_add ihn le_rfl)
    _ = ∑ i in Finset.Ico m (n + 1), _ := by {rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm];
      simp
    }
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i in Finset.Ico m n, edist (f i) (f (i + 1))
⊢ edist (f m) (f (n + 1)) ≤ ∑ i in Finset.Ico m (n + 1), edist (f i) (f (i + 1))
[PROOFSTEP]
calc
  edist (f m) (f (n + 1)) ≤ edist (f m) (f n) + edist (f n) (f (n + 1)) := edist_triangle _ _ _
  _ ≤ (∑ i in Finset.Ico m n, _) + _ := (add_le_add ihn le_rfl)
  _ = ∑ i in Finset.Ico m (n + 1), _ := by {rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm]; simp
  }
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i in Finset.Ico m n, edist (f i) (f (i + 1))
⊢ ∑ i in Finset.Ico m n, edist (f i) (f (i + 1)) + edist (f n) (f (n + 1)) =
    ∑ i in Finset.Ico m (n + 1), edist (f i) (f (i + 1))
[PROOFSTEP]
{rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm]; simp
}
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i in Finset.Ico m n, edist (f i) (f (i + 1))
⊢ ∑ i in Finset.Ico m n, edist (f i) (f (i + 1)) + edist (f n) (f (n + 1)) =
    ∑ i in Finset.Ico m (n + 1), edist (f i) (f (i + 1))
[PROOFSTEP]
rw [Nat.Ico_succ_right_eq_insert_Ico hle, Finset.sum_insert, add_comm]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i in Finset.Ico m n, edist (f i) (f (i + 1))
⊢ ¬n ∈ Finset.Ico m n
[PROOFSTEP]
simp
[GOAL]
α : Type u
β✝ : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
⊢ HasBasis (𝓤 α) p fun x => {p | edist p.fst p.snd < f x}
[PROOFSTEP]
refine' ⟨fun s => uniformity_basis_edist.mem_iff.trans _⟩
[GOAL]
α : Type u
β✝ : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.fst p.snd < i} ⊆ s) ↔ ∃ i, p i ∧ {p | edist p.fst p.snd < f i} ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β✝ : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.fst p.snd < i} ⊆ s) → ∃ i, p i ∧ {p | edist p.fst p.snd < f i} ⊆ s
[PROOFSTEP]
rintro ⟨ε, ε₀, hε⟩
[GOAL]
case mp.intro.intro
α : Type u
β✝ : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.fst p.snd < ε} ⊆ s
⊢ ∃ i, p i ∧ {p | edist p.fst p.snd < f i} ⊆ s
[PROOFSTEP]
rcases hf ε ε₀ with ⟨i, hi, H⟩
[GOAL]
case mp.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.fst p.snd < ε} ⊆ s
i : β
hi : p i
H : f i ≤ ε
⊢ ∃ i, p i ∧ {p | edist p.fst p.snd < f i} ⊆ s
[PROOFSTEP]
exact ⟨i, hi, fun x hx => hε <| lt_of_lt_of_le hx.out H⟩
[GOAL]
case mpr
α : Type u
β✝ : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | edist p.fst p.snd < f i} ⊆ s) → ∃ i, 0 < i ∧ {p | edist p.fst p.snd < i} ⊆ s
[PROOFSTEP]
exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, H⟩
[GOAL]
α : Type u
β✝ : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
⊢ HasBasis (𝓤 α) p fun x => {p | edist p.fst p.snd ≤ f x}
[PROOFSTEP]
refine' ⟨fun s => uniformity_basis_edist.mem_iff.trans _⟩
[GOAL]
α : Type u
β✝ : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.fst p.snd < i} ⊆ s) ↔ ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β✝ : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.fst p.snd < i} ⊆ s) → ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s
[PROOFSTEP]
rintro ⟨ε, ε₀, hε⟩
[GOAL]
case mp.intro.intro
α : Type u
β✝ : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.fst p.snd < ε} ⊆ s
⊢ ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s
[PROOFSTEP]
rcases exists_between ε₀ with ⟨ε', hε'⟩
[GOAL]
case mp.intro.intro.intro
α : Type u
β✝ : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.fst p.snd < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
⊢ ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s
[PROOFSTEP]
rcases hf ε' hε'.1 with ⟨i, hi, H⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u
β✝ : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p | edist p.fst p.snd < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
i : β
hi : p i
H : f i ≤ ε'
⊢ ∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s
[PROOFSTEP]
exact ⟨i, hi, fun x hx => hε <| lt_of_le_of_lt (le_trans hx.out H) hε'.2⟩
[GOAL]
case mpr
α : Type u
β✝ : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, p i ∧ {p | edist p.fst p.snd ≤ f i} ⊆ s) → ∃ i, 0 < i ∧ {p | edist p.fst p.snd < i} ⊆ s
[PROOFSTEP]
exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x hx => H (le_of_lt hx.out)⟩
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ≥0∞), 0 < i' → ∃ i, 0 < i ∧ Prod.map f f ⁻¹' {p | edist p.fst p.snd < i} ⊆ {p | edist p.fst p.snd < i'}) ↔
    ∀ (δ : ℝ≥0∞), δ > 0 → ∃ ε, ε > 0 ∧ ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
[PROOFSTEP]
simp only [subset_def, Prod.forall]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ≥0∞),
      0 < i' →
        ∃ i,
          0 < i ∧
            ∀ (a b : α),
              (a, b) ∈ Prod.map f f ⁻¹' {p | edist p.fst p.snd < i} → (a, b) ∈ {p | edist p.fst p.snd < i'}) ↔
    ∀ (δ : ℝ≥0∞), δ > 0 → ∃ ε, ε > 0 ∧ ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f ≠ ⊥ ∧ ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, t ∈ f ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → edist x y < ε
[PROOFSTEP]
rw [← neBot_iff]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ NeBot f ∧ ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, t ∈ f ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → edist x y < ε
[PROOFSTEP]
exact uniformity_basis_edist.cauchy_iff
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoLocallyUniformlyOn F f p s ↔
    ∀ (ε : ℝ≥0∞),
      ε > 0 → ∀ (x : β), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → edist (f y) (F n y) < ε
[PROOFSTEP]
refine' ⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu x hx => _⟩
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H :
  ∀ (ε : ℝ≥0∞), ε > 0 → ∀ (x : β), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → (f y, F n y) ∈ u
[PROOFSTEP]
rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H :
  ∀ (ε : ℝ≥0∞), ε > 0 → ∀ (x : β), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → (f y, F n y) ∈ u
[PROOFSTEP]
rcases H ε εpos x hx with ⟨t, ht, Ht⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H :
  ∀ (ε : ℝ≥0∞), ε > 0 → ∀ (x : β), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
t : Set β
ht : t ∈ 𝓝[s] x
Ht : ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → edist (f y) (F n y) < ε
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → (f y, F n y) ∈ u
[PROOFSTEP]
exact ⟨t, ht, Ht.mono fun n hs x hx => hε (hs x hx)⟩
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoUniformlyOn F f p s ↔ ∀ (ε : ℝ≥0∞), ε > 0 → ∀ᶠ (n : ι) in p, ∀ (x : β), x ∈ s → edist (f x) (F n x) < ε
[PROOFSTEP]
refine' ⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu => _⟩
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ (ε : ℝ≥0∞), ε > 0 → ∀ᶠ (n : ι) in p, ∀ (x : β), x ∈ s → edist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
⊢ ∀ᶠ (n : ι) in p, ∀ (x : β), x ∈ s → (f x, F n x) ∈ u
[PROOFSTEP]
rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ (ε : ℝ≥0∞), ε > 0 → ∀ᶠ (n : ι) in p, ∀ (x : β), x ∈ s → edist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ (x : β), x ∈ s → (f x, F n x) ∈ u
[PROOFSTEP]
exact (H ε εpos).mono fun n hs x hx => hε (hs x hx)
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoLocallyUniformly F f p ↔
    ∀ (ε : ℝ≥0∞), ε > 0 → ∀ (x : β), ∃ t, t ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → edist (f y) (F n y) < ε
[PROOFSTEP]
simp only [← tendstoLocallyUniformlyOn_univ, tendstoLocallyUniformlyOn_iff, mem_univ, forall_const, exists_prop,
  nhdsWithin_univ]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoUniformly F f p ↔ ∀ (ε : ℝ≥0∞), ε > 0 → ∀ᶠ (n : ι) in p, ∀ (x : β), edist (f x) (F n x) < ε
[PROOFSTEP]
simp only [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff, mem_univ, forall_const]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α × β
⊢ edist x x = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α × β
⊢ edist x y = edist y x
[PROOFSTEP]
simp [edist_comm]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
⊢ comap (fun p => (p.fst.fst, p.snd.fst)) (𝓤 α) ⊓ comap (fun p => (p.fst.snd, p.snd.snd)) (𝓤 β) =
    ⨅ (ε : ℝ≥0∞) (_ : ε > 0), 𝓟 {p | edist p.fst p.snd < ε}
[PROOFSTEP]
simp [PseudoEMetricSpace.uniformity_edist, ← iInf_inf_eq, setOf_and]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → EDist (π b)
f g : (b : β) → π b
d : ℝ≥0∞
⊢ (∀ (b : β), b ∈ Finset.univ → edist (f b) (g b) ≤ d) ↔ ∀ (b : β), edist (f b) (g b) ≤ d
[PROOFSTEP]
simp only [Finset.mem_univ, forall_const]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
f : (b : β) → π b
⊢ ∀ (b : β), b ∈ Finset.univ → edist (f b) (f b) ≤ ⊥
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
f g : (b : β) → π b
⊢ edist f g = edist g f
[PROOFSTEP]
simp [edist_pi_def, edist_comm]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
⊢ 𝓤 ((b : β) → π b) = ⨅ (ε : ℝ≥0∞) (_ : ε > 0), 𝓟 {p | edist p.fst p.snd < ε}
[PROOFSTEP]
simp only [Pi.uniformity, PseudoEMetricSpace.uniformity_edist, comap_iInf, gt_iff_lt, preimage_setOf_eq,
  comap_principal, edist_pi_def]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
⊢ ⨅ (i : β) (i_1 : ℝ≥0∞) (_ : 0 < i_1), 𝓟 {a | edist (Prod.fst a i) (Prod.snd a i) < i_1} =
    ⨅ (ε : ℝ≥0∞) (_ : 0 < ε), 𝓟 {p | (sup Finset.univ fun b => edist (Prod.fst p b) (Prod.snd p b)) < ε}
[PROOFSTEP]
rw [iInf_comm]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
⊢ ⨅ (j : ℝ≥0∞) (i : β) (_ : 0 < j), 𝓟 {a | edist (Prod.fst a i) (Prod.snd a i) < j} =
    ⨅ (ε : ℝ≥0∞) (_ : 0 < ε), 𝓟 {p | (sup Finset.univ fun b => edist (Prod.fst p b) (Prod.snd p b)) < ε}
[PROOFSTEP]
congr
[GOAL]
case e_s
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
⊢ (fun j => ⨅ (i : β) (_ : 0 < j), 𝓟 {a | edist (Prod.fst a i) (Prod.snd a i) < j}) = fun ε =>
    ⨅ (_ : 0 < ε), 𝓟 {p | (sup Finset.univ fun b => edist (Prod.fst p b) (Prod.snd p b)) < ε}
[PROOFSTEP]
funext ε
[GOAL]
case e_s.h
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
ε : ℝ≥0∞
⊢ ⨅ (i : β) (_ : 0 < ε), 𝓟 {a | edist (Prod.fst a i) (Prod.snd a i) < ε} =
    ⨅ (_ : 0 < ε), 𝓟 {p | (sup Finset.univ fun b => edist (Prod.fst p b) (Prod.snd p b)) < ε}
[PROOFSTEP]
rw [iInf_comm]
[GOAL]
case e_s.h
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
ε : ℝ≥0∞
⊢ ⨅ (_ : 0 < ε) (i : β), 𝓟 {a | edist (Prod.fst a i) (Prod.snd a i) < ε} =
    ⨅ (_ : 0 < ε), 𝓟 {p | (sup Finset.univ fun b => edist (Prod.fst p b) (Prod.snd p b)) < ε}
[PROOFSTEP]
congr
[GOAL]
case e_s.h.e_s
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
ε : ℝ≥0∞
⊢ (fun j => ⨅ (i : β), 𝓟 {a | edist (Prod.fst a i) (Prod.snd a i) < ε}) = fun x =>
    𝓟 {p | (sup Finset.univ fun b => edist (Prod.fst p b) (Prod.snd p b)) < ε}
[PROOFSTEP]
funext εpos
[GOAL]
case e_s.h.e_s.h
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ⨅ (i : β), 𝓟 {a | edist (Prod.fst a i) (Prod.snd a i) < ε} =
    𝓟 {p | (sup Finset.univ fun b => edist (Prod.fst p b) (Prod.snd p b)) < ε}
[PROOFSTEP]
simp [setOf_forall, εpos]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ y ∈ ball x ε ↔ edist x y < ε
[PROOFSTEP]
rw [edist_comm, mem_ball]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ y ∈ closedBall x ε ↔ edist x y ≤ ε
[PROOFSTEP]
rw [edist_comm, mem_closedBall]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
h : 0 < ε
⊢ x ∈ ball x ε
[PROOFSTEP]
rwa [mem_ball, edist_self]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ x ∈ closedBall x ε
[PROOFSTEP]
rw [mem_closedBall, edist_self]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ 0 ≤ ε
[PROOFSTEP]
apply zero_le
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ x ∈ ball y ε ↔ y ∈ ball x ε
[PROOFSTEP]
rw [mem_ball', mem_ball]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ x ∈ closedBall y ε ↔ y ∈ closedBall x ε
[PROOFSTEP]
rw [mem_closedBall', mem_closedBall]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
h : y ∈ ball x ε
⊢ ∃ ε', ε' > 0 ∧ ball y ε' ⊆ ball x ε
[PROOFSTEP]
have : 0 < ε - edist y x := by simpa using h
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
h : y ∈ ball x ε
⊢ 0 < ε - edist y x
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
h : y ∈ ball x ε
this : 0 < ε - edist y x
⊢ ∃ ε', ε' > 0 ∧ ball y ε' ⊆ ball x ε
[PROOFSTEP]
refine' ⟨ε - edist y x, this, ball_subset _ (ne_top_of_lt h)⟩
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
h : y ∈ ball x ε
this : 0 < ε - edist y x
⊢ edist y x + (ε - edist y x) ≤ ε
[PROOFSTEP]
exact (add_tsub_cancel_of_le (mem_ball.mp h).le).le
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x : α
⊢ edist x x < ⊤
[PROOFSTEP]
rw [edist_self]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x : α
⊢ 0 < ⊤
[PROOFSTEP]
exact ENNReal.coe_lt_top
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x✝ y✝ : α
h : edist x✝ y✝ < ⊤
⊢ edist y✝ x✝ < ⊤
[PROOFSTEP]
rwa [edist_comm]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ ball x 0 = ∅
[PROOFSTEP]
rw [EMetric.ball_eq_empty_iff]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x✝² y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s t✝ : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ x ∈ ball a δ ∩ s → f x ∈ ball b ε ∩ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x✝² y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s t✝ : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
[PROOFSTEP]
tauto
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ (ε : ℝ≥0∞), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
[PROOFSTEP]
rw [← nhdsWithin_univ b, tendsto_nhdsWithin_nhdsWithin]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ (∀ (ε : ℝ≥0∞), ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → f x ∈ univ ∧ edist (f x) b < ε) ↔
    ∀ (ε : ℝ≥0∞), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
[PROOFSTEP]
simp only [mem_univ, true_and_iff]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ IsOpen s ↔ ∀ (x : α), x ∈ s → ∃ ε, ε > 0 ∧ ball x ε ⊆ s
[PROOFSTEP]
simp [isOpen_iff_nhds, mem_nhds_iff]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x✝ y✝ z✝ : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : PseudoEMetricSpace β
x : α
y : β
r : ℝ≥0∞
z : α × β
⊢ z ∈ ball x r ×ˢ ball y r ↔ z ∈ ball (x, y) r
[PROOFSTEP]
simp [Prod.edist_eq]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x✝ y✝ z✝ : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : PseudoEMetricSpace β
x : α
y : β
r : ℝ≥0∞
z : α × β
⊢ z ∈ closedBall x r ×ˢ closedBall y r ↔ z ∈ closedBall (x, y) r
[PROOFSTEP]
simp [Prod.edist_eq]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ (∀ (i : ℝ≥0∞), 0 < i → ∃ y, y ∈ s ∧ y ∈ ball x i) ↔ ∀ (ε : ℝ≥0∞), ε > 0 → ∃ y, y ∈ s ∧ edist x y < ε
[PROOFSTEP]
simp only [mem_ball, edist_comm x]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
a : α
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, True ∧ ∀ (x : β), x ∈ Ici ia → u x ∈ ball a ib) ↔
    ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n : β), n ≥ N → edist (u n) a < ε
[PROOFSTEP]
simp only [exists_prop, true_and_iff, mem_Ici, mem_ball]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ Inseparable x y ↔ edist x y = 0
[PROOFSTEP]
simp [inseparable_iff_mem_closure, mem_closure_iff, edist_comm, forall_lt_iff_le']
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ closure t
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | ⟨x₀, hx₀⟩)
[GOAL]
case inl
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ ∅ ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
⊢ ∃ t, t ⊆ ∅ ∧ Set.Countable t ∧ ∅ ⊆ closure t
[PROOFSTEP]
exact ⟨∅, empty_subset _, countable_empty, empty_subset _⟩
[GOAL]
case inr.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ closure t
[PROOFSTEP]
choose! T hTc hsT using fun n : ℕ => hs n⁻¹ (by simp)
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
n : ℕ
⊢ (↑n)⁻¹ > 0
[PROOFSTEP]
simp
[GOAL]
case inr.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsT : ∀ (n : ℕ), s ⊆ ⋃ (x : α) (_ : x ∈ T n), closedBall x (↑n)⁻¹
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ closure t
[PROOFSTEP]
have : ∀ r x, ∃ y ∈ s, closedBall x r ∩ s ⊆ closedBall y (r * 2) := fun r x =>
  by
  rcases(closedBall x r ∩ s).eq_empty_or_nonempty with (he | ⟨y, hxy, hys⟩)
  · refine' ⟨x₀, hx₀, _⟩
    rw [he]
    exact empty_subset _
  · refine' ⟨y, hys, fun z hz => _⟩
    calc
      edist z y ≤ edist z x + edist y x := edist_triangle_right _ _ _
      _ ≤ r + r := (add_le_add hz.1 hxy)
      _ = r * 2 := (mul_two r).symm
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsT : ∀ (n : ℕ), s ⊆ ⋃ (x : α) (_ : x ∈ T n), closedBall x (↑n)⁻¹
r : ℝ≥0∞
x : α
⊢ ∃ y, y ∈ s ∧ closedBall x r ∩ s ⊆ closedBall y (r * 2)
[PROOFSTEP]
rcases(closedBall x r ∩ s).eq_empty_or_nonempty with (he | ⟨y, hxy, hys⟩)
[GOAL]
case inl
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsT : ∀ (n : ℕ), s ⊆ ⋃ (x : α) (_ : x ∈ T n), closedBall x (↑n)⁻¹
r : ℝ≥0∞
x : α
he : closedBall x r ∩ s = ∅
⊢ ∃ y, y ∈ s ∧ closedBall x r ∩ s ⊆ closedBall y (r * 2)
[PROOFSTEP]
refine' ⟨x₀, hx₀, _⟩
[GOAL]
case inl
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsT : ∀ (n : ℕ), s ⊆ ⋃ (x : α) (_ : x ∈ T n), closedBall x (↑n)⁻¹
r : ℝ≥0∞
x : α
he : closedBall x r ∩ s = ∅
⊢ closedBall x r ∩ s ⊆ closedBall x₀ (r * 2)
[PROOFSTEP]
rw [he]
[GOAL]
case inl
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsT : ∀ (n : ℕ), s ⊆ ⋃ (x : α) (_ : x ∈ T n), closedBall x (↑n)⁻¹
r : ℝ≥0∞
x : α
he : closedBall x r ∩ s = ∅
⊢ ∅ ⊆ closedBall x₀ (r * 2)
[PROOFSTEP]
exact empty_subset _
[GOAL]
case inr.intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y✝ z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsT : ∀ (n : ℕ), s ⊆ ⋃ (x : α) (_ : x ∈ T n), closedBall x (↑n)⁻¹
r : ℝ≥0∞
x y : α
hxy : y ∈ closedBall x r
hys : y ∈ s
⊢ ∃ y, y ∈ s ∧ closedBall x r ∩ s ⊆ closedBall y (r * 2)
[PROOFSTEP]
refine' ⟨y, hys, fun z hz => _⟩
[GOAL]
case inr.intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y✝ z✝ : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsT : ∀ (n : ℕ), s ⊆ ⋃ (x : α) (_ : x ∈ T n), closedBall x (↑n)⁻¹
r : ℝ≥0∞
x y : α
hxy : y ∈ closedBall x r
hys : y ∈ s
z : α
hz : z ∈ closedBall x r ∩ s
⊢ z ∈ closedBall y (r * 2)
[PROOFSTEP]
calc
  edist z y ≤ edist z x + edist y x := edist_triangle_right _ _ _
  _ ≤ r + r := (add_le_add hz.1 hxy)
  _ = r * 2 := (mul_two r).symm
[GOAL]
case inr.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsT : ∀ (n : ℕ), s ⊆ ⋃ (x : α) (_ : x ∈ T n), closedBall x (↑n)⁻¹
this : ∀ (r : ℝ≥0∞) (x : α), ∃ y, y ∈ s ∧ closedBall x r ∩ s ⊆ closedBall y (r * 2)
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ closure t
[PROOFSTEP]
choose f hfs hf using this
[GOAL]
case inr.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsT : ∀ (n : ℕ), s ⊆ ⋃ (x : α) (_ : x ∈ T n), closedBall x (↑n)⁻¹
f : ℝ≥0∞ → α → α
hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s
hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ closure t
[PROOFSTEP]
refine'
  ⟨⋃ n : ℕ, f n⁻¹ '' T n, iUnion_subset fun n => image_subset_iff.2 fun z _ => hfs _ _,
    countable_iUnion fun n => (hTc n).image _, _⟩
[GOAL]
case inr.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsT : ∀ (n : ℕ), s ⊆ ⋃ (x : α) (_ : x ∈ T n), closedBall x (↑n)⁻¹
f : ℝ≥0∞ → α → α
hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s
hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)
⊢ s ⊆ closure (⋃ (n : ℕ), f (↑n)⁻¹ '' T n)
[PROOFSTEP]
refine' fun x hx => mem_closure_iff.2 fun ε ε0 => _
[GOAL]
case inr.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsT : ∀ (n : ℕ), s ⊆ ⋃ (x : α) (_ : x ∈ T n), closedBall x (↑n)⁻¹
f : ℝ≥0∞ → α → α
hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s
hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)
x : α
hx : x ∈ s
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∃ y, y ∈ ⋃ (n : ℕ), f (↑n)⁻¹ '' T n ∧ edist x y < ε
[PROOFSTEP]
rcases ENNReal.exists_inv_nat_lt (ENNReal.half_pos ε0.lt.ne').ne' with ⟨n, hn⟩
[GOAL]
case inr.intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsT : ∀ (n : ℕ), s ⊆ ⋃ (x : α) (_ : x ∈ T n), closedBall x (↑n)⁻¹
f : ℝ≥0∞ → α → α
hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s
hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)
x : α
hx : x ∈ s
ε : ℝ≥0∞
ε0 : ε > 0
n : ℕ
hn : (↑n)⁻¹ < ε / 2
⊢ ∃ y, y ∈ ⋃ (n : ℕ), f (↑n)⁻¹ '' T n ∧ edist x y < ε
[PROOFSTEP]
rcases mem_iUnion₂.1 (hsT n hx) with ⟨y, hyn, hyx⟩
[GOAL]
case inr.intro.intro.intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y✝ z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsT : ∀ (n : ℕ), s ⊆ ⋃ (x : α) (_ : x ∈ T n), closedBall x (↑n)⁻¹
f : ℝ≥0∞ → α → α
hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s
hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)
x : α
hx : x ∈ s
ε : ℝ≥0∞
ε0 : ε > 0
n : ℕ
hn : (↑n)⁻¹ < ε / 2
y : α
hyn : y ∈ T n
hyx : x ∈ closedBall y (↑n)⁻¹
⊢ ∃ y, y ∈ ⋃ (n : ℕ), f (↑n)⁻¹ '' T n ∧ edist x y < ε
[PROOFSTEP]
refine' ⟨f n⁻¹ y, mem_iUnion.2 ⟨n, mem_image_of_mem _ hyn⟩, _⟩
[GOAL]
case inr.intro.intro.intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y✝ z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsT : ∀ (n : ℕ), s ⊆ ⋃ (x : α) (_ : x ∈ T n), closedBall x (↑n)⁻¹
f : ℝ≥0∞ → α → α
hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s
hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)
x : α
hx : x ∈ s
ε : ℝ≥0∞
ε0 : ε > 0
n : ℕ
hn : (↑n)⁻¹ < ε / 2
y : α
hyn : y ∈ T n
hyx : x ∈ closedBall y (↑n)⁻¹
⊢ edist x (f (↑n)⁻¹ y) < ε
[PROOFSTEP]
calc
  edist x (f n⁻¹ y) ≤ (n : ℝ≥0∞)⁻¹ * 2 := hf _ _ ⟨hyx, hx⟩
  _ < ε := ENNReal.mul_lt_of_lt_div hn
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : IsSeparable s
⊢ SeparableSpace ↑s
[PROOFSTEP]
have : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε := fun ε ε0 =>
  by
  rcases hs with ⟨t, htc, hst⟩
  refine ⟨t, htc, hst.trans fun x hx => ?_⟩
  rcases mem_closure_iff.1 hx ε ε0 with ⟨y, hyt, hxy⟩
  exact mem_iUnion₂.2 ⟨y, hyt, mem_closedBall.2 hxy.le⟩
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : IsSeparable s
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
[PROOFSTEP]
rcases hs with ⟨t, htc, hst⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s✝ t✝ s : Set α
ε : ℝ≥0∞
ε0 : ε > 0
t : Set α
htc : Set.Countable t
hst : s ⊆ closure t
⊢ ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
[PROOFSTEP]
refine ⟨t, htc, hst.trans fun x hx => ?_⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s✝ t✝ s : Set α
ε : ℝ≥0∞
ε0 : ε > 0
t : Set α
htc : Set.Countable t
hst : s ⊆ closure t
x : α
hx : x ∈ closure t
⊢ x ∈ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
[PROOFSTEP]
rcases mem_closure_iff.1 hx ε ε0 with ⟨y, hyt, hxy⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y✝ z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s✝ t✝ s : Set α
ε : ℝ≥0∞
ε0 : ε > 0
t : Set α
htc : Set.Countable t
hst : s ⊆ closure t
x : α
hx : x ∈ closure t
y : α
hyt : y ∈ t
hxy : edist x y < ε
⊢ x ∈ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
[PROOFSTEP]
exact mem_iUnion₂.2 ⟨y, hyt, mem_closedBall.2 hxy.le⟩
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : IsSeparable s
this : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
⊢ SeparableSpace ↑s
[PROOFSTEP]
rcases subset_countable_closure_of_almost_dense_set _ this with ⟨t, hts, htc, hst⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t✝ s : Set α
hs : IsSeparable s
this : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
t : Set α
hts : t ⊆ s
htc : Set.Countable t
hst : s ⊆ closure t
⊢ SeparableSpace ↑s
[PROOFSTEP]
lift t to Set s using hts
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t✝ s : Set α
hs : IsSeparable s
this : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
t : Set ↑s
htc : Set.Countable ((fun x x_1 => x '' x_1) Subtype.val t)
hst : s ⊆ closure ((fun x x_1 => x '' x_1) Subtype.val t)
⊢ SeparableSpace ↑s
[PROOFSTEP]
refine ⟨⟨t, countable_of_injective_of_countable_image (Subtype.coe_injective.injOn _) htc, ?_⟩⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t✝ s : Set α
hs : IsSeparable s
this : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
t : Set ↑s
htc : Set.Countable ((fun x x_1 => x '' x_1) Subtype.val t)
hst : s ⊆ closure ((fun x x_1 => x '' x_1) Subtype.val t)
⊢ Dense t
[PROOFSTEP]
rwa [inducing_subtype_val.dense_iff, Subtype.forall]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : IsCompact s
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ closure t
[PROOFSTEP]
refine' subset_countable_closure_of_almost_dense_set s fun ε hε => _
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s✝ t s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
[PROOFSTEP]
rcases totallyBounded_iff'.1 hs.totallyBounded ε hε with ⟨t, -, htf, hst⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε✝ ε₁ ε₂ : ℝ≥0∞
s✝ t✝ s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
t : Set α
htf : Set.Finite t
hst : s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
⊢ ∃ t, Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
[PROOFSTEP]
exact ⟨t, htf.countable, hst.trans <| iUnion₂_mono fun _ _ => ball_subset_closedBall⟩
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
⊢ SecondCountableTopology α
[PROOFSTEP]
suffices SeparableSpace α by exact UniformSpace.secondCountable_of_separable α
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
this : SeparableSpace α
⊢ SecondCountableTopology α
[PROOFSTEP]
exact UniformSpace.secondCountable_of_separable α
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
⊢ SeparableSpace α
[PROOFSTEP]
choose T _ hTc hsubT using fun n => subset_countable_closure_of_compact (isCompact_compactCovering α n)
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
T : ℕ → Set α
h✝ : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure (T n)
⊢ SeparableSpace α
[PROOFSTEP]
refine' ⟨⟨⋃ n, T n, countable_iUnion hTc, fun x => _⟩⟩
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
T : ℕ → Set α
h✝ : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure (T n)
x : α
⊢ x ∈ closure (⋃ (n : ℕ), T n)
[PROOFSTEP]
rcases iUnion_eq_univ_iff.1 (iUnion_compactCovering α) x with ⟨n, hn⟩
[GOAL]
case intro
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
T : ℕ → Set α
h✝ : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), Set.Countable (T n)
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure (T n)
x : α
n : ℕ
hn : x ∈ compactCovering α n
⊢ x ∈ closure (⋃ (n : ℕ), T n)
[PROOFSTEP]
exact closure_mono (subset_iUnion _ n) (hsubT _ hn)
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ ⋃ (x : α) (_ : x ∈ t), closedBall x ε = univ
⊢ SecondCountableTopology α
[PROOFSTEP]
suffices SeparableSpace α from UniformSpace.secondCountable_of_separable α
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ ⋃ (x : α) (_ : x ∈ t), closedBall x ε = univ
⊢ SeparableSpace α
[PROOFSTEP]
have : ∀ ε > 0, ∃ t : Set α, Set.Countable t ∧ univ ⊆ ⋃ x ∈ t, closedBall x ε
[GOAL]
case this
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ ⋃ (x : α) (_ : x ∈ t), closedBall x ε = univ
⊢ ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ univ ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
[PROOFSTEP]
simpa only [univ_subset_iff] using hs
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ ⋃ (x : α) (_ : x ∈ t), closedBall x ε = univ
this : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ univ ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
⊢ SeparableSpace α
[PROOFSTEP]
rcases subset_countable_closure_of_almost_dense_set (univ : Set α) this with ⟨t, -, htc, ht⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ : Set α
hs : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ ⋃ (x : α) (_ : x ∈ t), closedBall x ε = univ
this : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, Set.Countable t ∧ univ ⊆ ⋃ (x : α) (_ : x ∈ t), closedBall x ε
t : Set α
htc : Set.Countable t
ht : univ ⊆ closure t
⊢ SeparableSpace α
[PROOFSTEP]
exact ⟨⟨t, htc, fun x => ht (mem_univ x)⟩⟩
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
d : ℝ≥0∞
⊢ diam s ≤ d ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → edist x y ≤ d
[PROOFSTEP]
simp only [diam, iSup_le_iff]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t : Set α
d : ℝ≥0∞
f : β → α
s : Set β
⊢ diam (f '' s) ≤ d ↔ ∀ (x : β), x ∈ s → ∀ (y : β), y ∈ s → edist (f x) (f y) ≤ d
[PROOFSTEP]
simp only [diam_le_iff, ball_image_iff]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t : Set α
ι : Type u_2
o : Option ι
s : ι → Set α
⊢ diam (⋃ (i : ι) (_ : i ∈ o), s i) = ⨆ (i : ι) (_ : i ∈ o), diam (s i)
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t : Set α
ι : Type u_2
s : ι → Set α
⊢ diam (⋃ (i : ι) (_ : i ∈ none), s i) = ⨆ (i : ι) (_ : i ∈ none), diam (s i)
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t : Set α
ι : Type u_2
s : ι → Set α
val✝ : ι
⊢ diam (⋃ (i : ι) (_ : i ∈ Option.some val✝), s i) = ⨆ (i : ι) (_ : i ∈ Option.some val✝), diam (s i)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
d : ℝ≥0∞
⊢ diam (insert x s) ≤ d ↔ max (⨆ (y : α) (_ : y ∈ s), edist x y) (diam s) ≤ d
[PROOFSTEP]
simp only [diam_le_iff, ball_insert_iff, edist_self, edist_comm x, max_le_iff, iSup_le_iff, zero_le, true_and_iff,
  forall_and, and_self_iff, ← and_assoc]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ diam {x, y} = edist x y
[PROOFSTEP]
simp only [iSup_singleton, diam_insert, diam_singleton, ENNReal.max_zero_right]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ diam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)
[PROOFSTEP]
simp only [diam_insert, iSup_insert, iSup_singleton, diam_singleton, ENNReal.max_zero_right, ENNReal.sup_eq_max]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ diam (s ∪ t) ≤ diam s + edist x y + diam t
[PROOFSTEP]
have A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ diam s + edist x y + diam t := fun a ha b hb =>
  calc
    edist a b ≤ edist a x + edist x y + edist y b := edist_triangle4 _ _ _ _
    _ ≤ diam s + edist x y + diam t :=
      add_le_add (add_le_add (edist_le_diam_of_mem ha xs) le_rfl) (edist_le_diam_of_mem yt hb)
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
⊢ diam (s ∪ t) ≤ diam s + edist x y + diam t
[PROOFSTEP]
refine' diam_le fun a ha b hb => _
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
⊢ edist a b ≤ diam s + edist x y + diam t
[PROOFSTEP]
cases' (mem_union _ _ _).1 ha with h'a h'a
[GOAL]
case inl
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ s
⊢ edist a b ≤ diam s + edist x y + diam t
[PROOFSTEP]
cases' (mem_union _ _ _).1 hb with h'b h'b
[GOAL]
case inr
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ t
⊢ edist a b ≤ diam s + edist x y + diam t
[PROOFSTEP]
cases' (mem_union _ _ _).1 hb with h'b h'b
[GOAL]
case inl.inl
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ s
h'b : b ∈ s
⊢ edist a b ≤ diam s + edist x y + diam t
[PROOFSTEP]
calc
  edist a b ≤ diam s := edist_le_diam_of_mem h'a h'b
  _ ≤ diam s + (edist x y + diam t) := le_self_add
  _ = diam s + edist x y + diam t := (add_assoc _ _ _).symm
[GOAL]
case inl.inr
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ s
h'b : b ∈ t
⊢ edist a b ≤ diam s + edist x y + diam t
[PROOFSTEP]
exact A a h'a b h'b
[GOAL]
case inr.inl
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ t
h'b : b ∈ s
⊢ edist a b ≤ diam s + edist x y + diam t
[PROOFSTEP]
have Z := A b h'b a h'a
[GOAL]
case inr.inl
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ t
h'b : b ∈ s
Z : edist b a ≤ diam s + edist x y + diam t
⊢ edist a b ≤ diam s + edist x y + diam t
[PROOFSTEP]
rwa [edist_comm] at Z
[GOAL]
case inr.inr
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ t
h'b : b ∈ t
⊢ edist a b ≤ diam s + edist x y + diam t
[PROOFSTEP]
calc
  edist a b ≤ diam t := edist_le_diam_of_mem h'a h'b
  _ ≤ diam s + edist x y + diam t := le_add_self
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
h : Set.Nonempty (s ∩ t)
⊢ diam (s ∪ t) ≤ diam s + diam t
[PROOFSTEP]
let ⟨x, ⟨xs, xt⟩⟩ := h
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
h : Set.Nonempty (s ∩ t)
x : α
xs : x ∈ s
xt : x ∈ t
⊢ diam (s ∪ t) ≤ diam s + diam t
[PROOFSTEP]
simpa using diam_union xs xt
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t : Set α
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), diam (s b) ≤ c
⊢ diam (Set.pi univ s) ≤ c
[PROOFSTEP]
refine diam_le fun x hx y hy => edist_pi_le_iff.mpr ?_
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
x✝ y✝ z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t : Set α
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), diam (s b) ≤ c
x : (i : β) → π i
hx : x ∈ Set.pi univ s
y : (i : β) → π i
hy : y ∈ Set.pi univ s
⊢ ∀ (b : β), edist (x b) (y b) ≤ c
[PROOFSTEP]
rw [mem_univ_pi] at hx hy
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
x✝ y✝ z : α
ε ε₁ ε₂ : ℝ≥0∞
s✝ t : Set α
π : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), diam (s b) ≤ c
x : (i : β) → π i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → π i
hy : ∀ (i : β), y i ∈ s i
⊢ ∀ (b : β), edist (x b) (y b) ≤ c
[PROOFSTEP]
exact fun b => diam_le_iff.1 (h b) (x b) (hx b) (y b) (hy b)
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
γ : Type w
inst✝ : EMetricSpace γ
x y : γ
⊢ 0 < edist x y ↔ x ≠ y
[PROOFSTEP]
simp [← not_le]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
γ : Type w
inst✝¹ : EMetricSpace γ
inst✝ : EMetricSpace β
f : γ → β
⊢ UniformEmbedding f ↔
    (∀ (ε : ℝ≥0∞), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧
      ∀ (δ : ℝ≥0∞), δ > 0 → ∃ ε, ε > 0 ∧ ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ
[PROOFSTEP]
rw [uniformEmbedding_iff_uniformInducing, uniformInducing_iff, uniformContinuous_iff]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
hs : IsCompact s
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s = closure t
[PROOFSTEP]
rcases subset_countable_closure_of_compact hs with ⟨t, hts, htc, hsub⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
hs : IsCompact s
t : Set γ
hts : t ⊆ s
htc : Set.Countable t
hsub : s ⊆ closure t
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s = closure t
[PROOFSTEP]
exact ⟨t, hts, htc, hsub.antisymm (closure_minimal hts hs.isClosed)⟩
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
⊢ 0 < diam s ↔ Set.Nontrivial s
[PROOFSTEP]
simp only [pos_iff_ne_zero, Ne.def, diam_eq_zero_iff, Set.not_subsingleton_iff]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
⊢ 0 < diam s ↔ ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y
[PROOFSTEP]
simp only [diam_pos_iff, Set.Nontrivial, exists_prop]
[GOAL]
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
γ : Type w
inst✝¹ : EMetricSpace γ
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0∞
x✝ : 0 < ε
⊢ (fun p =>
        (Quotient.mk (UniformSpace.separationSetoid X) p.fst, Quotient.mk (UniformSpace.separationSetoid X) p.snd)) ''
      {p | edist p.fst p.snd < ε} =
    {p | edist p.fst p.snd < ε}
[PROOFSTEP]
ext ⟨⟨x⟩, ⟨y⟩⟩
[GOAL]
case h.mk.mk.mk
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
γ : Type w
inst✝¹ : EMetricSpace γ
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0∞
x✝ : 0 < ε
fst✝ snd✝ : Quotient (UniformSpace.separationSetoid X)
x y : X
⊢ (Quot.mk Setoid.r x, Quot.mk Setoid.r y) ∈
      (fun p =>
          (Quotient.mk (UniformSpace.separationSetoid X) p.fst, Quotient.mk (UniformSpace.separationSetoid X) p.snd)) ''
        {p | edist p.fst p.snd < ε} ↔
    (Quot.mk Setoid.r x, Quot.mk Setoid.r y) ∈ {p | edist p.fst p.snd < ε}
[PROOFSTEP]
refine ⟨?_, fun h => ⟨(x, y), h, rfl⟩⟩
[GOAL]
case h.mk.mk.mk
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
γ : Type w
inst✝¹ : EMetricSpace γ
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0∞
x✝ : 0 < ε
fst✝ snd✝ : Quotient (UniformSpace.separationSetoid X)
x y : X
⊢ (Quot.mk Setoid.r x, Quot.mk Setoid.r y) ∈
      (fun p =>
          (Quotient.mk (UniformSpace.separationSetoid X) p.fst, Quotient.mk (UniformSpace.separationSetoid X) p.snd)) ''
        {p | edist p.fst p.snd < ε} →
    (Quot.mk Setoid.r x, Quot.mk Setoid.r y) ∈ {p | edist p.fst p.snd < ε}
[PROOFSTEP]
rintro ⟨⟨x', y'⟩, h', h⟩
[GOAL]
case h.mk.mk.mk.intro.mk.intro
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
γ : Type w
inst✝¹ : EMetricSpace γ
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0∞
x✝ : 0 < ε
fst✝ snd✝ : Quotient (UniformSpace.separationSetoid X)
x y x' y' : X
h' : (x', y') ∈ {p | edist p.fst p.snd < ε}
h :
  (fun p => (Quotient.mk (UniformSpace.separationSetoid X) p.fst, Quotient.mk (UniformSpace.separationSetoid X) p.snd))
      (x', y') =
    (Quot.mk Setoid.r x, Quot.mk Setoid.r y)
⊢ (Quot.mk Setoid.r x, Quot.mk Setoid.r y) ∈ {p | edist p.fst p.snd < ε}
[PROOFSTEP]
simp only [Prod.ext_iff] at h
[GOAL]
case h.mk.mk.mk.intro.mk.intro
α : Type u
β : Type v
X : Type u_1
inst✝² : PseudoEMetricSpace α
γ : Type w
inst✝¹ : EMetricSpace γ
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0∞
x✝ : 0 < ε
fst✝ snd✝ : Quotient (UniformSpace.separationSetoid X)
x y x' y' : X
h' : (x', y') ∈ {p | edist p.fst p.snd < ε}
h :
  Quotient.mk (UniformSpace.separationSetoid X) x' = Quot.mk Setoid.r x ∧
    Quotient.mk (UniformSpace.separationSetoid X) y' = Quot.mk Setoid.r y
⊢ (Quot.mk Setoid.r x, Quot.mk Setoid.r y) ∈ {p | edist p.fst p.snd < ε}
[PROOFSTEP]
rwa [← h.1, ← h.2]