Theorem: Lean4Axiomatic.Natural.lt_substL_add (Lean4Axiomatic/Natural/Order.lean)

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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
⊢ n₁ + m < n₂ + m
Tactic:
have (And.intro (_ : n₁ ≤ n₂) (_ : n₁ ≄ n₂)) := lt_defn.mp ‹n₁ < n₂›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
left✝ : n₁ ≤ n₂
right✝ : n₁ ≄ n₂
⊢ n₁ + m < n₂ + m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
left✝ : n₁ ≤ n₂
right✝ : n₁ ≄ n₂
⊢ n₁ + m < n₂ + m
Tactic:
have : n₁ + m ≤ n₂ + m := AA.substL ‹n₁ ≤ n₂›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
left✝ : n₁ ≤ n₂
right✝ : n₁ ≄ n₂
this : n₁ + m ≤ n₂ + m
⊢ n₁ + m < n₂ + m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
left✝ : n₁ ≤ n₂
right✝ : n₁ ≄ n₂
this : n₁ + m ≤ n₂ + m
⊢ n₁ + m < n₂ + m
Tactic:
have : n₁ + m ≄ n₂ + m := mt AA.cancelR ‹n₁ ≄ n₂›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
left✝ : n₁ ≤ n₂
right✝ : n₁ ≄ n₂
this✝ : n₁ + m ≤ n₂ + m
this : n₁ + m ≄ n₂ + m
⊢ n₁ + m < n₂ + m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
left✝ : n₁ ≤ n₂
right✝ : n₁ ≄ n₂
this✝ : n₁ + m ≤ n₂ + m
this : n₁ + m ≄ n₂ + m
⊢ n₁ + m < n₂ + m
Tactic:
have : n₁ + m < n₂ + m :=
  lt_defn.mpr (And.intro ‹n₁ + m ≤ n₂ + m› ‹n₁ + m ≄ n₂ + m›)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
left✝ : n₁ ≤ n₂
right✝ : n₁ ≄ n₂
this✝¹ : n₁ + m ≤ n₂ + m
this✝ : n₁ + m ≄ n₂ + m
this : n₁ + m < n₂ + m
⊢ n₁ + m < n₂ + m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
left✝ : n₁ ≤ n₂
right✝ : n₁ ≄ n₂
this✝¹ : n₁ + m ≤ n₂ + m
this✝ : n₁ + m ≄ n₂ + m
this : n₁ + m < n₂ + m
⊢ n₁ + m < n₂ + m
Tactic:
exact this
State after:
no goals