α : Type u_1
β : Type ?u.884606
γ : Type ?u.884609
δ : Type ?u.884612
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
ι : Type u_2
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
⊢ (∑' (x : { x // x ∈ SimpleFunc.range f }) (i : ι), ↑x * ↑↑(μ i) (↑f ⁻¹' {↑x})) =
    ∑' (i : ι) (x : { x // x ∈ SimpleFunc.range f }), ↑x * ↑↑(μ i) (↑f ⁻¹' {↑x})
α : Type u_1
β : Type ?u.884606
γ : Type ?u.884609
δ : Type ?u.884612
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
ι : Type u_2
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
⊢ lintegral f (Measure.sum μ) = ∑' (i : ι), lintegral f (μ i)
simp only [lintegral, Measure.sum_apply, f.measurableSet_preimage, ← Finset.tsum_subtype, ←
  ENNReal.tsum_mul_left]
no goals
α : Type u_1
β : Type ?u.884606
γ : Type ?u.884609
δ : Type ?u.884612
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
ι : Type u_2
f : α →ₛ ℝ≥0∞
μ : ι → Measure α
⊢ (∑' (x : { x // x ∈ SimpleFunc.range f }) (i : ι), ↑x * ↑↑(μ i) (↑f ⁻¹' {↑x})) =
    ∑' (i : ι) (x : { x // x ∈ SimpleFunc.range f }), ↑x * ↑↑(μ i) (↑f ⁻¹' {↑x})
apply ENNReal.tsum_comm