Theorem: zero_mul_eq_zero (meetings/ex6.lean)

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

⊢ mul (z, z) = z

case hs

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

State before:
case hz

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

State before:
case hs

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

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