α : Type u_1
E : Type u_2
F : Type ?u.218028
𝕜 : Type ?u.218031
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖ =
    ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) • ‖x‖
α : Type u_1
E : Type u_2
F : Type ?u.218028
𝕜 : Type ?u.218031
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ‖f‖ = SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))
rw [norm_eq_sum_mul f, (toSimpleFunc f).map_integral norm (SimpleFunc.integrable f) norm_zero]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.218028
𝕜 : Type ?u.218031
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
f : { x // x ∈ simpleFunc E 1 μ }
⊢ ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) * ‖x‖ =
    ∑ x in SimpleFunc.range (toSimpleFunc f), ENNReal.toReal (↑↑μ (↑(toSimpleFunc f) ⁻¹' {x})) • ‖x‖
simp_rw [smul_eq_mul]