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

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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
⊢ n < m ∨ n ≃ m
Tactic:
have ⟨d, (h : n + d ≃ m)⟩ := le_defn.mp ‹n ≤ m›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
h : n + d ≃ m
⊢ n < m ∨ n ≃ m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
h : n + d ≃ m
⊢ n < m ∨ n ≃ m
Tactic:
revert h
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
⊢ n + d ≃ m → n < m ∨ n ≃ m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
⊢ n + d ≃ m → n < m ∨ n ≃ m
Tactic:
apply cases_on (motive := λ d => n + d ≃ m → n < m ∨ n ≃ m) d
State after:
case zero
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
⊢ n + 0 ≃ m → n < m ∨ n ≃ m

case step
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
⊢ ∀ (m_1 : ℕ), n + step m_1 ≃ m → n < m ∨ n ≃ m

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
⊢ n + 0 ≃ m → n < m ∨ n ≃ m
Tactic:
case zero =>
  intro (_ : n + 0 ≃ m)
  apply Or.inr
  show n ≃ m
  calc
    n     ≃ _ := Rel.symm add_zero
    n + 0 ≃ _ := ‹n + 0 ≃ m›
    m     ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝ : n ≤ m
d : ℕ
⊢ ∀ (m_1 : ℕ), n + step m_1 ≃ m → n < m ∨ n ≃ m
Tactic:
case step =>
  intro d (_ : n + step d ≃ m)
  apply Or.inl
  show n < m
  apply lt_step_le.mpr
  show step n ≤ m
  apply le_defn.mpr
  exists d
  show step n + d ≃ m
  calc
    step n + d   ≃ _ := step_add
    step (n + d) ≃ _ := Rel.symm add_step
    n + step d   ≃ _ := ‹n + step d ≃ m›
    m            ≃ _ := Rel.refl
State after:
no goals

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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d : ℕ
x✝ : n + 0 ≃ m
⊢ n < m ∨ n ≃ m
Tactic:
apply Or.inr
State after:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d : ℕ
x✝ : n + 0 ≃ m
⊢ n ≃ m

State before:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d : ℕ
x✝ : n + 0 ≃ m
⊢ n ≃ m
Tactic:
calc
  n     ≃ _ := Rel.symm add_zero
  n + 0 ≃ _ := ‹n + 0 ≃ m›
  m     ≃ _ := Rel.refl
State after:
no goals

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

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d✝ d : ℕ
x✝ : n + step d ≃ m
⊢ n < m ∨ n ≃ m
Tactic:
apply Or.inl
State after:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
x✝¹ : n ≤ m
d✝ d : ℕ
x✝ : n + step d ≃ m
⊢ n < m

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

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

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

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