no goals
α : Type ?u.806647
β : Type ?u.806650
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q
rw [ENNReal.ofReal, ENNReal.ofReal, coe_eq_coe, Real.toNNReal_eq_toNNReal_iff hp hq]