∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] [inst_2 : CompleteSpace F']
  {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m ≤ m0}
  [inst_3 : MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : F'),
  (MeasureTheory.condExpL1CLM F' hm μ) ↑(MeasureTheory.Lp.simpleFunc.indicatorConst 1 hs hμs x) =
    (MeasureTheory.condExpInd F' hm μ s) x