Theorem: ipow_inv (HOLFloat/Common.lean)

State before:
r : ℝ
i : ℕ
⊢ r ^ negOfNat i = (r ^ i)⁻¹
Tactic:
induction i
State after:
case zero
r : ℝ
⊢ r ^ negOfNat Nat.zero = (r ^ Nat.zero)⁻¹

case succ
r : ℝ
n✝ : ℕ
n_ih✝ : r ^ negOfNat n✝ = (r ^ n✝)⁻¹
⊢ r ^ negOfNat (Nat.succ n✝) = (r ^ Nat.succ n✝)⁻¹

State before:
r : ℝ
⊢ r ^ negOfNat Nat.zero = (r ^ Nat.zero)⁻¹
Tactic:
case zero => simp; trivial
State after:
no goals

State before:
r : ℝ
n✝ : ℕ
n_ih✝ : r ^ negOfNat n✝ = (r ^ n✝)⁻¹
⊢ r ^ negOfNat (Nat.succ n✝) = (r ^ Nat.succ n✝)⁻¹
Tactic:
case succ => constructor
State after:
no goals

State before:
r : ℝ
⊢ r ^ negOfNat Nat.zero = (r ^ Nat.zero)⁻¹
Tactic:
simp
State after:
r : ℝ
⊢ r ^ negOfNat 0 = 1

State before:
r : ℝ
⊢ r ^ negOfNat 0 = 1
Tactic:
trivial
State after:
no goals

State before:
r : ℝ
n✝ : ℕ
n_ih✝ : r ^ negOfNat n✝ = (r ^ n✝)⁻¹
⊢ r ^ negOfNat (Nat.succ n✝) = (r ^ Nat.succ n✝)⁻¹
Tactic:
constructor
State after:
no goals