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

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

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