Theorem: succ_plus_n_eq_succ_n_plus' (meetings/ex5.lean)

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

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

case hs

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

State before:
case hz

⊢ ∀ (y : ↑N0), plus (S y, z) = S (plus (z, y))
Tactic:
intro y
State after:
case hz
y : ↑N0
⊢ plus (S y, z) = S (plus (z, y))

State before:
case hz
y : ↑N0
⊢ plus (S y, z) = S (plus (z, y))
Tactic:
rw [zplus, zero_plus_x_eq_eq]
State after:
no goals

State before:
case hs

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

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