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

State before:
a m n : Nat
⊢ a ^ (m + n) = a ^ m * a ^ n
Tactic:
induction n with
| zero => rw [add_zero, pow_zero, mul_one]
| succ n' ih =>
  rw [add_succ, pow_succ, pow_succ, ih, mul_assoc]
State after:
no goals

State before:
case zero
a m : Nat
⊢ a ^ (m + zero) = a ^ m * a ^ zero
Tactic:
rw [add_zero, pow_zero, mul_one]
State after:
no goals

State before:
case succ
a m n' : Nat
ih : a ^ (m + n') = a ^ m * a ^ n'
⊢ a ^ (m + succ n') = a ^ m * a ^ succ n'
Tactic:
rw [add_succ, pow_succ, pow_succ, ih, mul_assoc]
State after:
no goals