-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
Goal:
α : Type u_1
F' : Type u_3
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst_2 : SigmaFinite (μ.trim hm)
s : Set α
inst_3 : CompleteSpace F'
f_1 : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hf :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
hg :
  Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
refine_2 :
  HAdd.hAdd (α := F')
      (∫ (a : α) in s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
          a ∂μ)
      (∫ (a : α) in s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
          a ∂μ) =
    ∫ (x : α) in s,
      (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x + (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ
refine_2₁ :
  HAdd.hAdd (α := F')
      (∫ (a : α) in s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
          a ∂μ)
      (∫ (a : α) in s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
          a ∂μ) =
    HAdd.hAdd (α := F') (∫ (a : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') a ∂μ)
      (∫ (a : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') a ∂μ)
refine_2₂ :
  HAdd.hAdd (α := F') (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
      (∫ (a : α) in s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
          a ∂μ) =
    HAdd.hAdd (α := F') (∫ (a : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') a ∂μ)
      (∫ (a : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') a ∂μ)
refine_2₃ refine_2₄ :
  HAdd.hAdd (α := F') (∫ (x : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)
      (∫ (x : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ) =
    HAdd.hAdd (α := F') (∫ (a : α) in s, (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') a ∂μ)
      (∫ (a : α) in s, (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') a ∂μ)
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s,
      HAdd.hAdd (α := F')
        ((↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf_Lp)) : α →ₘ[μ] F') : α → F')
          x)
        ((↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg_Lp)) : α →ₘ[μ] F') : α → F')
          x) ∂μ)
    (∫ (x : α) in s,
      (↑(↑(MemLp.toLp f hf_Lp) : α →ₘ[μ] F') : α → F') x + (↑(↑(MemLp.toLp g hg_Lp) : α →ₘ[μ] F') : α → F') x ∂μ)

Tactic:
rw [integral_add (L1.integrable_coeFn _).integrableOn (L1.integrable_coeFn _).integrableOn,
      integral_add (L1.integrable_coeFn _).integrableOn (L1.integrable_coeFn _).integrableOn, hf,
      hg]

Premises used: MeasureTheory.L1.integrable_coeFn, MeasureTheory.Integrable.integrableOn, MeasureTheory.integral_add