Theorem: Nat.pow_assoc (GMLInit/Data/Nat/Pow.lean)

State before:
x y z : Nat
⊢ (x ^ y) ^ z = x ^ (y * z)
Tactic:
induction z with
| zero => rw [Nat.pow_zero, Nat.mul_zero, Nat.pow_zero]
| succ z H => rw [Nat.pow_succ, Nat.mul_succ, Nat.pow_add, H]
State after:
no goals

State before:
case zero
x y : Nat
⊢ (x ^ y) ^ 0 = x ^ (y * 0)
Tactic:
rw [Nat.pow_zero, Nat.mul_zero, Nat.pow_zero]
State after:
no goals

State before:
case succ
x y z : Nat
H : (x ^ y) ^ z = x ^ (y * z)
⊢ (x ^ y) ^ (z + 1) = x ^ (y * (z + 1))
Tactic:
rw [Nat.pow_succ, Nat.mul_succ, Nat.pow_add, H]
State after:
no goals