no goals
α : Type u_1
E : Type ?u.97756
F : Type u_2
𝕜 : Type ?u.97762
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.97864
F' : Type ?u.97867
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
m : MeasurableSpace α
μ : Measure α
f : α →ₛ F
⊢ integral μ f = ∑ x in SimpleFunc.range f, ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x
simp [integral, setToSimpleFunc, weightedSMul_apply]