Theorem: MyNat.succ_mul (LeanCourse/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean)

State before:
m n : MyNat
⊢ mul (succ m) n = add (mul m n) n
Tactic:
induction' n with n ih
State after:
case zero
m : MyNat
⊢ mul (succ m) zero = add (mul m zero) zero

case succ
m n : MyNat
ih : mul (succ m) n = add (mul m n) n
⊢ mul (succ m) (succ n) = add (mul m (succ n)) (succ n)

State before:
case succ
m n : MyNat
ih : mul (succ m) n = add (mul m n) n
⊢ mul (succ m) (succ n) = add (mul m (succ n)) (succ n)
Tactic:
rw [mul, mul, ih, add_assoc, add_assoc, add_comm n, succ_add]
State after:
case succ
m n : MyNat
ih : mul (succ m) n = add (mul m n) n
⊢ add (mul m n) (succ (add m n)) = add (mul m n) (add m (succ n))

State before:
case succ
m n : MyNat
ih : mul (succ m) n = add (mul m n) n
⊢ add (mul m n) (succ (add m n)) = add (mul m n) (add m (succ n))
Tactic:
rfl
State after:
no goals

State before:
case zero
m : MyNat
⊢ mul (succ m) zero = add (mul m zero) zero
Tactic:
rfl
State after:
no goals