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

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

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