awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp :
  MemLp.{u_1, u_7} (ε := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    2 μ
h_eq :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp
              (fun (a : α) ↦
                ⟪c,
                  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
                      α → E)
                    a⟫)
              h_mem_Lp) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
⊢ AEStronglyMeasurable.{u_1, u_7} (β := 𝕜)
    (fun (a : α) ↦
      ⟪c,
        (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
    μ

Tactic:
exact (lpMeas.aestronglyMeasurable _).const_inner

Premises used: MeasureTheory.AEStronglyMeasurable.const_inner, MeasureTheory.lpMeas.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  Eq.{u_3 + 1} (α := E')
    (∫ (a : α) in s,
      HSub.hSub (α := α → E')
        (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
          α → E')
        (↑(↑f : α →ₘ[μ] E') : α → E') a ∂μ)
    0
⊢ Eq.{u_3 + 1} (α := E')
    (∫ (x : α) in s,
      (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') : α → E')
        x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)

Tactic:
rw [← sub_eq_zero, ←
    integral_sub' (integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs)
      (integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs)]

Premises used: fact_one_le_two_ennreal, sub_eq_zero, MeasureTheory.integrableOn_Lp_of_measure_ne_top, MeasureTheory.integral_sub', Fact.elim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E')
    (∫ (a : α) in s,
      HSub.hSub (α := α → E')
        (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
          α → E')
        (↑(↑f : α →ₘ[μ] E') : α → E') a ∂μ)
    0

Tactic:
integral_eq_zero_of_forall_integral_inner_eq_zero 𝕜 _ ?_ ?_

Premises used: integral_eq_zero_of_forall_integral_inner_eq_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  Integrable
    ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') : α → E') -
      (↑(↑f : α →ₘ[μ] E') : α → E'))
    (μ.restrict s)
refine_2 :
  ∀ (c : E'),
    Eq.{u_7 + 1} (α := 𝕜)
      (∫ (x : α) in s,
        ⟪c,
          HSub.hSub (α := α → E')
            (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
              α → E')
            (↑(↑f : α →ₘ[μ] E') : α → E') x⟫ ∂μ)
      0
⊢ Eq.{u_3 + 1} (α := E')
    (∫ (a : α) in s,
      HSub.hSub (α := α → E')
        (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
          α → E')
        (↑(↑f : α →ₘ[μ] E') : α → E') a ∂μ)
    0

Tactic:
refine integral_eq_zero_of_forall_integral_inner_eq_zero 𝕜 _ ?_ ?_

Premises used: integral_eq_zero_of_forall_integral_inner_eq_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  Integrable
    (↑(↑((↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) - f) : α →ₘ[μ] E') :
      α → E')
    (μ.restrict s)
⊢ Integrable
    ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') : α → E') -
      (↑(↑f : α →ₘ[μ] E') : α → E'))
    (μ.restrict s)

Tactic:
rw [integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub (↑(condExpL2 E' 𝕜 hm f)) f).symm)]

Premises used: MeasureTheory.integrable_congr, MeasureTheory.ae_restrict_of_ae, MeasureTheory.Lp.coeFn_sub, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable
    (↑(↑((↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) - f) : α →ₘ[μ] E') :
      α → E')
    (μ.restrict s)

Tactic:
integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs

Premises used: fact_one_le_two_ennreal, MeasureTheory.integrableOn_Lp_of_measure_ne_top, MeasureTheory.IntegrableOn, Fact.elim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable
    (↑(↑((↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) - f) : α →ₘ[μ] E') :
      α → E')
    (μ.restrict s)

Tactic:
exact integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs

Premises used: fact_one_le_two_ennreal, MeasureTheory.integrableOn_Lp_of_measure_ne_top, Fact.elim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E'
refine_2 :
  Eq.{u_7 + 1} (α := 𝕜)
    (∫ (x : α) in s,
      ⟪c,
          (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
              α → E')
            x⟫ -
        ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') x⟫ ∂μ)
    0
⊢ Eq.{u_7 + 1} (α := 𝕜)
    (∫ (x : α) in s,
      ⟪c,
        HSub.hSub (α := α → E')
          (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
            α → E')
          (↑(↑f : α →ₘ[μ] E') : α → E') x⟫ ∂μ)
    0

Tactic:
simp_rw [Pi.sub_apply, inner_sub_right]

Premises used: inner_sub_right, Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E'
refine_2 :
  HSub.hSub (α := 𝕜)
      (∫ (a : α) in s,
        ⟪c,
          (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
              α → E')
            a⟫ ∂μ)
      (∫ (a : α) in s, ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫ ∂μ) =
    0
⊢ Eq.{u_7 + 1} (α := 𝕜)
    (∫ (x : α) in s,
      ⟪c,
          (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
              α → E')
            x⟫ -
        ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') x⟫ ∂μ)
    0

Tactic:
rw [integral_sub
      ((integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs).const_inner c)
      ((integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs).const_inner c)]

Premises used: MeasureTheory.integral_sub
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E'
⊢ EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫) ⋯) : α →ₘ[μ] 𝕜) : α → 𝕜) fun (a : α) ↦
    ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫

Tactic:
have h_ae_eq_f := MemLp.coeFn_toLp (E := 𝕜) ((Lp.memLp f).const_inner c)
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E'
h_ae_eq_f :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫) ⋯) : α →ₘ[μ] 𝕜) : α → 𝕜) fun (a : α) ↦
    ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫
refine_2 :
  Eq.{u_7 + 1} (α := 𝕜)
    (∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ))
                      (MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫) ⋯)) :
                  ↥(Lp 𝕜 2 μ)) :
              α →ₘ[μ] 𝕜) :
          α → 𝕜)
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫) ⋯) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ)
⊢ HSub.hSub (α := 𝕜)
      (∫ (a : α) in s,
        ⟪c,
          (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
              α → E')
            a⟫ ∂μ)
      (∫ (a : α) in s, ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫ ∂μ) =
    0

Tactic:
rw [sub_eq_zero, ←
    setIntegral_congr_ae (hm s hs) ((condExpL2_const_inner hm f c).mono fun x hx _ => hx), ←
    setIntegral_congr_ae (hm s hs) (h_ae_eq_f.mono fun x hx _ => hx)]

Premises used: sub_eq_zero, MeasureTheory.setIntegral_congr_ae, Filter.Eventually.mono, MeasureTheory.condExpL2_const_inner
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E'
h_ae_eq_f :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫) ⋯) : α →ₘ[μ] 𝕜) : α → 𝕜) fun (a : α) ↦
    ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫
⊢ Eq.{u_7 + 1} (α := 𝕜)
    (∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ))
                      (MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫) ⋯)) :
                  ↥(Lp 𝕜 2 μ)) :
              α →ₘ[μ] 𝕜) :
          α → 𝕜)
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫) ⋯) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ)

Tactic:
integral_condExpL2_eq_of_fin_meas_real _ hs hμs

Premises used: MeasureTheory.integral_condExpL2_eq_of_fin_meas_real
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E'
h_ae_eq_f :
  EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫) ⋯) : α →ₘ[μ] 𝕜) : α → 𝕜) fun (a : α) ↦
    ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫
