no goals
α : Type ?u.815667
β : Type ?u.815670
a b c d : ℝ≥0∞
r p q : ℝ≥0
x : ℝ
n : ℕ
⊢ ENNReal.ofReal (n • x) = n • ENNReal.ofReal x
simp only [nsmul_eq_mul, ← ofReal_coe_nat n, ← ofReal_mul n.cast_nonneg]