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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n < m ↔ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n < m → ∃ k, Positive k ∧ m ≃ n + k

case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ (∃ k, Positive k ∧ m ≃ n + k) → n < m

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ n < m → ∃ k, Positive k ∧ m ≃ n + k
Tactic:
intro (_ : n < m)
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
⊢ ∃ k, Positive k ∧ m ≃ n + k

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
have : step n ≤ m := lt_step_le.mp ‹n < m›
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
⊢ ∃ k, Positive k ∧ m ≃ n + k

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
have ⟨k, (_ : step n + k ≃ m)⟩ := le_defn.mp ‹step n ≤ m›
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ ∃ k, Positive k ∧ m ≃ n + k

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ ∃ k, Positive k ∧ m ≃ n + k
Tactic:
exists step k
State after:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ Positive (step k) ∧ m ≃ n + step k

State before:
case mp
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ Positive (step k) ∧ m ≃ n + step k
Tactic:
apply And.intro
State after:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ Positive (step k)

case mp.right
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ m ≃ n + step k

State before:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ Positive (step k)
Tactic:
have : step k ≄ 0 := step_neqv_zero
State after:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this✝ : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
this : step k ≄ 0
⊢ Positive (step k)

State before:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this✝ : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
this : step k ≄ 0
⊢ Positive (step k)
Tactic:
have : Positive (step k) := Signed.positive_defn.mpr ‹step k ≄ 0›
State after:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this✝¹ : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
this✝ : step k ≄ 0
this : Positive (step k)
⊢ Positive (step k)

State before:
case mp.left
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this✝¹ : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
this✝ : step k ≄ 0
this : Positive (step k)
⊢ Positive (step k)
Tactic:
exact this
State after:
no goals

State before:
case mp.right
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < m
this : step n ≤ m
k : ℕ
h✝ : step n + k ≃ m
⊢ m ≃ n + step k
Tactic:
calc
  m            ≃ _ := Rel.symm ‹step n + k ≃ m›
  step n + k   ≃ _ := step_add
  step (n + k) ≃ _ := Rel.symm add_step
  n + step k   ≃ _ := Rel.refl
State after:
no goals

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
⊢ (∃ k, Positive k ∧ m ≃ n + k) → n < m
Tactic:
intro ⟨k, (_ : Positive k), (_ : m ≃ n + k)⟩
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ n < m

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ n < m
Tactic:
apply lt_step_le.mpr
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ step n ≤ m

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ step n ≤ m
Tactic:
apply le_defn.mpr
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ ∃ k, step n + k ≃ m

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
⊢ ∃ k, step n + k ≃ m
Tactic:
have ⟨k', (_ : step k' ≃ k)⟩ := positive_step ‹Positive k›
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
k' : ℕ
h✝ : step k' ≃ k
⊢ ∃ k, step n + k ≃ m

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
k' : ℕ
h✝ : step k' ≃ k
⊢ ∃ k, step n + k ≃ m
Tactic:
exists k'
State after:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
k' : ℕ
h✝ : step k' ≃ k
⊢ step n + k' ≃ m

State before:
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k : ℕ
left✝ : Positive k
right✝ : m ≃ n + k
k' : ℕ
h✝ : step k' ≃ k
⊢ step n + k' ≃ m
Tactic:
calc
  step n + k'   ≃ _ := step_add
  step (n + k') ≃ _ := Rel.symm add_step
  n + step k'   ≃ _ := AA.substR ‹step k' ≃ k›
  n + k         ≃ _ := Rel.symm ‹m ≃ n + k›
  m             ≃ _ := Rel.refl
State after:
no goals