no goals
α : Type ?u.836623
β : Type ?u.836626
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
⊢ ENNReal.toNNReal (a / b) = ENNReal.toNNReal a / ENNReal.toNNReal b
rw [div_eq_mul_inv, toNNReal_mul, toNNReal_inv, div_eq_mul_inv]