α : Type u_2
E : Type ?u.101804
F : Type u_1
𝕜 : Type ?u.101810
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.101912
F' : Type ?u.101915
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
⊢ ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ↑(weightedSMul μ (↑f ⁻¹' {x})) x =
    ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x
α : Type u_2
E : Type ?u.101804
F : Type u_1
𝕜 : Type ?u.101810
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.101912
F' : Type ?u.101915
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
⊢ integral μ f = ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x
rw [integral_def, setToSimpleFunc_eq_sum_filter]
α : Type u_2
E : Type ?u.101804
F : Type u_1
𝕜 : Type ?u.101810
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.101912
F' : Type ?u.101915
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
⊢ ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x =
    ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x
α : Type u_2
E : Type ?u.101804
F : Type u_1
𝕜 : Type ?u.101810
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.101912
F' : Type ?u.101915
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
⊢ ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ↑(weightedSMul μ (↑f ⁻¹' {x})) x =
    ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x
simp_rw [weightedSMul_apply]
no goals
α : Type u_2
E : Type ?u.101804
F : Type u_1
𝕜 : Type ?u.101810
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
p : ℝ≥0∞
G : Type ?u.101912
F' : Type ?u.101915
inst✝³ : NormedAddCommGroup G
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m✝ : MeasurableSpace α
μ✝ : Measure α
inst✝ : DecidablePred fun x => x ≠ 0
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
⊢ ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x =
    ∑ x in filter (fun x => x ≠ 0) (SimpleFunc.range f), ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x
congr