Theorem: zero_plus_x_eq_eq (meetings/ex6.lean)

State before:
⊢ ∀ (x : ↑N0), plus (z, x) = x
Tactic:
apply generic_recursor
State after:
case hz

⊢ plus (z, z) = z

case hs

⊢ ∀ (n : ↑N0), plus (z, n) = n → plus (z, S n) = S n

State before:
case hz

⊢ plus (z, z) = z
Tactic:
exact zplus z
State after:
no goals

State before:
case hs

⊢ ∀ (n : ↑N0), plus (z, n) = n → plus (z, S n) = S n
Tactic:
intros n hi
State after:
case hs
n : ↑N0
hi : plus (z, n) = n
⊢ plus (z, S n) = S n

State before:
case hs
n : ↑N0
hi : plus (z, n) = n
⊢ plus (z, S n) = S n
Tactic:
rw [splus, hi]
State after:
no goals