Theorem: IMOSL.Extra.Infinitesimal.mul_of_abs_le_one_left (IMOSLLean4/Extra/Infinitesimal/Basic.lean)

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε r : R
hε : Infinitesimal ε
hr : |r| ≤ 1
k : ℕ
⊢ k • |r * ε| < 1
Tactic:
rw [abs_mul, nsmul_eq_mul', mul_assoc, ← nsmul_eq_mul']
State after:
R : Type u_1
inst✝ : LinearOrderedRing R
ε r : R
hε : Infinitesimal ε
hr : |r| ≤ 1
k : ℕ
⊢ |r| * k • |ε| < 1

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε r : R
hε : Infinitesimal ε
hr : |r| ≤ 1
k : ℕ
⊢ |r| * k • |ε| < 1
Tactic:
exact mul_lt_one_of_nonneg_of_lt_one_right hr (nsmul_nonneg (abs_nonneg ε) k) (hε k)
State after:
no goals