α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : LimZero g
ε : α
ε0 : ε > 0
F : α
F0 : F > 0
hF : ∀ (i : ℕ), abv (↑f i) < F
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑g j) < ε / F
j : ℕ
ij : j ≥ i
this : abv (↑f j) * abv (↑g j) < F * (ε / F)
⊢ abv (↑(f * g) j) < ε
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : LimZero g
ε : α
ε0 : ε > 0
F : α
F0 : F > 0
hF : ∀ (i : ℕ), abv (↑f i) < F
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑g j) < ε / F
j : ℕ
ij : j ≥ i
⊢ abv (↑(f * g) j) < ε
have := mul_lt_mul' (le_of_lt <| hF j) (H _ ij) (abv_nonneg abv _) F0
no goals
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : LimZero g
ε : α
ε0 : ε > 0
F : α
F0 : F > 0
hF : ∀ (i : ℕ), abv (↑f i) < F
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abv (↑g j) < ε / F
j : ℕ
ij : j ≥ i
this : abv (↑f j) * abv (↑g j) < F * (ε / F)
⊢ abv (↑(f * g) j) < ε
rwa [mul_comm F, div_mul_cancel _ (ne_of_gt F0), ← abv_mul] at this