Theorem: plus_comm (meetings/ex6.lean)

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

⊢ ∀ (b : ↑N0), plus (z, b) = plus (b, z)

case hs

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

State before:
case hz

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

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

State before:
case hs

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

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

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