Theorem: ipow_inv_neg (HOLFloat/Common.lean)

State before:
r : ℝ
i : ℤ
⊢ r ≠ 0 → r ^ i = (r ^ (-i))⁻¹
Tactic:
cases i with
| ofNat n =>
    intros
    simp_all only [ne_eq, Int.ofNat_eq_coe, zpow_coe_nat, zpow_neg, inv_inv]
| negSucc n =>
    intros
    simp_all only [ne_eq, zpow_negSucc, zpow_neg, inv_inv]
State after:
no goals

State before:
case ofNat
r : ℝ
n : ℕ
⊢ r ≠ 0 → r ^ ofNat n = (r ^ (-ofNat n))⁻¹
Tactic:
intros
State after:
case ofNat
r : ℝ
n : ℕ
a✝ : r ≠ 0
⊢ r ^ ofNat n = (r ^ (-ofNat n))⁻¹

State before:
case ofNat
r : ℝ
n : ℕ
a✝ : r ≠ 0
⊢ r ^ ofNat n = (r ^ (-ofNat n))⁻¹
Tactic:
simp_all only [ne_eq, Int.ofNat_eq_coe, zpow_coe_nat, zpow_neg, inv_inv]
State after:
no goals

State before:
case negSucc
r : ℝ
n : ℕ
⊢ r ≠ 0 → r ^ -[n+1] = (r ^ (- -[n+1]))⁻¹
Tactic:
intros
State after:
case negSucc
r : ℝ
n : ℕ
a✝ : r ≠ 0
⊢ r ^ -[n+1] = (r ^ (- -[n+1]))⁻¹

State before:
case negSucc
r : ℝ
n : ℕ
a✝ : r ≠ 0
⊢ r ^ -[n+1] = (r ^ (- -[n+1]))⁻¹
Tactic:
simp_all only [ne_eq, zpow_negSucc, zpow_neg, inv_inv]
State after:
no goals