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

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

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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < step m
this : step n ≤ step m
⊢ n < m ∨ n ≃ m
Tactic:
have : n ≤ m := AA.inject ‹step n ≤ step m›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < step m
this✝ : step n ≤ step m
this : n ≤ m
⊢ n < m ∨ n ≃ m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n < step m
this✝ : step n ≤ step m
this : n ≤ m
⊢ n < m ∨ n ≃ m
Tactic:
exact le_split ‹n ≤ m›
State after:
no goals