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

State before:
t a b : Nat
⊢ t * (a + b) = t * a + t * b
Tactic:
induction b with
| zero =>
  rw [add_zero, mul_zero, add_zero]
| succ b' ih =>
  rw [add_succ, mul_succ, ih, mul_succ, add_assoc]
State after:
no goals

State before:
case zero
t a : Nat
⊢ t * (a + zero) = t * a + t * zero
Tactic:
rw [add_zero, mul_zero, add_zero]
State after:
no goals

State before:
case succ
t a b' : Nat
ih : t * (a + b') = t * a + t * b'
⊢ t * (a + succ b') = t * a + t * succ b'
Tactic:
rw [add_succ, mul_succ, ih, mul_succ, add_assoc]
State after:
no goals