Theorem: MyNat.le_total (TheoremProvingLean/inductive_types.lean)

State before:
a b : Nat
⊢ a ≤ b ∨ b ≤ a
Tactic:
induction a with
| zero => apply Or.inl; exact (zero_le _)
| succ a' ih =>
  cases ih with
  | inl h =>
    cases h with
    | intro w pw =>
      cases w with
      | zero =>
        apply Or.inr
        exists one
        rw [add_zero] at pw
        rw [← succ_eq_add_one]
        exact succ_eq_succ_iff.mpr (Eq.symm pw)
      | succ w' =>
        apply Or.inl
        exists w'
        rw [add_succ] at pw
        rw [pw, succ_add]
  | inr h =>
    apply Or.inr
    apply le_succ
    assumption
State after:
no goals

State before:
case zero
b : Nat
⊢ zero ≤ b ∨ b ≤ zero
Tactic:
apply Or.inl
State after:
case zero.h
b : Nat
⊢ zero ≤ b

State before:
case zero.h
b : Nat
⊢ zero ≤ b
Tactic:
exact (zero_le _)
State after:
no goals

State before:
case succ
b a' : Nat
ih : a' ≤ b ∨ b ≤ a'
⊢ succ a' ≤ b ∨ b ≤ succ a'
Tactic:
cases ih with
| inl h =>
  cases h with
  | intro w pw =>
    cases w with
    | zero =>
      apply Or.inr
      exists one
      rw [add_zero] at pw
      rw [← succ_eq_add_one]
      exact succ_eq_succ_iff.mpr (Eq.symm pw)
    | succ w' =>
      apply Or.inl
      exists w'
      rw [add_succ] at pw
      rw [pw, succ_add]
| inr h =>
  apply Or.inr
  apply le_succ
  assumption
State after:
no goals

State before:
case succ.inl
b a' : Nat
h : a' ≤ b
⊢ succ a' ≤ b ∨ b ≤ succ a'
Tactic:
cases h with
| intro w pw =>
  cases w with
  | zero =>
    apply Or.inr
    exists one
    rw [add_zero] at pw
    rw [← succ_eq_add_one]
    exact succ_eq_succ_iff.mpr (Eq.symm pw)
  | succ w' =>
    apply Or.inl
    exists w'
    rw [add_succ] at pw
    rw [pw, succ_add]
State after:
no goals

State before:
case succ.inl.intro
b a' w : Nat
pw : b = a' + w
⊢ succ a' ≤ b ∨ b ≤ succ a'
Tactic:
cases w with
| zero =>
  apply Or.inr
  exists one
  rw [add_zero] at pw
  rw [← succ_eq_add_one]
  exact succ_eq_succ_iff.mpr (Eq.symm pw)
| succ w' =>
  apply Or.inl
  exists w'
  rw [add_succ] at pw
  rw [pw, succ_add]
State after:
no goals

State before:
case succ.inl.intro.zero
b a' : Nat
pw : b = a' + zero
⊢ succ a' ≤ b ∨ b ≤ succ a'
Tactic:
apply Or.inr
State after:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a' + zero
⊢ b ≤ succ a'

State before:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a' + zero
⊢ b ≤ succ a'
Tactic:
exists one
State after:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a' + zero
⊢ succ a' = b + one

State before:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a' + zero
⊢ succ a' = b + one
Tactic:
rw [add_zero] at pw
State after:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a'
⊢ succ a' = b + one

State before:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a'
⊢ succ a' = b + one
Tactic:
rw [← succ_eq_add_one]
State after:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a'
⊢ succ a' = succ b

State before:
case succ.inl.intro.zero.h
b a' : Nat
pw : b = a'
⊢ succ a' = succ b
Tactic:
exact succ_eq_succ_iff.mpr (Eq.symm pw)
State after:
no goals

State before:
case succ.inl.intro.succ
b a' w' : Nat
pw : b = a' + succ w'
⊢ succ a' ≤ b ∨ b ≤ succ a'
Tactic:
apply Or.inl
State after:
case succ.inl.intro.succ.h
b a' w' : Nat
pw : b = a' + succ w'
⊢ succ a' ≤ b

State before:
case succ.inl.intro.succ.h
b a' w' : Nat
pw : b = a' + succ w'
⊢ succ a' ≤ b
Tactic:
exists w'
State after:
case succ.inl.intro.succ.h
b a' w' : Nat
pw : b = a' + succ w'
⊢ b = succ a' + w'

State before:
case succ.inl.intro.succ.h
b a' w' : Nat
pw : b = a' + succ w'
⊢ b = succ a' + w'
Tactic:
rw [add_succ] at pw
State after:
case succ.inl.intro.succ.h
b a' w' : Nat
pw : b = succ (a' + w')
⊢ b = succ a' + w'

State before:
case succ.inl.intro.succ.h
b a' w' : Nat
pw : b = succ (a' + w')
⊢ b = succ a' + w'
Tactic:
rw [pw, succ_add]
State after:
no goals

State before:
case succ.inr
b a' : Nat
h : b ≤ a'
⊢ succ a' ≤ b ∨ b ≤ succ a'
Tactic:
apply Or.inr
State after:
case succ.inr.h
b a' : Nat
h : b ≤ a'
⊢ b ≤ succ a'

State before:
case succ.inr.h
b a' : Nat
h : b ≤ a'
⊢ b ≤ succ a'
Tactic:
apply le_succ
State after:
case succ.inr.h.a
b a' : Nat
h : b ≤ a'
⊢ b ≤ a'

State before:
case succ.inr.h.a
b a' : Nat
h : b ≤ a'
⊢ b ≤ a'
Tactic:
assumption
State after:
no goals