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

State before:
a : Nat
⊢ one * a = a
Tactic:
induction a with
| zero => rw [mul_zero]
| succ a' ih => rw [mul_succ, ih, succ_eq_add_one]
State after:
no goals

State before:
case zero

⊢ one * zero = zero
Tactic:
rw [mul_zero]
State after:
no goals

State before:
case succ
a' : Nat
ih : one * a' = a'
⊢ one * succ a' = succ a'
Tactic:
rw [mul_succ, ih, succ_eq_add_one]
State after:
no goals