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

State before:
a b c : Nat
⊢ a * b * c = a * (b * c)
Tactic:
induction c with
| zero => repeat (rw [mul_zero])
| succ c' ih =>
  repeat (rw [mul_succ])
  rw [mul_add]
  rw [ih]
State after:
no goals

State before:
case zero
a b : Nat
⊢ a * b * zero = a * (b * zero)
Tactic:
repeat (rw [mul_zero])
State after:
no goals

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

State before:
case zero
a b : Nat
⊢ zero = a * zero
Tactic:
rw [mul_zero]
State after:
no goals

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

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

State before:
case succ
a b c' : Nat
ih : a * b * c' = a * (b * c')
⊢ a * b * c' + a * b = a * (b * c') + a * b
Tactic:
rw [ih]
State after:
no goals

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

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