Theorem: Lean4Axiomatic.Natural.subst_mul_lt (Lean4Axiomatic/Natural/Multiplication.lean)

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
⊢ Positive m → n₁ < n₂ → n₁ * m < n₂ * m
Tactic:
intro (_ : Positive m) (_ : n₁ < n₂)
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
⊢ n₁ * m < n₂ * m

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
⊢ n₁ * m < n₂ * m
Tactic:
have ⟨(d : ℕ), (_ : Positive d), (_ : n₂ ≃ n₁ + d)⟩ :=
  lt_defn_add.mp ‹n₁ < n₂›
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
d : ℕ
left✝ : Positive d
right✝ : n₂ ≃ n₁ + d
⊢ n₁ * m < n₂ * m

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
d : ℕ
left✝ : Positive d
right✝ : n₂ ≃ n₁ + d
⊢ n₁ * m < n₂ * m
Tactic:
have : n₂ * m ≃ n₁ * m + d * m := calc
  n₂ * m         ≃ _ := AA.substL ‹n₂ ≃ n₁ + d›
  (n₁ + d) * m   ≃ _ := AA.distribR
  n₁ * m + d * m ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
d : ℕ
left✝ : Positive d
right✝ : n₂ ≃ n₁ + d
this : n₂ * m ≃ n₁ * m + d * m
⊢ n₁ * m < n₂ * m

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
d : ℕ
left✝ : Positive d
right✝ : n₂ ≃ n₁ + d
this : n₂ * m ≃ n₁ * m + d * m
⊢ n₁ * m < n₂ * m
Tactic:
have : Positive (d * m) := mul_positive ‹Positive d› ‹Positive m›
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
d : ℕ
left✝ : Positive d
right✝ : n₂ ≃ n₁ + d
this✝ : n₂ * m ≃ n₁ * m + d * m
this : Positive (d * m)
⊢ n₁ * m < n₂ * m

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
d : ℕ
left✝ : Positive d
right✝ : n₂ ≃ n₁ + d
this✝ : n₂ * m ≃ n₁ * m + d * m
this : Positive (d * m)
⊢ n₁ * m < n₂ * m
Tactic:
exact lt_defn_add.mpr
  ⟨d * m, ‹Positive (d * m)›, ‹n₂ * m ≃ n₁ * m + d * m›⟩
State after:
no goals