awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥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∞) ∂μ ≤
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ t)
have refine : ∫⁻ (x : α) in t, (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) ∂μ =
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ t)
Tactic: refine (lintegral_nnnorm_condExpL2_le ht hμt _).trans (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in t, (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) ∂μ =
    ∫⁻ (x : α) in t, s.indicator (fun (x : α) ↦ 1) x ∂μ
have refine : ∀ᵐ (x : α) ∂μ,
  Eq (α := ℝ≥0∞)
    ((fun (x : α) ↦ (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞)) x)
    (s.indicator (fun (x : α) ↦ 1) x)
Tactic: refine lintegral_congr_ae (ae_restrict_of_ae ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ,
    Eq (α := ℝ≥0∞)
      ((fun (x : α) ↦ (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞))
        x)
      (s.indicator (fun (x : α) ↦ 1) x)
have refine : ∀ (x : α)
  (hx :
    Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) (s.indicator (fun (x : α) ↦ 1) x)),
  Eq (α := ℝ≥0∞)
    ((fun (x : α) ↦ (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞)) x)
    (s.indicator (fun (x : α) ↦ 1) x)
Tactic: refine (@indicatorConstLp_coeFn _ _ _ 2 _ _ _ hs hμs (1 : ℝ)).mono fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) (s.indicator (fun (x : α) ↦ 1) x)
⊢ (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) =
    s.indicator (fun (x : α) ↦ 1) x
have rw : (↑(nnnorm (E := ℝ) (s.indicator (fun (x : α) ↦ 1) x)) : ℝ≥0∞) = s.indicator (fun (x : α) ↦ 1) x
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) (s.indicator (fun (x : α) ↦ 1) x)
⊢ (↑(nnnorm (E := ℝ) (if x ∈ s then 1 else 0)) : ℝ≥0∞) = if x ∈ s then 1 else 0
have pos : x ∈ s → (↑(nnnorm (E := ℝ) 1) : ℝ≥0∞) = 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) (s.indicator (fun (x : α) ↦ 1) x)
pos : x ∈ s → (↑(nnnorm (E := ℝ) 1) : ℝ≥0∞) = 1
⊢ (↑(nnnorm (E := ℝ) (if x ∈ s then 1 else 0)) : ℝ≥0∞) = if x ∈ s then 1 else 0
have neg : x ∉ s → (↑(nnnorm (E := ℝ) 0) : ℝ≥0∞) = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (hypothesis)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in t, (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) ∂μ =
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ t)
have h_eq : ∫⁻ (x : α) in t, (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) ∂μ =
  ∫⁻ (x : α) in t, s.indicator (fun (x : α) ↦ 1) x ∂μ
Tactic: have h_eq :
    ∫⁻ x in t, ‖(indicatorConstLp 2 hs hμs (1 : ℝ)) x‖₊ ∂μ =
      ∫⁻ x in t, s.indicator (fun _ => (1 : ℝ≥0∞)) x ∂μ := by
    refine lintegral_congr_ae (ae_restrict_of_ae ?_)
    refine (@indicatorConstLp_coeFn _ _ _ 2 _ _ _ hs hμs (1 : ℝ)).mono fun x hx => ?_
    dsimp only
    rw [hx]
    classical
    simp_rw [Set.indicator_apply]
    split_ifs <;> simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_eq :
  ∫⁻ (x : α) in t, (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) ∂μ =
    ∫⁻ (x : α) in t, s.indicator (fun (x : α) ↦ 1) x ∂μ
⊢ ∫⁻ (x : α) in t, (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) ∂μ =
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ t)
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ.restrict (s ∩ t) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ t)
Tactic: rw [h_eq, lintegral_indicator hs, lintegral_const, Measure.restrict_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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
⊢ 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 μ
have refine : MemLp.{u_1, u_2} (ε := E)
  (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) 2 μ
Tactic: refine MemLp.const_inner _ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (hypothesis)
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
⊢ EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ))
                  (MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫) ⋯)) :
              ↥(Lp 𝕜 2 μ)) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
have 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 μ
Tactic: have h_mem_Lp : MemLp (fun a => ⟪c, (condExpL2 E 𝕜 hm f : α → E) a⟫) 2 μ := by
    refine MemLp.const_inner _ ?_; exact Lp.memLp _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (hypothesis)
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 μ
⊢ EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ))
                  (MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫) ⋯)) :
              ↥(Lp 𝕜 2 μ)) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
have 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⟫
Tactic: have h_eq : h_mem_Lp.toLp _ =ᵐ[μ] fun a => ⟪c, (condExpL2 E 𝕜 hm f : α → E) a⟫ :=
    h_mem_Lp.coeFn_toLp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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⟫
⊢ EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
    (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ))
                  (MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫) ⋯)) :
              ↥(Lp 𝕜 2 μ)) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫
have refine : EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
  (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ))
                (MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫) sorry)) :
            ↥(Lp 𝕜 2 μ)) :
        α →ₘ[μ] 𝕜) :
    α → 𝕜)
  (↑(↑(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) :
        α →ₘ[μ] 𝕜) :
    α → 𝕜)
Tactic: refine EventuallyEq.trans ?_ h_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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⟫
s : Set α
h : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn.{u_1, u_7} (ε := 𝕜)
    (↑(↑(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) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    s μ
have refine_1 : Integrable.{u_7, u_1} (ε := 𝕜)
  (fun (a : α) ↦
    ⟪c, (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) : α → E) a⟫)
  (μ.restrict s)
Tactic: rw [IntegrableOn, integrable_congr (ae_restrict_of_ae h_eq)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
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} (β := 𝕜)
    (↑(↑(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) :
          α →ₘ[μ] 𝕜) :
      α → 𝕜)
    μ
have refine_4 : 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: refine AEStronglyMeasurable.congr ?_ h_eq.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
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥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 ∂μ)
have 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
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)]
-- 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∞)
⊢ 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
have 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)
Tactic: refine integral_eq_zero_of_forall_integral_inner_eq_zero 𝕜 _ ?_ ?_
-- 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∞)
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)
⊢ 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
have 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
Tactic: refine integral_eq_zero_of_forall_integral_inner_eq_zero 𝕜 _ ?_ ?_
-- 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∞)
⊢ Integrable
    ((↑(↑(↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) : α →ₘ[μ] E') : α → E') -
      (↑(↑f : α →ₘ[μ] E') : α → E'))
    (μ.restrict s)
have refine_1 : Integrable
  (↑(↑((↑((condExpL2 E' 𝕜 hm : (a : ↥(Lp E' 2 μ)) → ↥(lpMeas E' 𝕜 m 2 μ)) f) : ↥(Lp E' 2 μ)) - f) : α →ₘ[μ] E') :
    α → E')
  (μ.restrict s)
Tactic: rw [integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub (↑(condExpL2 E' 𝕜 hm f)) f).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
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
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
have 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
Tactic: simp_rw [Pi.sub_apply, inner_sub_right]
-- 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'
⊢ 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
have 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
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)]
-- 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
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E'
⊢ 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 h_ae_eq_f : EventuallyEq.{u_1, u_7} (β := 𝕜) (ae μ)
  (↑(↑(MemLp.toLp (fun (a : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫) sorry) : α →ₘ[μ] 𝕜) : α → 𝕜) fun (a : α) ↦
  ⟪c, (↑(↑f : α →ₘ[μ] E') : α → E') a⟫
Tactic: have h_ae_eq_f := MemLp.coeFn_toLp (E := 𝕜) ((Lp.memLp f).const_inner c)