Theorem: Real.rpow_eq_mul_rpow_pred (CvxLean/Lib/Math/Data/Real.lean)

State before:
x y : ℝ
hx : x ≠ 0
⊢ x ^ y = x * x ^ (y - 1)
Tactic:
conv => left; rw [(by ring : y = (y - 1) + 1), rpow_add_one hx, mul_comm]
State after:
no goals

State before:
x y : ℝ
hx : x ≠ 0
⊢ y = y - 1 + 1
Tactic:
ring
State after:
no goals