[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
⊢ Sigma.snd (inducedMap A) x ∈ A (res (↑x) n)
[PROOFSTEP]
have := x.property.some_mem
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
this : Set.Nonempty.some (_ : ↑x ∈ (inducedMap A).fst) ∈ ⋂ (n : ℕ), A (res (↑x) n)
⊢ Sigma.snd (inducedMap A) x ∈ A (res (↑x) n)
[PROOFSTEP]
rw [mem_iInter] at this 
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
x : ↑(inducedMap A).fst
n : ℕ
this : ∀ (i : ℕ), Set.Nonempty.some (_ : ↑x ∈ (inducedMap A).fst) ∈ A (res (↑x) i)
⊢ Sigma.snd (inducedMap A) x ∈ A (res (↑x) n)
[PROOFSTEP]
exact this n
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
⊢ Injective (inducedMap A).snd
[PROOFSTEP]
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
[GOAL]
case mk.mk
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
[PROOFSTEP]
refine' Subtype.coe_injective (res_injective _)
[GOAL]
case mk.mk
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ res ((fun a => ↑a) { val := x, property := hx }) = res ((fun a => ↑a) { val := y, property := hy })
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ res x = res y
[PROOFSTEP]
ext n : 1
[GOAL]
case mk.mk.h
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
⊢ res x n = res y n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case mk.mk.h.zero
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
⊢ res x Nat.zero = res y Nat.zero
[PROOFSTEP]
simp
[GOAL]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
⊢ res x (Nat.succ n) = res y (Nat.succ n)
[PROOFSTEP]
simp only [res_succ, cons.injEq]
[GOAL]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
⊢ x n = y n ∧ res x n = res y n
[PROOFSTEP]
refine' ⟨_, ih⟩
[GOAL]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
⊢ x n = y n
[PROOFSTEP]
contrapose hA
[GOAL]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ¬CantorScheme.Disjoint A
[PROOFSTEP]
simp only [CantorScheme.Disjoint, _root_.Pairwise, Ne.def, not_forall, exists_prop]
[GOAL]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ∃ x x_1 x_2, ¬x_1 = x_2 ∧ ¬_root_.Disjoint (A (x_1 :: x)) (A (x_2 :: x))
[PROOFSTEP]
refine' ⟨res x n, _, _, hA, _⟩
[GOAL]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ¬_root_.Disjoint (A (x n :: res x n)) (A (y n :: res x n))
[PROOFSTEP]
rw [not_disjoint_iff]
[GOAL]
case mk.mk.h.succ
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ ∃ x_1, x_1 ∈ A (x n :: res x n) ∧ x_1 ∈ A (y n :: res x n)
[PROOFSTEP]
refine' ⟨(inducedMap A).2 ⟨x, hx⟩, _, _⟩
[GOAL]
case mk.mk.h.succ.refine'_1
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (x n :: res x n)
[PROOFSTEP]
rw [← res_succ]
[GOAL]
case mk.mk.h.succ.refine'_1
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (res x (Nat.succ n))
[PROOFSTEP]
apply map_mem
[GOAL]
case mk.mk.h.succ.refine'_2
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := x, property := hx } ∈ A (y n :: res x n)
[PROOFSTEP]
rw [hxy, ih, ← res_succ]
[GOAL]
case mk.mk.h.succ.refine'_2
β : Type u_1
α : Type u_2
A : List β → Set α
x : ℕ → β
hx : x ∈ (inducedMap A).fst
y : ℕ → β
hy : y ∈ (inducedMap A).fst
hxy : Sigma.snd (inducedMap A) { val := x, property := hx } = Sigma.snd (inducedMap A) { val := y, property := hy }
n : ℕ
ih : res x n = res y n
hA : ¬x n = y n
⊢ Sigma.snd (inducedMap A) { val := y, property := hy } ∈ A (res y (Nat.succ n))
[PROOFSTEP]
apply map_mem
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
hA : VanishingDiam A
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
[PROOFSTEP]
specialize hA x
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : Tendsto (fun n => EMetric.diam (A (res x n))) atTop (𝓝 0)
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
[PROOFSTEP]
rw [ENNReal.tendsto_atTop_zero] at hA 
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
[PROOFSTEP]
cases'
  hA (ENNReal.ofReal (ε / 2))
    (by
      simp only [gt_iff_lt, ENNReal.ofReal_pos]
      linarith) with
  n hn
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
⊢ ENNReal.ofReal (ε / 2) > 0
[PROOFSTEP]
simp only [gt_iff_lt, ENNReal.ofReal_pos]
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
⊢ 0 < ε / 2
[PROOFSTEP]
linarith
[GOAL]
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ n, ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
[PROOFSTEP]
use n
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
⊢ ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
[PROOFSTEP]
intro y hy z hz
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ dist y z < ε
[PROOFSTEP]
rw [← ENNReal.ofReal_lt_ofReal_iff ε_pos, ← edist_dist]
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ edist y z < ENNReal.ofReal ε
[PROOFSTEP]
apply lt_of_le_of_lt (EMetric.edist_le_diam_of_mem hy hz)
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ EMetric.diam (A (res x n)) < ENNReal.ofReal ε
[PROOFSTEP]
apply lt_of_le_of_lt (hn _ (le_refl _))
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ ENNReal.ofReal (ε / 2) < ENNReal.ofReal ε
[PROOFSTEP]
rw [ENNReal.ofReal_lt_ofReal_iff ε_pos]
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝ : PseudoMetricSpace α
ε : ℝ
ε_pos : 0 < ε
x : ℕ → β
hA : ∀ (ε : ENNReal), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → EMetric.diam (A (res x n)) ≤ ε
n : ℕ
hn : ∀ (n_1 : ℕ), n_1 ≥ n → EMetric.diam (A (res x n_1)) ≤ ENNReal.ofReal (ε / 2)
y : α
hy : y ∈ A (res x n)
z : α
hz : z ∈ A (res x n)
⊢ ε / 2 < ε
[PROOFSTEP]
linarith
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
⊢ Continuous (inducedMap A).snd
[PROOFSTEP]
rw [Metric.continuous_iff']
[GOAL]
β : 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) < ε
[PROOFSTEP]
rintro ⟨x, hx⟩ ε ε_pos
[GOAL]
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 }) < ε
[PROOFSTEP]
cases' hA.dist_lt _ ε_pos x with n hn
[GOAL]
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 }) < ε
[PROOFSTEP]
rw [_root_.eventually_nhds_iff]
[GOAL]
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
[PROOFSTEP]
refine' ⟨(↑) ⁻¹' cylinder x n, _, _, by simp⟩
[GOAL]
β : 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
[PROOFSTEP]
simp
[GOAL]
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 }) < ε
[PROOFSTEP]
rintro ⟨y, hy⟩ hyx
[GOAL]
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 }) <
    ε
