-- 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.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⟩) < ε

Tactic:
apply hn

Result:
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 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 ∈ 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 ⟨x, hx⟩ ∈ A (res x n)

Proof state:
β : 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, hx⟩ ∈ Subtype.val ⁻¹' cylinder x n

Tactic:
simp

Result:
no goals

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

Tactic:
rw [_root_.eventually_nhds_iff]

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

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 ⟨x, hx⟩ ∈ A (res x n)

Tactic:
apply map_mem

Result:
no goals

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 x n)

Tactic:
rw [← hyx]

Result:
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)