no goals
α : Type ?u.33209
β : Type ?u.33212
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
hx : x ≠ ⊤
hy : y ≠ ⊤
⊢ ENNReal.toReal x = ENNReal.toReal y ↔ x = y
simp only [ENNReal.toReal, NNReal.coe_eq, toNNReal_eq_toNNReal_iff' hx hy]