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

State before:
n : Nat
⊢ n ≠ zero → succ (pred n) = n
Tactic:
intro h
State after:
n : Nat
h : n ≠ zero
⊢ succ (pred n) = n

State before:
n : Nat
h : n ≠ zero
⊢ succ (pred n) = n
Tactic:
simp [pred]
State after:
n : Nat
h : n ≠ zero
⊢ succ
      (match n with
      | zero => zero
      | succ k => k) =
    n

State before:
n : Nat
h : n ≠ zero
⊢ succ
      (match n with
      | zero => zero
      | succ k => k) =
    n
Tactic:
split
State after:
case h_1
x✝ : Nat
h : zero ≠ zero
⊢ succ zero = zero

case h_2
x✝ a✝ : Nat
h : succ a✝ ≠ zero
⊢ succ a✝ = succ a✝

State before:
case h_1
x✝ : Nat
h : zero ≠ zero
⊢ succ zero = zero

case h_2
x✝ a✝ : Nat
h : succ a✝ ≠ zero
⊢ succ a✝ = succ a✝
Tactic:
. contradiction
State after:
case h_2
x✝ a✝ : Nat
h : succ a✝ ≠ zero
⊢ succ a✝ = succ a✝

State before:
case h_2
x✝ a✝ : Nat
h : succ a✝ ≠ zero
⊢ succ a✝ = succ a✝
Tactic:
. rfl
State after:
no goals

State before:
case h_1
x✝ : Nat
h : zero ≠ zero
⊢ succ zero = zero
Tactic:
contradiction
State after:
no goals

State before:
case h_2
x✝ a✝ : Nat
h : succ a✝ ≠ zero
⊢ succ a✝ = succ a✝
Tactic:
rfl
State after:
no goals