awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
hS_finite : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
h_right :
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
⊢ Tendsto.{0, u_3} (β := F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    atTop
    (𝓝
      (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))

Tactic:
have h_left : Tendsto (fun i => ∫ x in S i ∩ s, condExpL1CLM F' hm μ f x ∂μ) atTop
      (𝓝 (∫ x in s, condExpL1CLM F' hm μ f x ∂μ)) := by
    have h := tendsto_setIntegral_of_monotone (fun i => (hS_meas0 i).inter (hm s hs)) h_mono
      (L1.integrable_coeFn (condExpL1CLM F' hm μ f)).integrableOn
    rwa [← hs_eq] at h
-- 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)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
hS_finite : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
h_right :
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
h_left :
  Tendsto.{0, u_3} (β := F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    atTop
    (𝓝
      (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))
⊢ Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝
      (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))

Tactic:
rw [h_eq_forall] at h_left
-- 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)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
hS_finite : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
h_right :
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
h_left :
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝
      (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ)

Tactic:
tendsto_nhds_unique h_left h_right

Premises used: tendsto_nhds_unique
-- 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)
s : Set α
inst_3 : CompleteSpace F'
f : ↥(Lp F' 1 μ)
hs : MeasurableSet s
S : (i : ℕ) → Set α := spanningSets (μ.trim hm)
hS_meas : ∀ (i : ℕ), MeasurableSet (S i)
hS_meas0 : ∀ (i : ℕ), MeasurableSet (S i)
hs_eq : s = ⋃ (i : ℕ), S i ∩ s
hS_finite : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_mono : Monotone.{0, u_1} (β := Set α) fun (i : ℕ) ↦ S i ∩ s
h_eq_forall :
  Eq.{u_3 + 1} (α := (i : ℕ) → F')
    (fun (i : ℕ) ↦
      ∫ (x : α) in S i ∩ s,
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ
h_right :
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ))
h_left :
  Tendsto.{0, u_3} (β := F') (fun (i : ℕ) ↦ ∫ (x : α) in S i ∩ s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ) atTop
    (𝓝
      (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ))
⊢ Eq.{u_3 + 1} (α := F')
    (∫ (x : α) in s, (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] F') : α → F') x ∂μ)

Tactic:
exact tendsto_nhds_unique h_left h_right

Premises used: tendsto_nhds_unique
-- 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 : ↥(Lp F' 1 μ)
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ

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

Premises used: MeasureTheory.AEEqFun.cast, MeasureTheory.condExpL1CLM, MeasureTheory.Lp.induction, Subtype.val, DFunLike.coe, MeasureTheory.AEStronglyMeasurable, ENNReal.one_ne_top
-- 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 : ↥(Lp F' 1 μ)
refine_1 :
  ∀ (c : F') {s : Set α} (hs : MeasurableSet s)
    (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (fun (f : ↥(Lp F' 1 μ)) ↦
        AEStronglyMeasurable.{u_1, u_3} (β := F')
          (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
      (↑(simpleFunc.indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp F' 1 μ))
refine_2 :
  ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
    Disjoint (Function.support f) (Function.support g) →
      (fun (f : ↥(Lp F' 1 μ)) ↦
            AEStronglyMeasurable.{u_1, u_3} (β := F')
              (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
          (MemLp.toLp f hf) →
        (fun (f : ↥(Lp F' 1 μ)) ↦
              AEStronglyMeasurable.{u_1, u_3} (β := F')
                (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
            (MemLp.toLp g hg) →
          (fun (f : ↥(Lp F' 1 μ)) ↦
              AEStronglyMeasurable.{u_1, u_3} (β := F')
                (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
            (MemLp.toLp f hf + MemLp.toLp g hg)
refine_3 :
  IsClosed (X := ↥(Lp F' 1 μ))
    {f : ↥(Lp F' 1 μ) |
      (fun (f : ↥(Lp F' 1 μ)) ↦
          AEStronglyMeasurable.{u_1, u_3} (β := F')
            (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
        f}
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ

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

Premises used: MeasureTheory.AEEqFun.cast, MeasureTheory.condExpL1CLM, MeasureTheory.Lp.induction, Subtype.val, DFunLike.coe, MeasureTheory.AEStronglyMeasurable, ENNReal.one_ne_top
-- 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 : ↥(Lp F' 1 μ)
c : F'
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) c) : α →ₘ[μ] F') : α → F') μ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
              (↑(simpleFunc.indicatorConst 1 (s := s) hs ⋯ c) : ↥(Lp F' 1 μ))) :
          α →ₘ[μ] F') :
      α → F')
    μ

Tactic:
rw [condExpL1CLM_indicatorConst hs hμs.ne c]

Premises used: MeasureTheory.condExpL1CLM_indicatorConst, LT.lt.ne
-- 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 : ↥(Lp F' 1 μ)
c : F'
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) c) : α →ₘ[μ] F') : α → F') μ

Tactic:
aestronglyMeasurable_condExpInd hs hμs.ne c

Premises used: MeasureTheory.aestronglyMeasurable_condExpInd, LT.lt.ne
-- 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 : ↥(Lp F' 1 μ)
c : F'
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpInd F' hm μ s : (a : F') → ↥(Lp F' 1 μ)) c) : α →ₘ[μ] F') : α → F') μ

Tactic:
exact aestronglyMeasurable_condExpInd hs hμs.ne c

Premises used: MeasureTheory.aestronglyMeasurable_condExpInd, LT.lt.ne
-- 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 : ↥(Lp F' 1 μ)
f g : α → F'
hf : MemLp f 1 μ
hg : MemLp g 1 μ
refine_2 :
  Disjoint (Function.support f) (Function.support g) →
    (fun (f : ↥(Lp F' 1 μ)) ↦
          AEStronglyMeasurable.{u_1, u_3} (β := F')
            (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
        (MemLp.toLp f hf) →
      (fun (f : ↥(Lp F' 1 μ)) ↦
            AEStronglyMeasurable.{u_1, u_3} (β := F')
              (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
          (MemLp.toLp g hg) →
        (fun (f : ↥(Lp F' 1 μ)) ↦
            AEStronglyMeasurable.{u_1, u_3} (β := F')
              (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
          (MemLp.toLp f hf + MemLp.toLp g hg)
⊢ Disjoint (Function.support f) (Function.support g) →
    (fun (f : ↥(Lp F' 1 μ)) ↦
          AEStronglyMeasurable.{u_1, u_3} (β := F')
            (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
        (MemLp.toLp f hf) →
      (fun (f : ↥(Lp F' 1 μ)) ↦
            AEStronglyMeasurable.{u_1, u_3} (β := F')
              (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
          (MemLp.toLp g hg) →
        (fun (f : ↥(Lp F' 1 μ)) ↦
            AEStronglyMeasurable.{u_1, u_3} (β := F')
              (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ)
          (MemLp.toLp f hf + MemLp.toLp g hg)

Tactic:
_
-- 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 : ↥(Lp F' 1 μ)
f g : α → F'
hf : MemLp f 1 μ
hg : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hfm :
  AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf)) : α →ₘ[μ] F') : α → F') μ
hgm :
  AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg)) : α →ₘ[μ] F') : α → F') μ
refine_2 :
  AEStronglyMeasurable
    (↑(↑(HAdd.hAdd (α := ↥(Lp F' 1 μ)) (β := ↥(Lp F' 1 μ))
              ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf) : ↥(Lp F' 1 μ))
              ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg) : ↥(Lp F' 1 μ))) :
          α →ₘ[μ] F') :
      α → F')
    μ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf + MemLp.toLp g hg)) : α →ₘ[μ] F') :
      α → F')
    μ

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

Premises used: MeasureTheory.condExpL1CLM, ContinuousLinearMap.map_add
-- 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 : ↥(Lp F' 1 μ)
f g : α → F'
hf : MemLp f 1 μ
hg : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hfm :
  AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf)) : α →ₘ[μ] F') : α → F') μ
hgm :
  AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg)) : α →ₘ[μ] F') : α → F') μ
⊢ AEStronglyMeasurable
    (↑(↑(HAdd.hAdd (α := ↥(Lp F' 1 μ)) (β := ↥(Lp F' 1 μ))
              ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf) : ↥(Lp F' 1 μ))
              ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg) : ↥(Lp F' 1 μ))) :
          α →ₘ[μ] F') :
      α → F')
    μ

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

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.Lp.coeFn_add, MeasureTheory.AEStronglyMeasurable.add, Filter.EventuallyEq.symm
-- 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 : ↥(Lp F' 1 μ)
f g : α → F'
hf : MemLp f 1 μ
hg : MemLp g 1 μ
h : Disjoint (Function.support f) (Function.support g)
hfm :
  AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf)) : α →ₘ[μ] F') : α → F') μ
hgm :
  AEStronglyMeasurable.{u_1, u_3} (β := F')
    (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg)) : α →ₘ[μ] F') : α → F') μ
⊢ AEStronglyMeasurable
    (↑(↑(HAdd.hAdd (α := ↥(Lp F' 1 μ)) (β := ↥(Lp F' 1 μ))
              ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp f hf) : ↥(Lp F' 1 μ))
              ((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) (MemLp.toLp g hg) : ↥(Lp F' 1 μ))) :
          α →ₘ[μ] F') :
      α → F')
    μ

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

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.Lp.coeFn_add, MeasureTheory.AEStronglyMeasurable.add, Filter.EventuallyEq.symm
-- 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 : ↥(Lp F' 1 μ)
⊢ Eq (α := Set ↥(Lp F' 1 μ))
    {f : ↥(Lp F' 1 μ) |
      AEStronglyMeasurable.{u_1, u_3} (β := F')
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ}
    (Set.preimage (β := ↥(Lp F' 1 μ)) (⇑(condExpL1CLM F' hm μ) : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      {f : ↥(Lp F' 1 μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ})

Tactic:
have : {f : Lp F' 1 μ | AEStronglyMeasurable[m] (condExpL1CLM F' hm μ f) μ} =
        condExpL1CLM F' hm μ ⁻¹' {f | AEStronglyMeasurable[m] f μ} := rfl
-- 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 : ↥(Lp F' 1 μ)
this :
  Eq (α := Set ↥(Lp F' 1 μ))
    {f : ↥(Lp F' 1 μ) |
      AEStronglyMeasurable.{u_1, u_3} (β := F')
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ}
    (Set.preimage (β := ↥(Lp F' 1 μ)) (⇑(condExpL1CLM F' hm μ) : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      {f : ↥(Lp F' 1 μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ})
⊢ IsClosed (X := ↥(Lp F' 1 μ))
    (Set.preimage (β := ↥(Lp F' 1 μ)) (⇑(condExpL1CLM F' hm μ) : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      {f : ↥(Lp F' 1 μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ})

Tactic:
IsClosed.preimage (condExpL1CLM F' hm μ).continuous ?_

Premises used: MeasureTheory.condExpL1CLM, ContinuousLinearMap.continuous, IsClosed.preimage
-- 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 : ↥(Lp F' 1 μ)
this :
  Eq (α := Set ↥(Lp F' 1 μ))
    {f : ↥(Lp F' 1 μ) |
      AEStronglyMeasurable.{u_1, u_3} (β := F')
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ}
    (Set.preimage (β := ↥(Lp F' 1 μ)) (⇑(condExpL1CLM F' hm μ) : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      {f : ↥(Lp F' 1 μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ})
refine_3 : IsClosed (X := ↥(Lp F' 1 μ)) {f : ↥(Lp F' 1 μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ}
⊢ IsClosed (X := ↥(Lp F' 1 μ))
    (Set.preimage (β := ↥(Lp F' 1 μ)) (⇑(condExpL1CLM F' hm μ) : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      {f : ↥(Lp F' 1 μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ})

Tactic:
refine IsClosed.preimage (condExpL1CLM F' hm μ).continuous ?_

Premises used: MeasureTheory.condExpL1CLM, ContinuousLinearMap.continuous, IsClosed.preimage
-- 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 : ↥(Lp F' 1 μ)
this :
  Eq (α := Set ↥(Lp F' 1 μ))
    {f : ↥(Lp F' 1 μ) |
      AEStronglyMeasurable.{u_1, u_3} (β := F')
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ}
    (Set.preimage (β := ↥(Lp F' 1 μ)) (⇑(condExpL1CLM F' hm μ) : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      {f : ↥(Lp F' 1 μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ})
⊢ IsClosed (X := ↥(Lp F' 1 μ)) {f : ↥(Lp F' 1 μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ}

Tactic:
isClosed_aestronglyMeasurable hm

Premises used: MeasureTheory.isClosed_aestronglyMeasurable
-- 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 : ↥(Lp F' 1 μ)
this :
  Eq (α := Set ↥(Lp F' 1 μ))
    {f : ↥(Lp F' 1 μ) |
      AEStronglyMeasurable.{u_1, u_3} (β := F')
        (↑(↑((condExpL1CLM F' hm μ : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ)) f) : α →ₘ[μ] F') : α → F') μ}
    (Set.preimage (β := ↥(Lp F' 1 μ)) (⇑(condExpL1CLM F' hm μ) : (a : ↥(Lp F' 1 μ)) → ↥(Lp F' 1 μ))
      {f : ↥(Lp F' 1 μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ})
⊢ IsClosed (X := ↥(Lp F' 1 μ)) {f : ↥(Lp F' 1 μ) | AEStronglyMeasurable (↑(↑f : α →ₘ[μ] F') : α → F') μ}

Tactic:
exact isClosed_aestronglyMeasurable hm

Premises used: MeasureTheory.isClosed_aestronglyMeasurable
-- 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
⊢ f = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ)) g

Tactic:
simp only [g, LinearIsometryEquiv.symm_apply_apply]

Premises used: LinearIsometryEquiv.symm_apply_apply
-- 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
⊢ f = (LinearIsometryEquiv.symm (lpMeasToLpTrimLie F' ℝ 1 μ hm) : (a : ↥(Lp F' 1 (μ.trim hm))) → ↥(lpMeas F' ℝ m 1 μ)) g

Tactic:
have hfg : f = (lpMeasToLpTrimLie F' ℝ 1 μ hm).symm g := by
    simp only [g, LinearIsometryEquiv.symm_apply_apply]