no goals
α : Type ?u.814548
β : Type ?u.814551
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
hp : 0 ≤ p
⊢ ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
simp only [ENNReal.ofReal, ← coe_mul, Real.toNNReal_mul hp]