Theorem: muls (meetings/ex6.lean)

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

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

case hs

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

State before:
case hz

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

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

State before:
case hs

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

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

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