no goals
x : ℝ≥0
⊢ ↑(↑x * ⊤) = ↑↑x * ↑⊤
rw [mul_comm, coe_ennreal_top_mul, EReal.mul_comm, coe_ennreal_top]
no goals
x y : ℝ≥0
⊢ ↑(↑x * ↑y) = ↑↑x * ↑↑y
simp only [← ENNReal.coe_mul, coe_nnreal_eq_coe_real, NNReal.coe_mul, EReal.coe_mul]