α : Type u_1
β : Type ?u.857846
γ : Type ?u.857849
δ : Type ?u.857852
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x in SimpleFunc.range (pair f g), (x.fst + x.snd) * ↑↑μ (↑(pair f g) ⁻¹' {x}) =
    ∑ x in SimpleFunc.range (pair f g), (x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x}) + x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x}))
α : Type u_1
β : Type ?u.857846
γ : Type ?u.857849
δ : Type ?u.857852
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ lintegral (f + g) μ =
    ∑ x in SimpleFunc.range (pair f g), (x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x}) + x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x}))
rw [add_eq_map₂, map_lintegral]
no goals
α : Type u_1
β : Type ?u.857846
γ : Type ?u.857849
δ : Type ?u.857852
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x in SimpleFunc.range (pair f g), (x.fst + x.snd) * ↑↑μ (↑(pair f g) ⁻¹' {x}) =
    ∑ x in SimpleFunc.range (pair f g), (x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x}) + x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x}))
exact Finset.sum_congr rfl fun a _ => add_mul _ _ _
no goals
α : Type u_1
β : Type ?u.857846
γ : Type ?u.857849
δ : Type ?u.857852
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x in SimpleFunc.range (pair f g), (x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x}) + x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x})) =
    ∑ x in SimpleFunc.range (pair f g), x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x}) +
      ∑ x in SimpleFunc.range (pair f g), x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x})
rw [Finset.sum_add_distrib]
no goals
α : Type u_1
β : Type ?u.857846
γ : Type ?u.857849
δ : Type ?u.857852
m : MeasurableSpace α
μ ν : Measure α
f g : α →ₛ ℝ≥0∞
⊢ ∑ x in SimpleFunc.range (pair f g), x.fst * ↑↑μ (↑(pair f g) ⁻¹' {x}) +
      ∑ x in SimpleFunc.range (pair f g), x.snd * ↑↑μ (↑(pair f g) ⁻¹' {x}) =
    lintegral (map Prod.fst (pair f g)) μ + lintegral (map Prod.snd (pair f g)) μ
rw [map_lintegral, map_lintegral]