Theorem: succ_zero_mul_eq_self' (meetings/ex5.lean)

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

⊢ mul (S z, z) = z

case hs

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

State before:
case hz

⊢ mul (S z, z) = z
Tactic:
rw [zmul]
State after:
no goals

State before:
case hs

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

State before:
case hs
x : ↑N0
hi : mul (S z, x) = x
⊢ mul (S z, S x) = S x
Tactic:
rw [smul, hi, splus, zplus]
State after:
no goals