-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem aestronglyMeasurable_condExpL1CLM (f : α →₁[μ] F') :
    AEStronglyMeasurable[m] (condExpL1CLM F' hm μ f) μ

Proof state:
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
⊢ AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ

Tactic:
refine @Lp.induction _ _ _ _ _ _ _ ENNReal.one_ne_top
  (fun f : α →₁[μ] F' => AEStronglyMeasurable[m] (condExpL1CLM F' hm μ f) μ) ?_ ?_ ?_ f

Result:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
⊢ ∀ (c : F') {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤),
    (fun f => AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ) ↑(simpleFunc.indicatorConst 1 hs ⋯ c)

case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
⊢ ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
    Disjoint (Function.support f) (Function.support g) →
      (fun f => AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ) (MemLp.toLp f hf) →
        (fun f => AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ) (MemLp.toLp g hg) →
          (fun f => AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ) (MemLp.toLp f hf + MemLp.toLp g hg)

case refine_3
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
⊢ IsClosed {f | (fun f => AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ) f}

Proof state:
case refine_3
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
⊢ IsClosed {f | (fun f => AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ) f}

Tactic:
have : {f : Lp F' 1 μ | AEStronglyMeasurable[m] (condExpL1CLM F' hm μ f) μ} =
    condExpL1CLM F' hm μ ⁻¹' {f | AEStronglyMeasurable[m] f μ} := rfl

Result:
case refine_3
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
this :
  {f | AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ} =
    ⇑(condExpL1CLM F' hm μ) ⁻¹' {f | AEStronglyMeasurable (↑↑f) μ}
⊢ IsClosed {f | (fun f => AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ) f}

Proof state:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
⊢ ∀ (c : F') {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤),
    (fun f => AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ) ↑(simpleFunc.indicatorConst 1 hs ⋯ c)

Tactic:
intro c s hs hμs

Result:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
c : F'
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) ↑(simpleFunc.indicatorConst 1 hs ⋯ c))) μ

Proof state:
case refine_3
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
this :
  {f | AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ} =
    ⇑(condExpL1CLM F' hm μ) ⁻¹' {f | AEStronglyMeasurable (↑↑f) μ}
⊢ IsClosed {f | AEStronglyMeasurable (↑↑f) μ}

Tactic:
exact isClosed_aeStronglyMeasurable' hm

Result:
no goals

Proof state:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f✝ : ↥(Lp F' 1 μ)
f g : α → F'
hf : MemLp f 1 μ
hg : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hfm : AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf))) μ
hgm : AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg))) μ
⊢ AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf) + (condExpL1CLM F' hm μ) (MemLp.toLp g hg))) μ

Tactic:
exact (hfm.add hgm).congr (coeFn_add ..).symm

Result:
no goals

Proof state:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
c : F'
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ AEStronglyMeasurable (↑↑((condExpInd F' hm μ s) c)) μ

Tactic:
exact aestronglyMeasurable_condExpInd hs hμs.ne c

Result:
no goals

Proof state:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f✝ : ↥(Lp F' 1 μ)
f g : α → F'
hf : MemLp f 1 μ
hg : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hfm : AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf))) μ
hgm : AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg))) μ
⊢ AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf + MemLp.toLp g hg))) μ

Tactic:
rw [(condExpL1CLM F' hm μ).map_add]

Result:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f✝ : ↥(Lp F' 1 μ)
f g : α → F'
hf : MemLp f 1 μ
hg : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hfm : AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf))) μ
hgm : AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg))) μ
⊢ AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf) + (condExpL1CLM F' hm μ) (MemLp.toLp g hg))) μ

Proof state:
case refine_3
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
this :
  {f | AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ} =
    ⇑(condExpL1CLM F' hm μ) ⁻¹' {f | AEStronglyMeasurable (↑↑f) μ}
⊢ IsClosed {f | (fun f => AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ) f}

Tactic:
rw [this]

Result:
case refine_3
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
this :
  {f | AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ} =
    ⇑(condExpL1CLM F' hm μ) ⁻¹' {f | AEStronglyMeasurable (↑↑f) μ}
⊢ IsClosed (⇑(condExpL1CLM F' hm μ) ⁻¹' {f | AEStronglyMeasurable (↑↑f) μ})