-- 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)
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 :
  (condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      (↑(HAdd.hAdd (α := ↥(lpMeas F' ℝ m 1 μ)) (β := ↥(lpMeas F' ℝ m 1 μ))
            ((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                  (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                (MemLp.toLp f hf) :
              ↥(lpMeas F' ℝ m 1 μ))
            ((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                  (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
                (MemLp.toLp g hg) :
              ↥(lpMeas F' ℝ m 1 μ))) :
        ↥(Lp F' 1 μ)) =
    (↑(HAdd.hAdd (α := ↥(lpMeas F' ℝ m 1 μ)) (β := ↥(lpMeas F' ℝ m 1 μ))
          ((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
              (MemLp.toLp f hf) :
            ↥(lpMeas F' ℝ m 1 μ))
          ((LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) :
                (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ))
              (MemLp.toLp g hg) :
            ↥(lpMeas F' ℝ m 1 μ))) :
      ↥(Lp F' 1 μ))
⊢ 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 + 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 f hf + MemLp.toLp g hg)) :
      ↥(Lp F' 1 μ))

Tactic:
rw [LinearIsometryEquiv.map_add]

Premises used: LinearIsometryEquiv.map_add