no goals
α : Type ?u.837272
β : Type ?u.837275
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
⊢ ENNReal.toReal (a / b) = ENNReal.toReal a / ENNReal.toReal b
rw [div_eq_mul_inv, toReal_mul, toReal_inv, div_eq_mul_inv]