Theorem: Pos.pow_mul' (Extra/Pos/Lemmas.lean)

State before:
x : Pos
y z : Nat
⊢ x ^ (y * z) = (x ^ z) ^ y
Tactic:
by_toNat
State after:
x : Pos
y z : Nat
⊢ x.toNat ^ (y * z) = (x.toNat ^ z) ^ y

State before:
x : Pos
y z : Nat
⊢ x.toNat ^ (y * z) = (x.toNat ^ z) ^ y
Tactic:
exact Nat.pow_mul' ..
State after:
no goals