Theorem: succ_plus_eq_succ_plus (meetings/ex6.lean)

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

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

case hs

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

State before:
case hz

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

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

State before:
case hs

⊢ ∀ (n : ↑N0), (∀ (a : ↑N0), plus (S a, n) = S (plus (a, n))) → ∀ (a : ↑N0), plus (S a, S n) = S (plus (a, S n))
Tactic:
intro b hi a
State after:
case hs
b : ↑N0
hi : ∀ (a : ↑N0), plus (S a, b) = S (plus (a, b))
a : ↑N0
⊢ plus (S a, S b) = S (plus (a, S b))

State before:
case hs
b : ↑N0
hi : ∀ (a : ↑N0), plus (S a, b) = S (plus (a, b))
a : ↑N0
⊢ plus (S a, S b) = S (plus (a, S b))
Tactic:
specialize hi a
State after:
case hs
b a : ↑N0
hi : plus (S a, b) = S (plus (a, b))
⊢ plus (S a, S b) = S (plus (a, S b))

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