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

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε : R
x✝ : ∃ N, ∀ (k : ℕ), k • |ε| < ↑N
k N : ℕ
h : ∀ (k : ℕ), k • |ε| < ↑N
⊢ N • k • |ε| < N • 1
Tactic:
rw [← mul_nsmul, nsmul_one]
State after:
R : Type u_1
inst✝ : LinearOrderedRing R
ε : R
x✝ : ∃ N, ∀ (k : ℕ), k • |ε| < ↑N
k N : ℕ
h : ∀ (k : ℕ), k • |ε| < ↑N
⊢ (k * N) • |ε| < ↑N

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε : R
x✝ : ∃ N, ∀ (k : ℕ), k • |ε| < ↑N
k N : ℕ
h : ∀ (k : ℕ), k • |ε| < ↑N
⊢ (k * N) • |ε| < ↑N
Tactic:
exact h _
State after:
no goals