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