no goals
α : Type ?u.223062
β : Type ?u.223065
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ : ℝ≥0∞
⊢ (x✝ ^ 0)⁻¹ = x✝⁻¹ ^ 0
simp only [pow_zero, inv_one]
no goals
α : Type ?u.223062
β : Type ?u.223065
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
⊢ (⊤ ^ (n + 1))⁻¹ = ⊤⁻¹ ^ (n + 1)
simp [top_pow]
case inl
α : Type ?u.223062
β : Type ?u.223065
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
⊢ (↑0 ^ (n + 1))⁻¹ = (↑0)⁻¹ ^ (n + 1)

case inr
α : Type ?u.223062
β : Type ?u.223065
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
n : ℕ
ha : a ≠ 0
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)
α : Type ?u.223062
β : Type ?u.223065
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
n : ℕ
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)
rcases eq_or_ne a 0 with (rfl | ha)
no goals
case inl
α : Type ?u.223062
β : Type ?u.223065
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
⊢ (↑0 ^ (n + 1))⁻¹ = (↑0)⁻¹ ^ (n + 1)
simp [top_pow]
case inr
α : Type ?u.223062
β : Type ?u.223065
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)
case inr
α : Type ?u.223062
β : Type ?u.223065
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
n : ℕ
ha : a ≠ 0
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)
have := pow_ne_zero (n + 1) ha
case inr
α : Type ?u.223062
β : Type ?u.223065
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ (a ^ (n + 1))⁻¹ = a⁻¹ ^ (n + 1)
case inr
α : Type ?u.223062
β : Type ?u.223065
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)
norm_cast
no goals
case inr
α : Type ?u.223062
β : Type ?u.223065
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ (a ^ (n + 1))⁻¹ = a⁻¹ ^ (n + 1)
rw [inv_pow]