β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
⊢ ∀ (a : ↑(inducedMap A).fst) (ε : ℝ),
    ε > 0 → ∀ᶠ (x : ↑(inducedMap A).fst) in 𝓝 a, dist (Sigma.snd (inducedMap A) x) (Sigma.snd (inducedMap A) a) < ε
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
⊢ Continuous (inducedMap A).snd
rw [Metric.continuous_iff']
case mk
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
⊢ ∀ᶠ (x_1 : ↑(inducedMap A).fst) in 𝓝 { val := x, property := hx },
    dist (Sigma.snd (inducedMap A) x_1) (Sigma.snd (inducedMap A) { val := x, property := hx }) < ε
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
⊢ ∀ (a : ↑(inducedMap A).fst) (ε : ℝ),
    ε > 0 → ∀ᶠ (x : ↑(inducedMap A).fst) in 𝓝 a, dist (Sigma.snd (inducedMap A) x) (Sigma.snd (inducedMap A) a) < ε
rintro ⟨x, hx⟩ ε ε_pos
case mk.intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ ∀ᶠ (x_1 : ↑(inducedMap A).fst) in 𝓝 { val := x, property := hx },
    dist (Sigma.snd (inducedMap A) x_1) (Sigma.snd (inducedMap A) { val := x, property := hx }) < ε
case mk
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
⊢ ∀ᶠ (x_1 : ↑(inducedMap A).fst) in 𝓝 { val := x, property := hx },
    dist (Sigma.snd (inducedMap A) x_1) (Sigma.snd (inducedMap A) { val := x, property := hx }) < ε
cases' hA.dist_lt _ ε_pos x with n hn
case mk.intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ ∃ t,
    (∀ (x_1 : ↑(inducedMap A).fst),
        x_1 ∈ t → dist (Sigma.snd (inducedMap A) x_1) (Sigma.snd (inducedMap A) { val := x, property := hx }) < ε) ∧
      IsOpen t ∧ { val := x, property := hx } ∈ t
case mk.intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ ∀ᶠ (x_1 : ↑(inducedMap A).fst) in 𝓝 { val := x, property := hx },
    dist (Sigma.snd (inducedMap A) x_1) (Sigma.snd (inducedMap A) { val := x, property := hx }) < ε
rw [_root_.eventually_nhds_iff]
case mk.intro.refine'_1
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ ∀ (x_1 : ↑(inducedMap A).fst),
    x_1 ∈ Subtype.val ⁻¹' cylinder x n →
      dist (Sigma.snd (inducedMap A) x_1) (Sigma.snd (inducedMap A) { val := x, property := hx }) < ε

case mk.intro.refine'_2
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ IsOpen (Subtype.val ⁻¹' cylinder x n)
case mk.intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ ∃ t,
    (∀ (x_1 : ↑(inducedMap A).fst),
        x_1 ∈ t → dist (Sigma.snd (inducedMap A) x_1) (Sigma.snd (inducedMap A) { val := x, property := hx }) < ε) ∧
      IsOpen t ∧ { val := x, property := hx } ∈ t
refine' ⟨(↑)⁻¹' cylinder x n, _, _, by simp⟩
case mk.intro.refine'_2.a
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ IsOpen (cylinder x n)
case mk.intro.refine'_2
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ IsOpen (Subtype.val ⁻¹' cylinder x n)
apply continuous_subtype_val.isOpen_preimage
no goals
case mk.intro.refine'_2.a
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ IsOpen (cylinder x n)
apply isOpen_cylinder
no goals
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' cylinder x n
simp
case mk.intro.refine'_1.mk
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : { val := y, property := hy } ∈ Subtype.val ⁻¹' cylinder x n
⊢ dist (Sigma.snd (inducedMap A) { val := y, property := hy }) (Sigma.snd (inducedMap A) { val := x, property := hx }) <
    ε
case mk.intro.refine'_1
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ ∀ (x_1 : ↑(inducedMap A).fst),
    x_1 ∈ Subtype.val ⁻¹' cylinder x n →
      dist (Sigma.snd (inducedMap A) x_1) (Sigma.snd (inducedMap A) { val := x, property := hx }) < ε
rintro ⟨y, hy⟩ hyx
case mk.intro.refine'_1.mk
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : res y n = res x n
⊢ dist (Sigma.snd (inducedMap A) { val := y, property := hy }) (Sigma.snd (inducedMap A) { val := x, property := hx }) <
    ε
case mk.intro.refine'_1.mk
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : { val := y, property := hy } ∈ Subtype.val ⁻¹' cylinder x n
⊢ dist (Sigma.snd (inducedMap A) { val := y, property := hy }) (Sigma.snd (inducedMap A) { val := x, property := hx }) <
    ε
rw [mem_preimage, Subtype.coe_mk, cylinder_eq_res, mem_setOf] at hyx
case mk.intro.refine'_1.mk.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : res y n = res x n
⊢ Sigma.snd (inducedMap A) { val := y, property := hy } ∈ A (res x n)

case mk.intro.refine'_1.mk.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : res y n = res x n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (res x n)
case mk.intro.refine'_1.mk
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : res y n = res x n
⊢ dist (Sigma.snd (inducedMap A) { val := y, property := hy }) (Sigma.snd (inducedMap A) { val := x, property := hx }) <
    ε
apply hn
no goals
case mk.intro.refine'_1.mk.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : res y n = res x n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (res x n)
apply map_mem
case mk.intro.refine'_1.mk.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : res y n = res x n
⊢ Sigma.snd (inducedMap A) { val := y, property := hy } ∈ A (res y n)
case mk.intro.refine'_1.mk.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : res y n = res x n
⊢ Sigma.snd (inducedMap A) { val := y, property := hy } ∈ A (res x n)
rw [← hyx]
no goals
case mk.intro.refine'_1.mk.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : res y n = res x n
⊢ Sigma.snd (inducedMap A) { val := y, property := hy } ∈ A (res y n)
apply map_mem