α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : lim f = 0
hf : f ≈ const abv (lim f)
⊢ LimZero f
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : lim f = 0
⊢ LimZero f
have hf := equiv_lim f
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : lim f = 0
hf : f ≈ const abv 0
⊢ LimZero f
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : lim f = 0
hf : f ≈ const abv (lim f)
⊢ LimZero f
rw [h] at hf
no goals
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : lim f = 0
hf : f ≈ const abv 0
⊢ LimZero f
exact (limZero_congr hf).mpr (const_limZero.mpr rfl)
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : LimZero f
h₁ : f = f - const abv 0
⊢ lim f = 0
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : LimZero f
⊢ lim f = 0
have h₁ : f = f - const abv 0 := ext fun n => by simp [sub_apply, const_apply]
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : LimZero (f - const abv 0)
h₁ : f = f - const abv 0
⊢ lim f = 0
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : LimZero f
h₁ : f = f - const abv 0
⊢ lim f = 0
rw [h₁] at h
no goals
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : LimZero (f - const abv 0)
h₁ : f = f - const abv 0
⊢ lim f = 0
exact lim_eq_of_equiv_const h
no goals
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
h : LimZero f
n : ℕ
⊢ ↑f n = ↑(f - const abv 0) n
simp [sub_apply, const_apply]