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

State before:
n : MyNat
⊢ mul zero n = zero
Tactic:
induction' n with n ih
State after:
case zero

⊢ mul zero zero = zero

case succ
n : MyNat
ih : mul zero n = zero
⊢ mul zero (succ n) = zero

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

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

State before:
case zero

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