-- 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)
inst_3 : CompleteSpace F'
f_1 : ↥(lpMeas F' ℝ m 1 μ)
g_1 : ↥(Lp F' 1 (μ.trim hm)) :=
  (lpMeasToLpTrimLie F' ℝ 1 μ hm : (a : ↥(lpMeas F' ℝ m 1 μ)) → ↥(Lp F' 1 (μ.trim hm))) f_1
hfg :
  f_1 =
    (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ)) g_1
f g : α → F'
hf : MemLp f 1 (μ.trim hm)
hg : MemLp g 1 (μ.trim hm)
refine_2 :
  Disjoint (Function.support f) (Function.support g) →
    (fun (g : ↥(Lp F' 1 (μ.trim hm))) ↦
          Eq (α := ↥(Lp F' 1 μ))
            ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
              (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                      (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                    g) :
                ↥(Lp F' 1 μ)))
            (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                    (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                  g) :
              ↥(Lp F' 1 μ)))
        (MemLp.toLp f hf) →
      (fun (g : ↥(Lp F' 1 (μ.trim hm))) ↦
            Eq (α := ↥(Lp F' 1 μ))
              ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
                (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                        (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                      g) :
                  ↥(Lp F' 1 μ)))
              (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                      (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                    g) :
                ↥(Lp F' 1 μ)))
          (MemLp.toLp g hg) →
        (fun (g : ↥(Lp F' 1 (μ.trim hm))) ↦
            Eq (α := ↥(Lp F' 1 μ))
              ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
                (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                        (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                      g) :
                  ↥(Lp F' 1 μ)))
              (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                      (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                    g) :
                ↥(Lp F' 1 μ)))
          (MemLp.toLp f hf + MemLp.toLp g hg)
⊢ Disjoint (Function.support f) (Function.support g) →
    (fun (g : ↥(Lp F' 1 (μ.trim hm))) ↦
          Eq (α := ↥(Lp F' 1 μ))
            ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
              (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                      (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                    g) :
                ↥(Lp F' 1 μ)))
            (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                    (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                  g) :
              ↥(Lp F' 1 μ)))
        (MemLp.toLp f hf) →
      (fun (g : ↥(Lp F' 1 (μ.trim hm))) ↦
            Eq (α := ↥(Lp F' 1 μ))
              ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
                (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                        (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                      g) :
                  ↥(Lp F' 1 μ)))
              (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                      (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                    g) :
                ↥(Lp F' 1 μ)))
          (MemLp.toLp g hg) →
        (fun (g : ↥(Lp F' 1 (μ.trim hm))) ↦
            Eq (α := ↥(Lp F' 1 μ))
              ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
                (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                        (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                      g) :
                  ↥(Lp F' 1 μ)))
              (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                      (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                    g) :
                ↥(Lp F' 1 μ)))
          (MemLp.toLp f hf + MemLp.toLp g hg)

Tactic:
_