x✝ y z x : ℝ
H : x ^ ↑(-1) = x⁻¹
⊢ x ^ (-1) = x⁻¹

case H
x✝ y z x : ℝ
⊢ x ^ ↑(-1) = x⁻¹
x✝ y z x : ℝ
⊢ x ^ (-1) = x⁻¹
suffices H : x ^ ((-1 : ℤ) : ℝ) = x⁻¹
no goals
case H
x✝ y z x : ℝ
⊢ x ^ ↑(-1) = x⁻¹
simp only [rpow_int_cast, zpow_one, zpow_neg]
no goals
x✝ y z x : ℝ
H : x ^ ↑(-1) = x⁻¹
⊢ x ^ (-1) = x⁻¹
rwa [Int.cast_neg, Int.cast_one] at H