case none
y : ℝ
⊢ none ^ (-y) = (none ^ y)⁻¹

case some
y : ℝ
x : ℝ≥0
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹
x : ℝ≥0∞
y : ℝ
⊢ x ^ (-y) = (x ^ y)⁻¹
cases' x with x
no goals
case none
y : ℝ
⊢ none ^ (-y) = (none ^ y)⁻¹
rcases lt_trichotomy y 0 with (H | H | H) <;>
  simp [top_rpow_of_pos, top_rpow_of_neg, H, neg_pos.mpr]
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹

case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹
case some
y : ℝ
x : ℝ≥0
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹
by_cases h : x = 0
no goals
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹
rcases lt_trichotomy y 0 with (H | H | H) <;>
  simp [h, zero_rpow_of_pos, zero_rpow_of_neg, H, neg_pos.mpr]
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
A : x ^ y ≠ 0
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹
have A : x ^ y ≠ 0 := by simp [h]
no goals
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
A : x ^ y ≠ 0
⊢ Option.some x ^ (-y) = (Option.some x ^ y)⁻¹
simp [coe_rpow_of_ne_zero h, ← coe_inv A, NNReal.rpow_neg]
no goals
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ x ^ y ≠ 0
simp [h]