Theorem: MyNat.zero_mul (TheoremProvingLean/inductive_types.lean)

State before:
a : Nat
⊢ zero * a = zero
Tactic:
induction a
State after:
case zero

⊢ zero * zero = zero

case succ
a✝ : Nat
a_ih✝ : zero * a✝ = zero
⊢ zero * succ a✝ = zero

State before:
case zero

⊢ zero * zero = zero

case succ
a✝ : Nat
a_ih✝ : zero * a✝ = zero
⊢ zero * succ a✝ = zero
Tactic:
. rfl
State after:
case succ
a✝ : Nat
a_ih✝ : zero * a✝ = zero
⊢ zero * succ a✝ = zero

State before:
case succ
a✝ : Nat
a_ih✝ : zero * a✝ = zero
⊢ zero * succ a✝ = zero
Tactic:
. rw [mul_succ, add_zero]
  assumption
State after:
no goals

State before:
case zero

⊢ zero * zero = zero
Tactic:
rfl
State after:
no goals

State before:
case succ
a✝ : Nat
a_ih✝ : zero * a✝ = zero
⊢ zero * succ a✝ = zero
Tactic:
rw [mul_succ, add_zero]
State after:
case succ
a✝ : Nat
a_ih✝ : zero * a✝ = zero
⊢ zero * a✝ = zero

State before:
case succ
a✝ : Nat
a_ih✝ : zero * a✝ = zero
⊢ zero * a✝ = zero
Tactic:
assumption
State after:
no goals