awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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))
    μ
⊢ AEStronglyMeasurable
    (↑(↑(T.compLp (↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ))) :
          α →ₘ[μ] E'') :
      α → E'')
    μ

Tactic:
refine AEStronglyMeasurable.congr ?_ h_coe.symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, 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 α
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.{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:
T.continuous.comp_aestronglyMeasurable (lpMeas.aestronglyMeasurable (condExpL2 E' 𝕜 hm f))

Premises used: Continuous.comp_aestronglyMeasurable, MeasureTheory.condExpL2, ContinuousLinearMap.continuous, DFunLike.coe, 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 μ)
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.{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:
exact T.continuous.comp_aestronglyMeasurable (lpMeas.aestronglyMeasurable (condExpL2 E' 𝕜 hm f))

Premises used: Continuous.comp_aestronglyMeasurable, MeasureTheory.condExpL2, ContinuousLinearMap.continuous, DFunLike.coe, 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
rw :
  EventuallyEq.{u_1, u_3} (β := E') (ae μ)
    (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ))
                  (compLp (toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1))) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E')
    fun (a : α) ↦
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x
⊢ EventuallyEq.{u_1, u_3} (β := E') (ae μ)
    (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs x)) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E')
    fun (a : α) ↦
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x

Tactic:
rw [indicatorConstLp_eq_toSpanSingleton_compLp hs hμs x]

Premises used: MeasureTheory.indicatorConstLp_eq_toSpanSingleton_compLp
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
⊢ (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ))
                  (compLp (toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1))) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E')

Tactic:
have h_comp :=
    condExpL2_comp_continuousLinearMap ℝ 𝕜 hm (toSpanSingleton ℝ x)
      (indicatorConstLp 2 hs hμs (1 : ℝ))
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
h_comp :
  (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ))
                  (compLp (toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1))) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E')
⊢ EventuallyEq.{u_1, u_3} (β := E') (ae μ)
    (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ))
                  (compLp (toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1))) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E')
    fun (a : α) ↦
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x

Tactic:
h_comp.trans ?_

Premises used: Filter.EventuallyEq.trans
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
h_comp :
  (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ))
                  (compLp (toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1))) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E')
refine :
  (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    fun (a : α) ↦
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x
⊢ EventuallyEq.{u_1, u_3} (β := E') (ae μ)
    (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ))
                  (compLp (toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1))) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E')
    fun (a : α) ↦
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x

Tactic:
refine h_comp.trans ?_

Premises used: Filter.EventuallyEq.trans
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
h_comp :
  (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ))
                  (compLp (toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1))) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E')
⊢ (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    fun (a : α) ↦
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x

Tactic:
(toSpanSingleton ℝ x).coeFn_compLp _

Premises used: Real, MeasureTheory.AEEqFun.cast, Filter.EventuallyEq, dite, ContinuousLinearMap.toSpanSingleton, ContinuousLinearMap.coeFn_compLp
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
h_comp :
  (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ))
                  (compLp (toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1))) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E')
⊢ (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    fun (a : α) ↦
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x

Tactic:
exact (toSpanSingleton ℝ x).coeFn_compLp _

Premises used: Real, ContinuousLinearMap.toSpanSingleton, ContinuousLinearMap.coeFn_compLp
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
h :
  (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs x)) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E')
⊢ Eq (α := ↥(Lp E' 2 μ))
    (↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs x)) :
      ↥(Lp E' 2 μ))
    (compLp (toSpanSingleton ℝ x)
      (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        ↥(Lp ℝ 2 μ)))

Tactic:
ext1
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
⊢ (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs x)) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E')

Tactic:
(condExpL2_indicator_ae_eq_smul 𝕜 hm hs hμs x).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExpL2_indicator_ae_eq_smul
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
h :
  (fun (a : α) ↦
      HSMul.hSMul (α := ℝ)
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          a)
        x) =ᶠ[ae μ]
    (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E')
⊢ (↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs x)) :
              ↥(Lp E' 2 μ)) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E')

Tactic:
refine (condExpL2_indicator_ae_eq_smul 𝕜 hm hs hμs x).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExpL2_indicator_ae_eq_smul
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
⊢ ∀ᵐ (a : α) ∂μ,
    (↑(↑(compLp (toSpanSingleton ℝ x)
                  (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                        (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ))) :
              α →ₘ[μ] E') :
          α → E')
        a =
      (toSpanSingleton ℝ x : (a : ℝ) → E')
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          a)

Tactic:
have h_comp := (toSpanSingleton ℝ x).coeFn_compLp
    (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α →₂[μ] ℝ)
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
h_comp :
  ∀ᵐ (a : α) ∂μ,
    (↑(↑(compLp (toSpanSingleton ℝ x)
                  (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                        (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ))) :
              α →ₘ[μ] E') :
          α → E')
        a =
      (toSpanSingleton ℝ x : (a : ℝ) → E')
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          a)
⊢ (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    fun (a : α) ↦
    (toSpanSingleton ℝ x : (a : ℝ) → E')
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)

Tactic:
rw [← EventuallyEq] at h_comp

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 α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
h_comp :
  (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    fun (a : α) ↦
    (toSpanSingleton ℝ x : (a : ℝ) → E')
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
⊢ (fun (a : α) ↦
      HSMul.hSMul (α := ℝ)
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          a)
        x) =ᶠ[ae μ]
    (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E')

Tactic:
EventuallyEq.trans ?_ h_comp.symm

Premises used: Filter.EventuallyEq.trans, 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
h_comp :
  (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E') =ᶠ[ae μ]
    fun (a : α) ↦
    (toSpanSingleton ℝ x : (a : ℝ) → E')
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
h :
  EventuallyEq.{u_1, u_3} (β := E') (ae μ)
    (fun (a : α) ↦
      HSMul.hSMul (α := ℝ)
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          a)
        x)
    fun (a : α) ↦
    (toSpanSingleton ℝ x : (a : ℝ) → E')
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
⊢ (fun (a : α) ↦
      HSMul.hSMul (α := ℝ)
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          a)
        x) =ᶠ[ae μ]
    (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E')

Tactic:
refine EventuallyEq.trans ?_ h_comp.symm

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.symm