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

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

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