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

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

State before:
case zero
a b : Nat
⊢ (a + b) * zero = a * zero + b * zero
Tactic:
simp
State after:
no goals

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

State before:
case succ
a b t' : Nat
ih : (a + b) * t' = a * t' + b * t'
⊢ a * t' + b * t' + (a + b) = a * t' + a + (b * t' + b)
Tactic:
simp
State after:
no goals