⊢ Eq.{u_7 + 1} (α := 𝕜)
    (∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ))
                      (MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫) ⋯)) :
                  ↥(Lp 𝕜 2 μ)) :
              α →ₘ[μ] 𝕜) :
          α → 𝕜)
        x ∂μ)
    (∫ (x : α) in s, (↑(↑(MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫) ⋯) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ)

Tactic:
exact integral_condExpL2_eq_of_fin_meas_real _ hs hμs

Premises used: MeasureTheory.integral_condExpL2_eq_of_fin_meas_real
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst_5 : RCLike 𝕜'
inst_6 : NormedAddCommGroup E''
inst_7 : InnerProductSpace 𝕜' E''
inst_8 : CompleteSpace E''
inst_9 : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ (↑(↑(↑((condExpL2 E'' 𝕜' hm : (a : ↥(Lp E'' 2 μ)) → ↥(lpMeas E'' 𝕜' m 2 μ)) (T.compLp f)) : ↥(Lp E'' 2 μ)) :
          α →ₘ[μ] E'') :
      α → E'') =ᶠ[ae μ]
    (↑(↑(T.compLp (↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ))) :
          α →ₘ[μ] E'') :
      α → E'')

Tactic:
Lp.ae_eq_of_forall_setIntegral_eq' 𝕜' hm _ _ two_ne_zero ENNReal.coe_ne_top
    (fun s _ hμs => integrableOn_condExpL2_of_measure_ne_top hm hμs.ne _) (fun s _ hμs =>
      integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs.ne) ?_ ?_ ?_

Premises used: fact_one_le_two_ennreal, MeasureTheory.integrableOn_Lp_of_measure_ne_top, MeasureTheory.condExpL2, MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq', ContinuousLinearMap.compLp, two_ne_zero, Fact.elim, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, Subtype.val, DFunLike.coe, LT.lt.ne, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst_5 : RCLike 𝕜'
inst_6 : NormedAddCommGroup E''
inst_7 : InnerProductSpace 𝕜' E''
inst_8 : CompleteSpace E''
inst_9 : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
refine_1 :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_8 + 1} (α := E'')
          (∫ (x : α) in s,
            (↑(↑(↑((condExpL2 E'' 𝕜' hm : (a : ↥(Lp E'' 2 μ)) → ↥(lpMeas E'' 𝕜' m 2 μ)) (T.compLp f)) : ↥(Lp E'' 2 μ)) :
                    α →ₘ[μ] E'') :
                α → E'')
              x ∂μ)
          (∫ (x : α) in s,
            (↑(↑(T.compLp (↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ))) :
                    α →ₘ[μ] E'') :
                α → E'')
              x ∂μ)
refine_2 :
  AEStronglyMeasurable.{u_1, u_8} (β := E'')
    (↑(↑(↑((condExpL2 E'' 𝕜' hm : (a : ↥(Lp E'' 2 μ)) → ↥(lpMeas E'' 𝕜' m 2 μ)) (T.compLp f)) : ↥(Lp E'' 2 μ)) :
          α →ₘ[μ] E'') :
      α → E'')
    μ
