-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
hm : m ≤ mΩ
f : SimpleFunc Ω F
g : Ω → E
hg : Integrable g μ
this :
  ∀ (s : Set Ω) (c : F) (f : Ω → E),
    Eq (α := (ω : Ω) → G)
      (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (s.indicator (Function.const Ω c) ω) : E →L[ℝ] G) : (a : E) → G) (f ω))
      (s.indicator fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) c : E →L[ℝ] G) : (a : E) → G) (f ω))
g₁ g₂ : SimpleFunc Ω F
h :
  Disjoint.{u_1} (α := Set Ω) (Function.support.{u_1, u_3} (M := F) (⇑g₁ : (a : Ω) → F))
    (Function.support.{u_1, u_3} (M := F) (⇑g₂ : (a : Ω) → F))
h_eq₁ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₁
h_eq₂ :
  (fun (f : SimpleFunc Ω F) ↦
      EventuallyEq.{u_1, u_4} (β := G) (ae μ)
        μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
        fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((f : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    g₂
h_add : (⇑(g₁ + g₂) : (a : Ω) → F) = HAdd.hAdd (α := (a : Ω) → F) (⇑g₁ : (a : Ω) → F) (⇑g₂ : (a : Ω) → F)
ω :
  μ[fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) (HAdd.hAdd (α := F) (β := F) ((g₁ : (a : Ω) → F) ω : F) ((g₂ : (a : Ω) → F) ω : F)) :
            E →L[ℝ] G) :
          (a : E) → G)
        (g ω) |
      m] =ᶠ[ae μ]
    HAdd.hAdd (α := Ω → G)
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
      μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
ω₁ :
  EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (fun (ω : Ω) ↦
      HAdd.hAdd (α := G) (β := G)
        ((((B : (a : F) → E →L[ℝ] G) ((g₁ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G)
        ((((B : (a : F) → E →L[ℝ] G) ((g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ + g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ + g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) ((g₁ + g₂ : (a : Ω) → F) ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

Tactic:
calc
      μ[fun ω ↦ B (g₁ ω + g₂ ω) (g ω) | m] =ᵐ[μ]
          μ[fun ω ↦ B (g₁ ω) (g ω) | m] + μ[fun ω ↦ B (g₂ ω) (g ω) | m] := by
        simp_rw [B.map_add]
        obtain ⟨C₁, hC₁⟩ := @SimpleFunc.exists_forall_norm_le _ _ m _ g₁
        obtain ⟨C₂, hC₂⟩ := @SimpleFunc.exists_forall_norm_le _ _ m _ g₂
        exact condExp_add
          (B.integrable_of_bilin_of_bdd_left C₁ (g₁.stronglyMeasurable.mono hm).aestronglyMeasurable
            (ae_of_all _ hC₁) hg)
          (B.integrable_of_bilin_of_bdd_left C₂ (g₂.stronglyMeasurable.mono hm).aestronglyMeasurable
            (ae_of_all _ hC₂) hg) m
      _ =ᵐ[μ] fun ω ↦ B (g₁ ω) (μ[g | m] ω) + B (g₂ ω) (μ[g | m] ω) := EventuallyEq.add h_eq₁ h_eq₂
      _ =ᵐ[μ] fun ω ↦ B ((g₁ + g₂) ω) (μ[g | m] ω) := by simp

Premises used: MeasureTheory.condExp, HAdd.hAdd, Filter.EventuallyEq.add, DFunLike.coe