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

State before:
n : Nat
⊢ n ≠ succ n
Tactic:
induction n with
| zero => apply zero_ne_succ
| succ n' ih =>
  intro (h : succ n' = succ (succ n'))
  have hn : n' = succ n' := by exact succ_inj h
  exact ih hn
State after:
no goals

State before:
case zero

⊢ zero ≠ succ zero
Tactic:
apply zero_ne_succ
State after:
no goals

State before:
case succ
n' : Nat
ih : n' ≠ succ n'
⊢ succ n' ≠ succ (succ n')
Tactic:
intro (h : succ n' = succ (succ n'))
State after:
case succ
n' : Nat
ih : n' ≠ succ n'
h : succ n' = succ (succ n')
⊢ False

State before:
case succ
n' : Nat
ih : n' ≠ succ n'
h : succ n' = succ (succ n')
⊢ False
Tactic:
have hn : n' = succ n' := by exact succ_inj h
State after:
case succ
n' : Nat
ih : n' ≠ succ n'
h : succ n' = succ (succ n')
hn : n' = succ n'
⊢ False

State before:
case succ
n' : Nat
ih : n' ≠ succ n'
h : succ n' = succ (succ n')
hn : n' = succ n'
⊢ False
Tactic:
exact ih hn
State after:
no goals

State before:
n' : Nat
ih : n' ≠ succ n'
h : succ n' = succ (succ n')
⊢ n' = succ n'
Tactic:
exact succ_inj h
State after:
no goals