α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε / 2 ∧ abv (↑g j) < ε / 2
j : ℕ
ij : j ≥ i
H₁ : abv (↑f j) < ε / 2
H₂ : abv (↑g j) < ε / 2
⊢ abv (↑(f + g) j) < ε
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε / 2 ∧ abv (↑g j) < ε / 2
j : ℕ
ij : j ≥ i
⊢ abv (↑(f + g) j) < ε
let ⟨H₁, H₂⟩ := H _ ij
no goals
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑f j) < ε / 2 ∧ abv (↑g j) < ε / 2
j : ℕ
ij : j ≥ i
H₁ : abv (↑f j) < ε / 2
H₂ : abv (↑g j) < ε / 2
⊢ abv (↑(f + g) j) < ε
simpa [add_halves ε] using lt_of_le_of_lt (abv_add abv _ _) (add_lt_add H₁ H₂)