-- 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 : ↥(lpMeas F' ℝ m 1 μ)
g : ↥(Lp F' 1 (μ.trim hm)) := (lpMeasToLpTrimLie F' ℝ 1 μ hm : (a : ↥(lpMeas F' ℝ m 1 μ)) → ↥(Lp F' 1 (μ.trim hm))) f
hfg :
  f = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ)) g
refine_1 :
  ∀ (c : F') {s : Set α} (hs : MeasurableSet s)
    (hμs : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (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 μ)))
      (↑(simpleFunc.indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp F' 1 (μ.trim hm)))
refine_2 :
  ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 (μ.trim hm)) (hg : MemLp g 1 (μ.trim hm)),
    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)
refine_3 :
  IsClosed (X := ↥(Lp F' 1 (μ.trim hm)))
    {f : ↥(Lp F' 1 (μ.trim hm)) |
      (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 μ)))
        f}
⊢ 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 μ))

Tactic:
refine @Lp.induction α F' m _ 1 (μ.trim hm) _ ENNReal.coe_ne_top (fun g : α →₁[μ.trim hm] F' =>
    condExpL1CLM F' hm μ ((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g : α →₁[μ] F') =
    ↑((lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g)) ?_ ?_ ?_ g

Premises used: Real, LinearIsometryEquiv.symm, MeasureTheory.lpMeasToLpTrimLie, MeasureTheory.condExpL1CLM, MeasureTheory.Lp.induction, OfNat.ofNat, Subtype.val, Eq, DFunLike.coe, ENNReal.coe_ne_top