[PROOFSTEP]
rw [mem_preimage, Subtype.coe_mk, cylinder_eq_res, mem_setOf] at hyx 
[GOAL]
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 }) <
    ε
[PROOFSTEP]
apply hn
[GOAL]
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)
[PROOFSTEP]
rw [← hyx]
[GOAL]
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)
[PROOFSTEP]
apply map_mem
[GOAL]
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)
[PROOFSTEP]
apply map_mem
[GOAL]
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)
[PROOFSTEP]
apply continuous_subtype_val.isOpen_preimage
[GOAL]
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)
[PROOFSTEP]
apply isOpen_cylinder
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
⊢ (inducedMap A).fst = univ
[PROOFSTEP]
rw [eq_univ_iff_forall]
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
⊢ ∀ (x : ℕ → β), x ∈ (inducedMap A).fst
[PROOFSTEP]
intro x
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
⊢ x ∈ (inducedMap A).fst
[PROOFSTEP]
choose u hu using fun n => hnonempty (res x n)
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ x ∈ (inducedMap A).fst
[PROOFSTEP]
have umem : ∀ n m : ℕ, n ≤ m → u m ∈ A (res x n) :=
  by
  have : Antitone fun n : ℕ => A (res x n) :=
    by
    refine' antitone_nat_of_succ_le _
    intro n
    apply hanti.antitone
  intro n m hnm
  exact this hnm (hu _)
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
[PROOFSTEP]
have : Antitone fun n : ℕ => A (res x n) :=
  by
  refine' antitone_nat_of_succ_le _
  intro n
  apply hanti.antitone
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ Antitone fun n => A (res x n)
[PROOFSTEP]
refine' antitone_nat_of_succ_le _
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ ∀ (n : ℕ), A (res x (n + 1)) ≤ A (res x n)
[PROOFSTEP]
intro n
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
n : ℕ
⊢ A (res x (n + 1)) ≤ A (res x n)
[PROOFSTEP]
apply hanti.antitone
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
this : Antitone fun n => A (res x n)
⊢ ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
[PROOFSTEP]
intro n m hnm
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
this : Antitone fun n => A (res x n)
n m : ℕ
hnm : n ≤ m
⊢ u m ∈ A (res x n)
[PROOFSTEP]
exact this hnm (hu _)
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ x ∈ (inducedMap A).fst
[PROOFSTEP]
have : CauchySeq u := by
  rw [Metric.cauchySeq_iff]
  intro ε ε_pos
  cases' hdiam.dist_lt _ ε_pos x with n hn
  use n
  intro m₀ hm₀ m₁ hm₁
  apply hn <;> apply umem <;> assumption
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ CauchySeq u
[PROOFSTEP]
rw [Metric.cauchySeq_iff]
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
⊢ ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → dist (u m) (u n) < ε
[PROOFSTEP]
intro ε ε_pos
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
⊢ ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → dist (u m) (u n) < ε
[PROOFSTEP]
cases' hdiam.dist_lt _ ε_pos x with n hn
[GOAL]
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → dist (u m) (u n) < ε
[PROOFSTEP]
use n
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
⊢ ∀ (m : ℕ), m ≥ n → ∀ (n_1 : ℕ), n_1 ≥ n → dist (u m) (u n_1) < ε
[PROOFSTEP]
intro m₀ hm₀ m₁ hm₁
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ dist (u m₀) (u m₁) < ε
[PROOFSTEP]
apply hn
[GOAL]
case h.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ u m₀ ∈ A (res x n)
[PROOFSTEP]
apply umem
[GOAL]
case h.x
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ u m₁ ∈ A (res x n)
[PROOFSTEP]
apply umem
[GOAL]
case h.x.a
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ n ≤ m₀
[PROOFSTEP]
assumption
[GOAL]
case h.x.a
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ (y : α), y ∈ A (res x n) → ∀ (z : α), z ∈ A (res x n) → dist y z < ε
m₀ : ℕ
hm₀ : m₀ ≥ n
m₁ : ℕ
hm₁ : m₁ ≥ n
⊢ n ≤ m₁
[PROOFSTEP]
assumption
[GOAL]
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
⊢ x ∈ (inducedMap A).fst
[PROOFSTEP]
cases' cauchySeq_tendsto_of_complete this with y hy
[GOAL]
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
⊢ x ∈ (inducedMap A).fst
[PROOFSTEP]
use y
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
⊢ y ∈ ⋂ (n : ℕ), A (res x n)
[PROOFSTEP]
rw [mem_iInter]
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
⊢ ∀ (i : ℕ), y ∈ A (res x i)
[PROOFSTEP]
intro n
[GOAL]
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ y ∈ A (res x n)
[PROOFSTEP]
apply hanti _ (x n)
[GOAL]
case h.a
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ y ∈ closure (A (x n :: res x n))
[PROOFSTEP]
apply mem_closure_of_tendsto hy
[GOAL]
case h.a
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ ∀ᶠ (x_1 : ℕ) in atTop, u x_1 ∈ A (x n :: res x n)
[PROOFSTEP]
rw [eventually_atTop]
[GOAL]
case h.a
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), Set.Nonempty (A l)
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → u b ∈ A (x n :: res x n)
[PROOFSTEP]
exact ⟨n.succ, umem _⟩
