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

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε : R
hε : Infinitesimal ε
n k : ℕ
⊢ k • |n • ε| < 1
Tactic:
rw [abs_nsmul, ← mul_nsmul']
State after:
R : Type u_1
inst✝ : LinearOrderedRing R
ε : R
hε : Infinitesimal ε
n k : ℕ
⊢ (k * n) • |ε| < 1

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε : R
hε : Infinitesimal ε
n k : ℕ
⊢ (k * n) • |ε| < 1
Tactic:
exact hε _
State after:
no goals