no goals
α : Type ?u.32929
β : Type ?u.32932
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
hx : x ≠ ⊤
hy : y ≠ ⊤
⊢ ENNReal.toNNReal x = ENNReal.toNNReal y ↔ x = y
simp only [ENNReal.toNNReal_eq_toNNReal_iff x y, hx, hy, and_false, false_and, or_false]