-- Mathlib/Topology/MetricSpace/CantorScheme.lean
theorem VanishingDiam.map_continuous [TopologicalSpace β] [DiscreteTopology β]
    (hA : VanishingDiam A) : Continuous (inducedMap A).2

Proof state:
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 ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
⊢ ∀ y ∈ Subtype.val ⁻¹' cylinder x n, dist ((inducedMap A).snd y) ((inducedMap A).snd ⟨x, hx⟩) < ε

Tactic:
rintro ⟨y, hy⟩ hyx

Result:
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 ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : ⟨y, hy⟩ ∈ Subtype.val ⁻¹' cylinder x n
⊢ dist ((inducedMap A).snd ⟨y, hy⟩) ((inducedMap A).snd ⟨x, hx⟩) < ε

Proof state:
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 ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : ⟨y, hy⟩ ∈ Subtype.val ⁻¹' cylinder x n
⊢ dist ((inducedMap A).snd ⟨y, hy⟩) ((inducedMap A).snd ⟨x, hx⟩) < ε

Tactic:
rw [mem_preimage, Subtype.coe_mk, cylinder_eq_res, mem_setOf] at hyx

Result:
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 ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : res y n = res x n
⊢ dist ((inducedMap A).snd ⟨y, hy⟩) ((inducedMap A).snd ⟨x, hx⟩) < ε

Proof state:
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 ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
⊢ IsOpen (cylinder x n)

Tactic:
apply isOpen_cylinder

Result:
no goals

Proof state:
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 𝓝 ⟨x, hx⟩, dist ((inducedMap A).snd x_1) ((inducedMap A).snd ⟨x, hx⟩) < ε

Tactic:
obtain ⟨n, hn⟩ := hA.dist_lt _ ε_pos x

Result:
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 ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
⊢ ∀ᶠ (x_1 : ↑(inducedMap A).fst) in 𝓝 ⟨x, hx⟩, dist ((inducedMap A).snd x_1) ((inducedMap A).snd ⟨x, hx⟩) < ε

Proof state:
β : 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 ((inducedMap A).snd x) ((inducedMap A).snd a) < ε

Tactic:
rintro ⟨x, hx⟩ ε ε_pos

Result:
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 𝓝 ⟨x, hx⟩, dist ((inducedMap A).snd x_1) ((inducedMap A).snd ⟨x, hx⟩) < ε

Proof state:
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 ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hyx : res y n = res x n
⊢ (inducedMap A).snd ⟨y, hy⟩ ∈ A (res y n)

Tactic:
apply map_mem

Result:
no goals

Proof state:
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 ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
⊢ IsOpen (Subtype.val ⁻¹' cylinder x n)

Tactic:
apply continuous_subtype_val.isOpen_preimage

Result:
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 ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
⊢ IsOpen (cylinder x n)

Proof state:
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 ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
⊢ ∃ t, (∀ y ∈ t, dist ((inducedMap A).snd y) ((inducedMap A).snd ⟨x, hx⟩) < ε) ∧ IsOpen t ∧ ⟨x, hx⟩ ∈ t

Tactic:
refine ⟨(↑)⁻¹' cylinder x n, ?_, ?_, by simp⟩

Result:
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 ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
⊢ ∀ y ∈ Subtype.val ⁻¹' cylinder x n, dist ((inducedMap A).snd y) ((inducedMap A).snd ⟨x, 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 ∈ A (res x n), ∀ z ∈ A (res x n), dist y z < ε
⊢ IsOpen (Subtype.val ⁻¹' cylinder x n)

Proof state:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
⊢ Continuous (inducedMap A).snd

Tactic:
rw [Metric.continuous_iff']

Result:
β : 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 ((inducedMap A).snd x) ((inducedMap A).snd a) < ε