α : Type ?u.828266
β : Type ?u.828269
a b c d : ℝ≥0∞
r✝ p q r : ℝ≥0
s : ℝ≥0∞
⊢ ↑r * ENNReal.toReal s = r • ENNReal.toReal s
α : Type ?u.828266
β : Type ?u.828269
a b c d : ℝ≥0∞
r✝ p q r : ℝ≥0
s : ℝ≥0∞
⊢ ENNReal.toReal (r • s) = r • ENNReal.toReal s
rw [ENNReal.smul_def, smul_eq_mul, toReal_mul, coe_toReal]
no goals
α : Type ?u.828266
β : Type ?u.828269
a b c d : ℝ≥0∞
r✝ p q r : ℝ≥0
s : ℝ≥0∞
⊢ ↑r * ENNReal.toReal s = r • ENNReal.toReal s
rfl