x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
⊢ x = 0 ∧ y < 0 ∨ x = ⊤ ∧ 0 < y → x = ⊤
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
⊢ x ^ y = ⊤ → x = ⊤
rw [ENNReal.rpow_eq_top_iff]
case inl
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ y < 0
⊢ x = ⊤

case inr
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = ⊤ ∧ 0 < y
⊢ x = ⊤
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
⊢ x = 0 ∧ y < 0 ∨ x = ⊤ ∧ 0 < y → x = ⊤
rintro (h|h)
case inl.h
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ y < 0
⊢ False
case inl
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ y < 0
⊢ x = ⊤
exfalso
case inl.h
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ ¬y ≥ 0
⊢ False
case inl.h
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ y < 0
⊢ False
rw [lt_iff_not_ge] at h
no goals
case inl.h
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = 0 ∧ ¬y ≥ 0
⊢ False
exact h.right hy0
no goals
case inr
x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
h : x = ⊤ ∧ 0 < y
⊢ x = ⊤
exact h.left