α : Type u_1
E : Type u_2
F : Type ?u.423076
𝕜 : Type ?u.423079
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ↑L1.integralCLM ↑f = MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)
α : Type u_1
E : Type u_2
F : Type ?u.423076
𝕜 : Type ?u.423079
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ simpleFunc E 1 μ }
⊢ L1.integral ↑f = integral f
simp only [integral, L1.integral]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.423076
𝕜 : Type ?u.423079
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
inst✝² : SMulCommClass ℝ 𝕜 E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ↑L1.integralCLM ↑f = MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)
exact setToL1_eq_setToL1SCLM (dominatedFinMeasAdditive_weightedSMul μ) f