[GOAL]
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
⊢ ∀ (s : Set β), IsOpen s → lim f ∈ s → ↑f ⁻¹' s ∈ atTop
[PROOFSTEP]
intro s os lfs
[GOAL]
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
⊢ ↑f ⁻¹' s ∈ atTop
[PROOFSTEP]
suffices ∃ a : ℕ, ∀ b : ℕ, b ≥ a → f b ∈ s by simpa using this
[GOAL]
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
this : ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
⊢ ↑f ⁻¹' s ∈ atTop
[PROOFSTEP]
simpa using this
[GOAL]
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
[PROOFSTEP]
rcases Metric.isOpen_iff.1 os _ lfs with ⟨ε, ⟨hε, hεs⟩⟩
[GOAL]
case intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
[PROOFSTEP]
cases' Setoid.symm (CauSeq.equiv_lim f) _ hε with N hN
[GOAL]
case intro.intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑f b ∈ s
[PROOFSTEP]
exists N
[GOAL]
case intro.intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
⊢ ∀ (b : ℕ), b ≥ N → ↑f b ∈ s
[PROOFSTEP]
intro b hb
[GOAL]
case intro.intro.intro
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ ↑f b ∈ s
[PROOFSTEP]
apply hεs
[GOAL]
case intro.intro.intro.a
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ ↑f b ∈ Metric.ball (lim f) ε
[PROOFSTEP]
dsimp [Metric.ball]
[GOAL]
case intro.intro.intro.a
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ dist (↑f b) (lim f) < ε
[PROOFSTEP]
rw [dist_comm, dist_eq_norm]
[GOAL]
case intro.intro.intro.a
β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
s : Set β
os : IsOpen s
lfs : lim f ∈ s
ε : ℝ
hε : ε > 0
hεs : Metric.ball (lim f) ε ⊆ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(const norm (lim f) - f) j‖ < ε
b : ℕ
hb : b ≥ N
⊢ ‖lim f - ↑f b‖ < ε
[PROOFSTEP]
solve_by_elim
[GOAL]
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
⊢ IsCauSeq norm f
[PROOFSTEP]
cases' cauchy_iff.1 hf with hf1 hf2
[GOAL]
case intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
⊢ IsCauSeq norm f
[PROOFSTEP]
intro ε hε
[GOAL]
case intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖f j - f i‖ < ε
[PROOFSTEP]
rcases hf2 {x | dist x.1 x.2 < ε} (dist_mem_uniformity hε) with ⟨t, ⟨ht, htsub⟩⟩
[GOAL]
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
ht : t ∈ map f atTop
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖f j - f i‖ < ε
[PROOFSTEP]
simp at ht 
[GOAL]
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
ht : ∃ a, ∀ (b : ℕ), a ≤ b → f b ∈ t
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖f j - f i‖ < ε
[PROOFSTEP]
cases' ht with N hN
[GOAL]
case intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖f j - f i‖ < ε
[PROOFSTEP]
exists N
[GOAL]
case intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
⊢ ∀ (j : ℕ), j ≥ N → ‖f j - f N‖ < ε
[PROOFSTEP]
intro j hj
[GOAL]
case intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
j : ℕ
hj : j ≥ N
⊢ ‖f j - f N‖ < ε
[PROOFSTEP]
rw [← dist_eq_norm]
[GOAL]
case intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
j : ℕ
hj : j ≥ N
⊢ dist (f j) (f N) < ε
[PROOFSTEP]
apply @htsub (f j, f N)
[GOAL]
case intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
j : ℕ
hj : j ≥ N
⊢ (f j, f N) ∈ t ×ˢ t
[PROOFSTEP]
apply Set.mk_mem_prod
[GOAL]
case intro.intro.intro.intro.ha
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
j : ℕ
hj : j ≥ N
⊢ f j ∈ t
[PROOFSTEP]
solve_by_elim [le_refl]
[GOAL]
case intro.intro.intro.intro.hb
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : NeBot (map f atTop)
hf2 : ∀ (s : Set (β × β)), s ∈ uniformity β → ∃ t, t ∈ map f atTop ∧ t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.fst x.snd < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
j : ℕ
hj : j ≥ N
⊢ f N ∈ t
[PROOFSTEP]
solve_by_elim [le_refl]
[GOAL]
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
⊢ CauchySeq ↑f
[PROOFSTEP]
refine' cauchy_iff.2 ⟨by infer_instance, fun s hs => _⟩
[GOAL]
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
⊢ NeBot (map (↑f) atTop)
[PROOFSTEP]
infer_instance
[GOAL]
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
⊢ ∃ t, t ∈ map (↑f) atTop ∧ t ×ˢ t ⊆ s
[PROOFSTEP]
rcases mem_uniformity_dist.1 hs with ⟨ε, ⟨hε, hεs⟩⟩
[GOAL]
case intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
⊢ ∃ t, t ∈ map (↑f) atTop ∧ t ×ˢ t ⊆ s
[PROOFSTEP]
cases' CauSeq.cauchy₂ f hε with N hN
[GOAL]
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ∃ t, t ∈ map (↑f) atTop ∧ t ×ˢ t ⊆ s
[PROOFSTEP]
exists {n | n ≥ N}.image f
[GOAL]
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ↑f '' {n | n ≥ N} ∈ map (↑f) atTop ∧ (↑f '' {n | n ≥ N}) ×ˢ (↑f '' {n | n ≥ N}) ⊆ s
[PROOFSTEP]
simp only [exists_prop, mem_atTop_sets, mem_map, mem_image, ge_iff_le, mem_setOf_eq]
[GOAL]
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ (∃ a, ∀ (b : ℕ), a ≤ b → b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})) ∧ (↑f '' {n | N ≤ n}) ×ˢ (↑f '' {n | N ≤ n}) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})
[PROOFSTEP]
exists N
[GOAL]
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ ∀ (b : ℕ), N ≤ b → b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})
[PROOFSTEP]
intro b hb
[GOAL]
case intro.intro.intro.left
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
b : ℕ
hb : N ≤ b
⊢ b ∈ ↑f ⁻¹' (↑f '' {n | N ≤ n})
[PROOFSTEP]
exists b
[GOAL]
case intro.intro.intro.right
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
⊢ (↑f '' {n | N ≤ n}) ×ˢ (↑f '' {n | N ≤ n}) ⊆ s
[PROOFSTEP]
rintro ⟨a, b⟩ ⟨⟨a', ⟨ha'1, ha'2⟩⟩, ⟨b', ⟨hb'1, hb'2⟩⟩⟩
[GOAL]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ∈ {n | N ≤ n}
ha'2 : ↑f a' = (a, b).fst
b' : ℕ
hb'1 : b' ∈ {n | N ≤ n}
hb'2 : ↑f b' = (a, b).snd
⊢ (a, b) ∈ s
[PROOFSTEP]
dsimp at ha'1 ha'2 hb'1 hb'2 
[GOAL]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ (a, b) ∈ s
[PROOFSTEP]
rw [← ha'2, ← hb'2]
[GOAL]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ (↑f a', ↑f b') ∈ s
[PROOFSTEP]
apply hεs
[GOAL]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ dist (↑f a') (↑f b') < ε
[PROOFSTEP]
rw [dist_eq_norm]
[GOAL]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ ‖↑f a' - ↑f b'‖ < ε
[PROOFSTEP]
apply hN
[GOAL]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a.x
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ a' ≥ N
[PROOFSTEP]
assumption
[GOAL]
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro.a.x
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ {a b : β}, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : N ≤ a'
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : N ≤ b'
hb'2 : ↑f b' = b
⊢ b' ≥ N
[PROOFSTEP]
assumption
[GOAL]
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
⊢ CompleteSpace β
[PROOFSTEP]
apply complete_of_cauchySeq_tendsto
[GOAL]
case a
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
⊢ ∀ (u : ℕ → β), CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)
[PROOFSTEP]
intro u hu
[GOAL]
case a
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (𝓝 a)
[PROOFSTEP]
have C : IsCauSeq norm u := isCauSeq_iff_cauchySeq.2 hu
[GOAL]
case a
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
⊢ ∃ a, Tendsto u atTop (𝓝 a)
[PROOFSTEP]
exists CauSeq.lim ⟨u, C⟩
[GOAL]
case a
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
⊢ Tendsto u atTop (𝓝 (CauSeq.lim { val := u, property := C }))
[PROOFSTEP]
rw [Metric.tendsto_atTop]
[GOAL]
case a
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
⊢ ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (CauSeq.lim { val := u, property := C }) < ε
[PROOFSTEP]
intro ε εpos
[GOAL]
case a
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (CauSeq.lim { val := u, property := C }) < ε
[PROOFSTEP]
cases' (CauSeq.equiv_lim ⟨u, C⟩) _ εpos with N hN
[GOAL]
case a.intro
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
ε : ℝ
εpos : ε > 0
N : ℕ
hN :
  ∀ (j : ℕ), j ≥ N → ‖↑({ val := u, property := C } - CauSeq.const norm (CauSeq.lim { val := u, property := C })) j‖ < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (CauSeq.lim { val := u, property := C }) < ε
[PROOFSTEP]
exists N
[GOAL]
case a.intro
β : Type v
inst✝¹ : NormedField β
inst✝ : CauSeq.IsComplete β norm
u : ℕ → β
hu : CauchySeq u
C : IsCauSeq norm u
ε : ℝ
εpos : ε > 0
N : ℕ
hN :
  ∀ (j : ℕ), j ≥ N → ‖↑({ val := u, property := C } - CauSeq.const norm (CauSeq.lim { val := u, property := C })) j‖ < ε
⊢ ∀ (n : ℕ), n ≥ N → dist (u n) (CauSeq.lim { val := u, property := C }) < ε
[PROOFSTEP]
simpa [dist_eq_norm] using hN
