no goals
α : Type u_1
E : Type u_2
F : Type ?u.1268526
𝕜 : Type ?u.1268529
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1271220
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
inst✝ : IsFiniteMeasure μ
f : α → E
C : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ (∫ (x : α), C ∂μ) = C * ENNReal.toReal (↑↑μ univ)
rw [integral_const, smul_eq_mul, mul_comm]