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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
⊢ 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
have 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
Tactic: rw [indicatorConstLp_eq_toSpanSingleton_compLp hs hμs x]
-- 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 α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : 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
have 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')
Tactic: have h_comp :=
    condExpL2_comp_continuousLinearMap ℝ 𝕜 hm (toSpanSingleton ℝ x)
      (indicatorConstLp 2 hs hμs (1 : ℝ))
-- 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
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
have 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
Tactic: refine h_comp.trans ?_
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : 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 μ)))
have 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')
Tactic: ext1
-- 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
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')
have 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')
Tactic: refine (condExpL2_indicator_ae_eq_smul 𝕜 hm hs hμs x).trans ?_
-- 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 α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : 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) =ᶠ[ae μ]
    (↑(↑(compLp (toSpanSingleton ℝ x)
              (↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ))) :
          α →ₘ[μ] E') :
      α → E')
have 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)
Tactic: have h_comp := (toSpanSingleton ℝ x).coeFn_compLp
    (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α →₂[μ] ℝ)
-- 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 α
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)
⊢ (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')
have 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)
Tactic: rw [← EventuallyEq] at h_comp
Cleared hypotheses: h_comp
-- 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
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')
have 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)
Tactic: refine EventuallyEq.trans ?_ h_comp.symm
-- 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
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)
⊢ 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)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x_1 : α |
      (fun (x_2 : α) ↦
          Eq.{u_3 + 1} (α := 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)
              x_2)
            ((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) :
                  E'))
              x_2))
        x_1}
    a
Tactic: filter_upwards with y using rfl
-- 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
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 :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        (fun (x_2 : α) ↦
            Eq.{u_3 + 1} (α := 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)
                x_2)
              ((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) :
                    E'))
                x_2))
          x_1}
      a
⊢ 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)
have h₁ : ∀ (a : α),
  HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x =
    (toSpanSingleton ℝ x : (a : ℝ) → E')
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
Tactic: filter_upwards with y using rfl
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
a : α
ha :
  Eq.{u_3 + 1} (α := 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')
      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)
      a)
h : a ∈ t
⊢ (↑(nnnorm.{u_3} (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')
            a)) :
      ℝ≥0∞) =
    (↑‖HSMul.hSMul (α := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                            (indicatorConstLp (s := s) 2 hs hμs 1)) :
                        ↥(Lp ℝ 2 μ)) :
                    α →ₘ[μ] ℝ) :
                α → ℝ)
              a)
            x‖₊ :
      ℝ≥0∞)
have rw : (↑(nnnorm.{u_3} (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)
          a)) :
    ℝ≥0∞) =
  (↑‖HSMul.hSMul (α := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                      ↥(Lp ℝ 2 μ)) :
                  α →ₘ[μ] ℝ) :
              α → ℝ)
            a)
          x‖₊ :
    ℝ≥0∞)
Tactic: rw [ha]
-- 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
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E'
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (a : α) in t,
      (↑‖HSMul.hSMul (α := ℝ)
              ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                              (indicatorConstLp (s := s) 2 hs hμs 1)) :
                          ↥(Lp ℝ 2 μ)) :
                      α →ₘ[μ] ℝ) :
                  α → ℝ)
                a)
              x‖₊ :
        ℝ≥0∞) ∂μ =
    (∫⁻ (a : α) in t,
        (↑(nnnorm (E := ℝ)
              ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                              (indicatorConstLp (s := s) 2 hs hμs 1)) :
                          ↥(Lp ℝ 2 μ)) :
                      α →ₘ[μ] ℝ) :
                  α → ℝ)
                a)) :
          ℝ≥0∞) ∂μ) *
      (↑‖x‖₊ : ℝ≥0∞)
have simp_rw : ∫⁻ (a : α) in t,
    (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                            (indicatorConstLp (s := s) 2 hs hμs 1)) :
                        ↥(Lp ℝ 2 μ)) :
                    α →ₘ[μ] ℝ) :
                α → ℝ)
              a)) :
        ℝ≥0∞) *
      (↑‖x‖₊ : ℝ≥0∞) ∂μ =
  (∫⁻ (a : α) in t,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                            (indicatorConstLp (s := s) 2 hs hμs 1)) :
                        ↥(Lp ℝ 2 μ)) :
                    α →ₘ[μ] ℝ) :
                α → ℝ)
              a)) :
        ℝ≥0∞) ∂μ) *
    (↑‖x‖₊ : ℝ≥0∞)
Tactic: simp_rw [nnnorm_smul, ENNReal.coe_mul]