no goals
α : Type ?u.32519
β : Type ?u.32522
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
⊢ ENNReal.toReal x = ENNReal.toReal y ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0
simp only [ENNReal.toReal, NNReal.coe_eq, toNNReal_eq_toNNReal_iff]