-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 (goal)
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)
h : Disjoint (Function.support f) (Function.support g)
hf_eq :
  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 μ))
            (MemLp.toLp f hf)) :
        ↥(Lp F' 1 μ)))
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
          (MemLp.toLp f hf)) :
      ↥(Lp F' 1 μ))
hg_eq :
  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 μ))
            (MemLp.toLp g hg)) :
        ↥(Lp F' 1 μ)))
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
          (MemLp.toLp g hg)) :
      ↥(Lp F' 1 μ))
refine_2 :
  HAdd.hAdd (α := ↥(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 μ))
              (MemLp.toLp f hf)) :
          ↥(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 μ))
              (MemLp.toLp g hg)) :
          ↥(Lp F' 1 μ))) =
    HAdd.hAdd (α := ↥(Lp F' 1 μ))
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
              (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
            (MemLp.toLp f hf)) :
        ↥(Lp F' 1 μ))
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
              (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
            (MemLp.toLp g hg)) :
        ↥(Lp F' 1 μ))
⊢ (condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      (HAdd.hAdd (α := ↥(Lp F' 1 μ))
        (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
              (MemLp.toLp f hf)) :
          ↥(Lp F' 1 μ))
        (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
              (MemLp.toLp g hg)) :
          ↥(Lp F' 1 μ))) =
    HAdd.hAdd (α := ↥(Lp F' 1 μ))
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
              (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
            (MemLp.toLp f hf)) :
        ↥(Lp F' 1 μ))
      (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
              (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
            (MemLp.toLp g hg)) :
        ↥(Lp F' 1 μ))
have refine_2₁ : HAdd.hAdd (α := ↥(Lp F' 1 μ))
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
          (MemLp.toLp f hf)) :
      ↥(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 μ))
            (MemLp.toLp g hg)) :
        ↥(Lp F' 1 μ))) =
  HAdd.hAdd (α := ↥(Lp F' 1 μ))
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
          (MemLp.toLp f hf)) :
      ↥(Lp F' 1 μ))
    (↑((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
          (MemLp.toLp g hg)) :
      ↥(Lp F' 1 μ))
Tactic: rw [map_add, hf_eq, hg_eq]