refine_3 :
  AEStronglyMeasurable
    (↑(↑(T.compLp (↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ))) :
          α →ₘ[μ] E'') :
      α → E'')
    μ
⊢ (↑(↑(↑((condExpL2 E'' 𝕜' hm : (a : ↥(Lp E'' 2 μ)) → ↥(lpMeas E'' 𝕜' m 2 μ)) (T.compLp f)) : ↥(Lp E'' 2 μ)) :
          α →ₘ[μ] E'') :
      α → E'') =ᶠ[ae μ]
    (↑(↑(T.compLp (↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ))) :
          α →ₘ[μ] E'') :
      α → E'')

Tactic:
refine Lp.ae_eq_of_forall_setIntegral_eq' 𝕜' hm _ _ two_ne_zero ENNReal.coe_ne_top
    (fun s _ hμs => integrableOn_condExpL2_of_measure_ne_top hm hμs.ne _) (fun s _ hμs =>
      integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs.ne) ?_ ?_ ?_

Premises used: fact_one_le_two_ennreal, MeasureTheory.integrableOn_Lp_of_measure_ne_top, MeasureTheory.Lp.ae_eq_of_forall_setIntegral_eq', two_ne_zero, Fact.elim, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, LT.lt.ne, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst_5 : RCLike 𝕜'
inst_6 : NormedAddCommGroup E''
inst_7 : InnerProductSpace 𝕜' E''
inst_8 : CompleteSpace E''
inst_9 : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ AEStronglyMeasurable.{u_1, u_8} (β := E'')
    (↑(↑(↑((condExpL2 E'' 𝕜' hm : (a : ↥(Lp E'' 2 μ)) → ↥(lpMeas E'' 𝕜' m 2 μ)) (T.compLp f)) : ↥(Lp E'' 2 μ)) :
          α →ₘ[μ] E'') :
      α → E'')
    μ

Tactic:
lpMeas.aestronglyMeasurable _

Premises used: MeasureTheory.lpMeas.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst_5 : RCLike 𝕜'
inst_6 : NormedAddCommGroup E''
inst_7 : InnerProductSpace 𝕜' E''
inst_8 : CompleteSpace E''
inst_9 : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ AEStronglyMeasurable.{u_1, u_8} (β := E'')
    (↑(↑(↑((condExpL2 E'' 𝕜' hm : (a : ↥(Lp E'' 2 μ)) → ↥(lpMeas E'' 𝕜' m 2 μ)) (T.compLp f)) : ↥(Lp E'' 2 μ)) :
          α →ₘ[μ] E'') :
      α → E'')
    μ

Tactic:
exact lpMeas.aestronglyMeasurable _

Premises used: MeasureTheory.lpMeas.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst_5 : RCLike 𝕜'
inst_6 : NormedAddCommGroup E''
inst_7 : InnerProductSpace 𝕜' E''
inst_8 : CompleteSpace E''
inst_9 : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
⊢ ∀ᵐ (a : α) ∂μ,
    (↑(↑(T.compLp (↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ))) :
              α →ₘ[μ] E'') :
          α → E'')
        a =
      (T : (a : E') → E'')
        ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
            α → E')
          a)

Tactic:
have h_coe := T.coeFn_compLp (condExpL2 E' 𝕜 hm f : α →₂[μ] E')
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst_5 : RCLike 𝕜'
inst_6 : NormedAddCommGroup E''
inst_7 : InnerProductSpace 𝕜' E''
inst_8 : CompleteSpace E''
inst_9 : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
h_coe :
  ∀ᵐ (a : α) ∂μ,
    (↑(↑(T.compLp (↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ))) :
              α →ₘ[μ] E'') :
          α → E'')
        a =
      (T : (a : E') → E'')
        ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
            α → E')
          a)
⊢ (↑(↑(T.compLp (↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ))) : α →ₘ[μ] E'') :
      α → E'') =ᶠ[ae μ]
    fun (a : α) ↦
    (T : (a : E') → E'')
      ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') : α → E')
        a)

Tactic:
rw [← EventuallyEq] at h_coe

Premises used: Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
E'' : Type u_8
𝕜' : Type u_9
inst_5 : RCLike 𝕜'
inst_6 : NormedAddCommGroup E''
inst_7 : InnerProductSpace 𝕜' E''
inst_8 : CompleteSpace E''
inst_9 : NormedSpace ℝ E''
hm : m ≤ m0
T : E' →L[ℝ] E''
f : ↥(Lp E' 2 μ)
h_coe :
  (↑(↑(T.compLp (↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ))) : α →ₘ[μ] E'') :
      α → E'') =ᶠ[ae μ]
    fun (a : α) ↦
    (T : (a : E') → E'')
      ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') : α → E')
        a)
⊢ AEStronglyMeasurable
    (↑(↑(T.compLp (↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ))) :
          α →ₘ[μ] E'') :
      α → E'')
    μ

Tactic:
AEStronglyMeasurable.congr ?_ h_coe.symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, Filter.EventuallyEq.symm