awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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⟫
⊢ 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
have 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⟫) sorry)) :
                ↥(Lp 𝕜 2 μ)) :
            α →ₘ[μ] 𝕜) :
        α → 𝕜)
      x ∂μ)
  (∫ (x : α) in s, (↑(↑(MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫) sorry) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ)
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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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'')
have 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 ∂μ)
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) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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 ∂μ)
⊢ (↑(↑(↑((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'')
have 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'')
  μ
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) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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'')
    μ
⊢ (↑(↑(↑((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'')
have refine_3 : AEStronglyMeasurable
  (↑(↑(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) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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 μ)
s : Set α
hs : MeasurableSet s
hμ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 ∂μ)
have refine_1 : 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 : (a : E') → E'')
      ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') : α → E')
        x) ∂μ)
Tactic: rw [T.setIntegral_compLp _ (hm s hs),
      T.integral_comp_comm
        (integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs.ne),
      integral_condExpL2_eq hm f hs hμs.ne,
      integral_condExpL2_eq hm (T.compLp f) hs hμs.ne, T.setIntegral_compLp _ (hm s hs),
      T.integral_comp_comm
        (integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs.ne)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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 μ)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  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 : (a : E') → E'')
        ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
            α → E')
          x) ∂μ)
⊢ 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 ∂μ)
have refine_1₁ : 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 ∂μ :
    E'')
  ((T : (a : E') → E'')
      (∫ (x : α) in s,
        (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
            α → E')
          x ∂μ) :
    E'')
Tactic: rw [T.setIntegral_compLp _ (hm s hs),
      T.integral_comp_comm
        (integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs.ne),
      integral_condExpL2_eq hm f hs hμs.ne,
      integral_condExpL2_eq hm (T.compLp f) hs hμs.ne, T.setIntegral_compLp _ (hm s hs),
      T.integral_comp_comm
        (integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs.ne)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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 μ)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  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 : (a : E') → E'')
        ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
            α → E')
          x) ∂μ)
refine_1₁ :
  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 ∂μ :
      E'')
    ((T : (a : E') → E'')
        (∫ (x : α) in s,
          (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
              α → E')
            x ∂μ) :
      E'')
⊢ 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 ∂μ)
have refine_1₂ : 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 ∂μ :
    E'')
  ((T : (a : E') → E'') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) : E'')
Tactic: rw [T.setIntegral_compLp _ (hm s hs),
      T.integral_comp_comm
        (integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs.ne),
      integral_condExpL2_eq hm f hs hμs.ne,
      integral_condExpL2_eq hm (T.compLp f) hs hμs.ne, T.setIntegral_compLp _ (hm s hs),
      T.integral_comp_comm
        (integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs.ne)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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 μ)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  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 : (a : E') → E'')
        ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
            α → E')
          x) ∂μ)
refine_1₁ :
  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 ∂μ :
      E'')
    ((T : (a : E') → E'')
        (∫ (x : α) in s,
          (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
              α → E')
            x ∂μ) :
      E'')
refine_1₂ :
  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 ∂μ :
      E'')
    ((T : (a : E') → E'') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) : E'')
⊢ 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 ∂μ)
have refine_1₃ : Eq.{u_8 + 1} (α := E'') (∫ (x : α) in s, (↑(↑(T.compLp f) : α →ₘ[μ] E'') : α → E'') x ∂μ : E'')
  ((T : (a : E') → E'') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) : E'')
Tactic: rw [T.setIntegral_compLp _ (hm s hs),
      T.integral_comp_comm
        (integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs.ne),
      integral_condExpL2_eq hm f hs hμs.ne,
      integral_condExpL2_eq hm (T.compLp f) hs hμs.ne, T.setIntegral_compLp _ (hm s hs),
      T.integral_comp_comm
        (integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs.ne)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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 μ)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  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 : (a : E') → E'')
        ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
            α → E')
          x) ∂μ)
refine_1₁ :
  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 ∂μ :
      E'')
    ((T : (a : E') → E'')
        (∫ (x : α) in s,
          (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') :
              α → E')
            x ∂μ) :
      E'')
refine_1₂ :
  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 ∂μ :
      E'')
    ((T : (a : E') → E'') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) : E'')
refine_1₃ :
  Eq.{u_8 + 1} (α := E'') (∫ (x : α) in s, (↑(↑(T.compLp f) : α →ₘ[μ] E'') : α → E'') x ∂μ : E'')
    ((T : (a : E') → E'') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) : E'')
⊢ 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 ∂μ)
have refine_1₄ : Eq.{u_8 + 1} (α := E'') (∫ (x : α) in s, (T : (a : E') → E'') ((↑(↑f : α →ₘ[μ] E') : α → E') x) ∂μ : E'')
  ((T : (a : E') → E'') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) : E'')
Tactic: rw [T.setIntegral_compLp _ (hm s hs),
      T.integral_comp_comm
        (integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs.ne),
      integral_condExpL2_eq hm f hs hμs.ne,
      integral_condExpL2_eq hm (T.compLp f) hs hμs.ne, T.setIntegral_compLp _ (hm s hs),
      T.integral_comp_comm
        (integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs.ne)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (hypothesis)
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
    (↑(↑(T.compLp (↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ))) :
          α →ₘ[μ] E'') :
      α → E'')
    μ
have 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)
Tactic: have h_coe := T.coeFn_compLp (condExpL2 E' 𝕜 hm f : α →₂[μ] E')
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (hypothesis)
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)
⊢ AEStronglyMeasurable
    (↑(↑(T.compLp (↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ))) :
          α →ₘ[μ] E'') :
      α → E'')
    μ
have 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)
Tactic: rw [← EventuallyEq] at h_coe
Cleared hypotheses: h_coe
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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'')
    μ
have refine_3 : AEStronglyMeasurable.{u_1, u_8} (β := E'')
  (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: refine AEStronglyMeasurable.congr ?_ h_coe.symm