-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst_5 : RCLike 𝕜'
inst_6 : NormedAddCommGroup E''
inst_7 : InnerProductSpace 𝕜' E''
inst_8 : CompleteSpace E''
inst_9 : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  Eq.{u_8 + 1} (α := E'')
    (∫ (x : α) in s,
      (↑(↑(↑((condExpL2 E'' 𝕜' hm : (a : ↥(Lp E'' 2 μ)) → ↥(lpMeas E'' 𝕜' m 2 μ)) (T.compLp f)) : ↥(Lp E'' 2 μ)) :
              α →ₘ[μ] E'') :
          α → E'')
        x ∂μ)
    (∫ (x : α) in s,
      (T : (a : E') → E'')
        ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
            α → E')
          x) ∂μ)
refine_1₁ :
  Eq.{u_8 + 1} (α := E'')
    (∫ (x : α) in s,
        (↑(↑(↑((condExpL2 E'' 𝕜' hm : (a : ↥(Lp E'' 2 μ)) → ↥(lpMeas E'' 𝕜' m 2 μ)) (T.compLp f)) : ↥(Lp E'' 2 μ)) :
                α →ₘ[μ] E'') :
            α → E'')
          x ∂μ :
      E'')
    ((T : (a : E') → E'')
        (∫ (x : α) in s,
          (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
              α → E')
            x ∂μ) :
      E'')
refine_1₂ :
  Eq.{u_8 + 1} (α := E'')
    (∫ (x : α) in s,
        (↑(↑(↑((condExpL2 E'' 𝕜' hm : (a : ↥(Lp E'' 2 μ)) → ↥(lpMeas E'' 𝕜' m 2 μ)) (T.compLp f)) : ↥(Lp E'' 2 μ)) :
                α →ₘ[μ] E'') :
            α → E'')
          x ∂μ :
      E'')
    ((T : (a : E') → E'') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) : E'')
refine_1₃ :
  Eq.{u_8 + 1} (α := E'') (∫ (x : α) in s, (↑(↑(T.compLp f) : α →ₘ[μ] E'') : α → E'') x ∂μ : E'')
    ((T : (a : E') → E'') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) : E'')
refine_1₄ :
  Eq.{u_8 + 1} (α := E'') (∫ (x : α) in s, (T : (a : E') → E'') ((↑(↑f : α →ₘ[μ] E') : α → E') x) ∂μ : E'')
    ((T : (a : E') → E'') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) : E'')
refine_1₅ refine_1₆ :
  Eq.{u_8 + 1} (α := E'') ((T : (a : E') → E'') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) : E'')
    ((T : (a : E') → E'') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) : E'')
⊢ Eq.{u_8 + 1} (α := E'')
    (∫ (x : α) in s,
      (↑(↑(↑((condExpL2 E'' 𝕜' hm : (a : ↥(Lp E'' 2 μ)) → ↥(lpMeas E'' 𝕜' m 2 μ)) (T.compLp f)) : ↥(Lp E'' 2 μ)) :
              α →ₘ[μ] E'') :
          α → E'')
        x ∂μ)
    (∫ (x : α) in s,
      (↑(↑(T.compLp (↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ))) :
              α →ₘ[μ] E'') :
          α → E'')
        x ∂μ)

Tactic:
rw [T.setIntegral_compLp _ (hm s hs),
      T.integral_comp_comm
        (integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs.ne),
      integral_condExpL2_eq hm f hs hμs.ne,
      integral_condExpL2_eq hm (T.compLp f) hs hμs.ne, T.setIntegral_compLp _ (hm s hs),
      T.integral_comp_comm
        (integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs.ne)]

Premises used: fact_one_le_two_ennreal, MeasureTheory.integral_condExpL2_eq, ContinuousLinearMap.setIntegral_compLp, MeasureTheory.integrableOn_Lp_of_measure_ne_top, ContinuousLinearMap.compLp, Fact.elim, ContinuousLinearMap.integral_comp_comm, LT.lt.ne