case none
y : ℝ
⊢ none ^ y = 0 ↔ none = 0 ∧ 0 < y ∨ none = ⊤ ∧ y < 0

case some
y : ℝ
x : ℝ≥0
⊢ Option.some x ^ y = 0 ↔ Option.some x = 0 ∧ 0 < y ∨ Option.some x = ⊤ ∧ y < 0
x : ℝ≥0∞
y : ℝ
⊢ x ^ y = 0 ↔ x = 0 ∧ 0 < y ∨ x = ⊤ ∧ y < 0
cases' x with x
no goals
case none
y : ℝ
⊢ none ^ y = 0 ↔ none = 0 ∧ 0 < y ∨ none = ⊤ ∧ y < 0
rcases lt_trichotomy y 0 with (H | H | H) <;>
  simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ Option.some x ^ y = 0 ↔ Option.some x = 0 ∧ 0 < y ∨ Option.some x = ⊤ ∧ y < 0

case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ Option.some x ^ y = 0 ↔ Option.some x = 0 ∧ 0 < y ∨ Option.some x = ⊤ ∧ y < 0
case some
y : ℝ
x : ℝ≥0
⊢ Option.some x ^ y = 0 ↔ Option.some x = 0 ∧ 0 < y ∨ Option.some x = ⊤ ∧ y < 0
by_cases h : x = 0
no goals
case pos
y : ℝ
x : ℝ≥0
h : x = 0
⊢ Option.some x ^ y = 0 ↔ Option.some x = 0 ∧ 0 < y ∨ Option.some x = ⊤ ∧ y < 0
rcases lt_trichotomy y 0 with (H | H | H) <;>
  simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]
no goals
case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ Option.some x ^ y = 0 ↔ Option.some x = 0 ∧ 0 < y ∨ Option.some x = ⊤ ∧ y < 0
simp [coe_rpow_of_ne_zero h, h]