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

State before:
a : Nat
⊢ ¬succ a ≤ a
Tactic:
intro h
State after:
a : Nat
h : succ a ≤ a
⊢ False

State before:
a : Nat
h : succ a ≤ a
⊢ False
Tactic:
cases h with
| intro w pw =>
  rw [succ_eq_add_one, add_comm_right, add_assoc] at pw
  have hw : w + one = zero := eq_zero_of_add_right_eq_self (Eq.symm pw)
  have _ : one = zero := add_left_eq_zero hw
  contradiction
State after:
no goals

State before:
case intro
a w : Nat
pw : a = succ a + w
⊢ False
Tactic:
rw [succ_eq_add_one, add_comm_right, add_assoc] at pw
State after:
case intro
a w : Nat
pw : a = a + (w + one)
⊢ False

State before:
case intro
a w : Nat
pw : a = a + (w + one)
⊢ False
Tactic:
have hw : w + one = zero := eq_zero_of_add_right_eq_self (Eq.symm pw)
State after:
case intro
a w : Nat
pw : a = a + (w + one)
hw : w + one = zero
⊢ False

State before:
case intro
a w : Nat
pw : a = a + (w + one)
hw : w + one = zero
⊢ False
Tactic:
have _ : one = zero := add_left_eq_zero hw
State after:
case intro
a w : Nat
pw : a = a + (w + one)
hw : w + one = zero
x✝ : one = zero
⊢ False

State before:
case intro
a w : Nat
pw : a = a + (w + one)
hw : w + one = zero
x✝ : one = zero
⊢ False
Tactic:
contradiction
State after:
no goals