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

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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
⊢ m + n₁ < m + n₂
Tactic:
have : n₁ + m < n₂ + m := lt_substL_add ‹n₁ < n₂›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n₁ n₂ m : ℕ
x✝ : n₁ < n₂
this : n₁ + m < n₂ + m
⊢ m + n₁ < m + n₂

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

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

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