α : Type u_1
E : Type u_2
F : Type ?u.1250929
𝕜 : Type ?u.1250932
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.1253623
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α →ₛ E
hfi : Integrable ↑f
⊢ setToSimpleFunc (weightedSMul μ) f = integral μ f
α : Type u_1
E : Type u_2
F : Type ?u.1250929
𝕜 : Type ?u.1250932
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.1253623
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α →ₛ E
hfi : Integrable ↑f
⊢ (∫ (x : α), ↑f x ∂μ) = ∑ x in SimpleFunc.range f, ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x
rw [← f.integral_eq_integral hfi, SimpleFunc.integral, ← SimpleFunc.integral_eq]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.1250929
𝕜 : Type ?u.1250932
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.1253623
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α →ₛ E
hfi : Integrable ↑f
⊢ setToSimpleFunc (weightedSMul μ) f = integral μ f
rfl