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

State before:
a m n : Nat
⊢ (a ^ m) ^ n = a ^ (m * n)
Tactic:
induction n with
| zero => rw [pow_zero, mul_zero, pow_zero]
| succ n' ih => rw [pow_succ, ih, mul_succ, pow_add]
State after:
no goals

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

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