case inl
x : ℝ≥0∞
⊢ x⁻¹ ^ 0 = (x ^ 0)⁻¹

case inr
x : ℝ≥0∞
y : ℝ
hy : y ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
x : ℝ≥0∞
y : ℝ
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
rcases eq_or_ne y 0 with (rfl | hy)
case inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
case inr
x : ℝ≥0∞
y : ℝ
hy : y ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
replace hy := hy.lt_or_lt
case inr.inl
y : ℝ
hy : y < 0 ∨ 0 < y
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹

case inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
case inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
rcases eq_or_ne x 0 with (rfl | h0)
case inr.inr.inl
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : ⊤ ≠ 0
⊢ ⊤⁻¹ ^ y = (⊤ ^ y)⁻¹

case inr.inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ⊤
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
case inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
rcases eq_or_ne x ⊤ with (rfl | h_top)
case inr.inr.inr.h
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ⊤
⊢ x⁻¹ ^ y * x ^ y = 1
case inr.inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ⊤
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
apply ENNReal.eq_inv_of_mul_eq_one_left
no goals
case inr.inr.inr.h
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ⊤
⊢ x⁻¹ ^ y * x ^ y = 1
rw [← mul_rpow_of_ne_zero (ENNReal.inv_ne_zero.2 h_top) h0, ENNReal.inv_mul_cancel h0 h_top,
  one_rpow]
no goals
case inl
x : ℝ≥0∞
⊢ x⁻¹ ^ 0 = (x ^ 0)⁻¹
simp only [rpow_zero, inv_one]
no goals
case inr.inl
y : ℝ
hy : y < 0 ∨ 0 < y
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹
cases hy <;> simp [*]
no goals
case inr.inr.inl
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : ⊤ ≠ 0
⊢ ⊤⁻¹ ^ y = (⊤ ^ y)⁻¹
cases hy <;> simp [*]