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

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε₁ ε₂ : R
h₁ : Infinitesimal ε₁
h₂ : Infinitesimal ε₂
k : ℕ
⊢ k • |ε₁ + ε₂| < 1
Tactic:
apply (nsmul_le_nsmul_right (abs_add ε₁ ε₂) k).trans_lt
State after:
R : Type u_1
inst✝ : LinearOrderedRing R
ε₁ ε₂ : R
h₁ : Infinitesimal ε₁
h₂ : Infinitesimal ε₂
k : ℕ
⊢ k • (|ε₁| + |ε₂|) < 1

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε₁ ε₂ : R
h₁ : Infinitesimal ε₁
h₂ : Infinitesimal ε₂
k : ℕ
⊢ k • (|ε₁| + |ε₂|) < 1
Tactic:
apply lt_of_nsmul_lt_nsmul_right 2
State after:
R : Type u_1
inst✝ : LinearOrderedRing R
ε₁ ε₂ : R
h₁ : Infinitesimal ε₁
h₂ : Infinitesimal ε₂
k : ℕ
⊢ 2 • k • (|ε₁| + |ε₂|) < 2 • 1

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε₁ ε₂ : R
h₁ : Infinitesimal ε₁
h₂ : Infinitesimal ε₂
k : ℕ
⊢ 2 • k • (|ε₁| + |ε₂|) < 2 • 1
Tactic:
rw [← mul_nsmul', nsmul_add, two_nsmul]
State after:
R : Type u_1
inst✝ : LinearOrderedRing R
ε₁ ε₂ : R
h₁ : Infinitesimal ε₁
h₂ : Infinitesimal ε₂
k : ℕ
⊢ (2 * k) • |ε₁| + (2 * k) • |ε₂| < 1 + 1

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