case ofNat
α : Type ?u.359170
β : Type ?u.359173
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.ofNat n) = ↑r ^ Int.ofNat n

case negSucc
α : Type ?u.359170
β : Type ?u.359173
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n
α : Type ?u.359170
β : Type ?u.359173
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : r ≠ 0
n : ℤ
⊢ ↑(r ^ n) = ↑r ^ n
cases' n with n n
no goals
case ofNat
α : Type ?u.359170
β : Type ?u.359173
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.ofNat n) = ↑r ^ Int.ofNat n
simp only [Int.ofNat_eq_coe, coe_pow, zpow_ofNat]
case negSucc
α : Type ?u.359170
β : Type ?u.359173
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : r ≠ 0
n : ℕ
this : r ^ Nat.succ n ≠ 0
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n
case negSucc
α : Type ?u.359170
β : Type ?u.359173
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n
have : r ^ n.succ ≠ 0 := pow_ne_zero (n + 1) hr
no goals
case negSucc
α : Type ?u.359170
β : Type ?u.359173
a b c d : ℝ≥0∞
r p q : ℝ≥0
hr : r ≠ 0
n : ℕ
this : r ^ Nat.succ n ≠ 0
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n
simp only [zpow_negSucc, coe_inv this, coe_pow]