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

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

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