awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ Eq (α := ↥(Lp E 2 μ))
    (↑(((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
              ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
            (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
          (indicatorConstLp (s := s) 2 ⋯ hμs c)) :
      ↥(Lp E 2 μ))
    (indicatorConstLp (s := s) 2 ⋯ hμs c)
have this : Fact (m ≤ m0)
Tactic: haveI : Fact (m ≤ m0) := ⟨hm⟩
-- 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 α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
this : Fact (m ≤ m0)
⊢ Eq (α := ↥(Lp E 2 μ))
    (↑(((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
              ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
            (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
          (indicatorConstLp (s := s) 2 ⋯ hμs c)) :
      ↥(Lp E 2 μ))
    (indicatorConstLp (s := s) 2 ⋯ hμs c)
have h_mem : Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) (indicatorConstLp (s := s) 2 sorry hμs c)
Tactic: have h_mem : indicatorConstLp 2 (hm s hs) hμs c ∈ lpMeas E 𝕜 m 2 μ :=
    mem_lpMeas_indicatorConstLp hm hs hμs
-- 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 α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
this : Fact (m ≤ m0)
h_mem : Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) (indicatorConstLp (s := s) 2 ⋯ hμs c)
ind : ↥(lpMeas E 𝕜 m 2 μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E 2 μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) x)
    (indicatorConstLp (s := s) 2 ⋯ hμs c) h_mem
⊢ Eq (α := ↥(Lp E 2 μ))
    (↑(((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
              ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
            (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
          (indicatorConstLp (s := s) 2 ⋯ hμs c)) :
      ↥(Lp E 2 μ))
    (indicatorConstLp (s := s) 2 ⋯ hμs c)
have h_coe_ind : (↑ind : ↥(Lp E 2 μ)) = indicatorConstLp (s := s) 2 sorry hμs c
Tactic: have h_coe_ind : (ind : α →₂[μ] E) = indicatorConstLp 2 (hm s hs) hμs c := rfl
-- 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 α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
this : Fact (m ≤ m0)
h_mem : Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) (indicatorConstLp (s := s) 2 ⋯ hμs c)
ind : ↥(lpMeas E 𝕜 m 2 μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E 2 μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) x)
    (indicatorConstLp (s := s) 2 ⋯ hμs c) h_mem
h_coe_ind : (↑ind : ↥(Lp E 2 μ)) = indicatorConstLp (s := s) 2 ⋯ hμs c
⊢ Eq (α := ↥(Lp E 2 μ))
    (↑(((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
              ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
            (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
          (indicatorConstLp (s := s) 2 ⋯ hμs c)) :
      ↥(Lp E 2 μ))
    (indicatorConstLp (s := s) 2 ⋯ hμs c)
have h_orth_mem : ((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
        ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
      (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
    (↑ind : ↥(Lp E 2 μ)) =
  ind
Tactic: have h_orth_mem := Submodule.orthogonalProjection_mem_subspace_eq_self ind
-- 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 α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
this : Fact (m ≤ m0)
h_mem : Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) (indicatorConstLp (s := s) 2 ⋯ hμs c)
ind : ↥(lpMeas E 𝕜 m 2 μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E 2 μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) x)
    (indicatorConstLp (s := s) 2 ⋯ hμs c) h_mem
h_coe_ind : (↑ind : ↥(Lp E 2 μ)) = indicatorConstLp (s := s) 2 ⋯ hμs c
h_orth_mem :
  ((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
          ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
        (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
      (↑ind : ↥(Lp E 2 μ)) =
    ind
⊢ Eq (α := ↥(Lp E 2 μ))
    (↑(((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
              ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
            (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
          (indicatorConstLp (s := s) 2 ⋯ hμs c)) :
      ↥(Lp E 2 μ))
    (indicatorConstLp (s := s) 2 ⋯ hμs c)
have rw : (↑(((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
            ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
          (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
        (↑ind : ↥(Lp E 2 μ))) :
    ↥(Lp E 2 μ)) =
  (↑ind : ↥(Lp E 2 μ))
Tactic: rw [← h_coe_ind, h_orth_mem]
-- 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 α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
this : Fact (m ≤ m0)
h_mem : Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) (indicatorConstLp (s := s) 2 ⋯ hμs c)
ind : ↥(lpMeas E 𝕜 m 2 μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E 2 μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) x)
    (indicatorConstLp (s := s) 2 ⋯ hμs c) h_mem
h_coe_ind : (↑ind : ↥(Lp E 2 μ)) = indicatorConstLp (s := s) 2 ⋯ hμs c
h_orth_mem :
  ((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
          ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
        (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
      (↑ind : ↥(Lp E 2 μ)) =
    ind
rw :
  (↑(((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
              ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
            (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
          (↑ind : ↥(Lp E 2 μ))) :
      ↥(Lp E 2 μ)) =
    (↑ind : ↥(Lp E 2 μ))
⊢ Eq (α := ↥(Lp E 2 μ))
    (↑(((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
              ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
            (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
          (indicatorConstLp (s := s) 2 ⋯ hμs c)) :
      ↥(Lp E 2 μ))
    (indicatorConstLp (s := s) 2 ⋯ hμs c)
have rw₁ : (↑ind : ↥(Lp E 2 μ)) = (↑ind : ↥(Lp E 2 μ))
Tactic: rw [← h_coe_ind, h_orth_mem]
-- 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 g : ↥(Lp E 2 μ)
hg : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E) : α → E) μ
⊢ ⟪(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)), g⟫ = ⟪f, g⟫
have symm : ⟪f, g⟫ = ⟪(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)), g⟫
Tactic: symm
-- 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 g : ↥(Lp E 2 μ)
hg : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E) : α → E) μ
⊢ ⟪f, g⟫ = ⟪(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) f) : ↥(Lp E 2 μ)), g⟫
have rw : ⟪f -
      (↑(((Submodule.orthogonalProjection (𝕜 := 𝕜) (E := ↥(Lp E 2 μ)) (lpMeas E 𝕜 m 2 μ) :
                ↥(Lp E 2 μ) →L[𝕜] ↥(lpMeas E 𝕜 m 2 μ)) :
              (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ))
            f) :
        ↥(Lp E 2 μ)),
    g⟫ =
  0
Tactic: rw [← sub_eq_zero, ← inner_sub_left, condExpL2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
𝕜 : Type u_7
inst : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_7 + 1} (α := 𝕜)
    (∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ)
    (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ)
have rw : ∫ (x : α) in s,
    (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
  ⟪indicatorConstLp (s := s) 2 sorry hμs 1, f⟫
Tactic: rw [← L2.inner_indicatorConstLp_one (𝕜 := 𝕜) (hm s hs) hμs f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
𝕜 : Type u_7
inst : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
    inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) (indicatorConstLp (s := s) 2 ⋯ hμs 1)
      (↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ))
have rw : Eq.{u_7 + 1} (α := 𝕜)
  (∫ (x : α) in s,
    (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ)
  (∫ (x : α) in s,
    (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ)
Tactic: rw [L2.inner_indicatorConstLp_one (hm s hs) hμs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_7
inst : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
    ⟪indicatorConstLp (s := s) 2 ⋯ hμs 1, f⟫
have h_eq_inner : ∫ (x : α) in s,
    (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
  inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) (indicatorConstLp (s := s) 2 sorry hμs 1)
    (↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ))
Tactic: have h_eq_inner : ∫ x in s, (condExpL2 𝕜 𝕜 hm f : α → 𝕜) x ∂μ =
      ⟪indicatorConstLp 2 (hm s hs) hμs (1 : 𝕜), condExpL2 𝕜 𝕜 hm f⟫ := by
    rw [L2.inner_indicatorConstLp_one (hm s hs) hμs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
𝕜 : Type u_7
inst : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_eq_inner :
  ∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
    inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) (indicatorConstLp (s := s) 2 ⋯ hμs 1)
      (↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ))
⊢ ∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
    ⟪indicatorConstLp (s := s) 2 ⋯ hμs 1, f⟫
have rw : inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) (indicatorConstLp (s := s) 2 sorry hμs 1)
    (↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) =
  ⟪indicatorConstLp (s := s) 2 sorry hμs 1, f⟫
Tactic: rw [h_eq_inner, ← inner_condExpL2_left_eq_right, condExpL2_indicator_of_measurable hm hs hμs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
𝕜 : Type u_7
inst : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_eq_inner :
  ∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
    inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) (indicatorConstLp (s := s) 2 ⋯ hμs 1)
      (↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ))
rw :
  inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) (indicatorConstLp (s := s) 2 ⋯ hμs 1)
      (↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) =
    ⟪indicatorConstLp (s := s) 2 ⋯ hμs 1, f⟫
⊢ ∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
    ⟪indicatorConstLp (s := s) 2 ⋯ hμs 1, f⟫
have rw₁ : ⟪(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) (indicatorConstLp (s := s) 2 sorry hμs 1)) : ↥(Lp 𝕜 2 μ)),
    f⟫ =
  ⟪indicatorConstLp (s := s) 2 sorry hμs 1, f⟫
Tactic: rw [h_eq_inner, ← inner_condExpL2_left_eq_right, condExpL2_indicator_of_measurable hm hs hμs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
𝕜 : Type u_7
inst : RCLike 𝕜
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp 𝕜 2 μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_eq_inner :
  ∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
    inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) (indicatorConstLp (s := s) 2 ⋯ hμs 1)
      (↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ))
rw :
  inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) (indicatorConstLp (s := s) 2 ⋯ hμs 1)
      (↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) =
    ⟪indicatorConstLp (s := s) 2 ⋯ hμs 1, f⟫
rw₁ :
  ⟪(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) (indicatorConstLp (s := s) 2 ⋯ hμs 1)) :
        ↥(Lp 𝕜 2 μ)),
      f⟫ =
    ⟪indicatorConstLp (s := s) 2 ⋯ hμs 1, f⟫
⊢ ∫ (x : α) in s,
      (↑(↑(↑((condExpL2 𝕜 𝕜 hm : (a : ↥(Lp 𝕜 2 μ)) → ↥(lpMeas 𝕜 𝕜 m 2 μ)) f) : ↥(Lp 𝕜 2 μ)) : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ =
    ⟪indicatorConstLp (s := s) 2 ⋯ hμs 1, f⟫
have rw₂ : ⟪indicatorConstLp (s := s) 2 sorry hμs 1, f⟫ = ⟪indicatorConstLp (s := s) 2 sorry hμs 1, f⟫
Tactic: rw [h_eq_inner, ← inner_condExpL2_left_eq_right, condExpL2_indicator_of_measurable hm hs hμs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (hypothesis)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
⊢ ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ
have hg_meas : StronglyMeasurable g
Tactic: have hg_meas : StronglyMeasurable[m] g := h_meas.choose_spec.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (hypothesis)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
⊢ ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ
have hg_eq : g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
Tactic: have hg_eq : g =ᵐ[μ] condExpL2 ℝ ℝ hm f := h_meas.choose_spec.2.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (hypothesis)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
⊢ ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ
have hg_eq_restrict : g =ᶠ[ae (μ.restrict s)]
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
Tactic: have hg_eq_restrict : g =ᵐ[μ.restrict s] condExpL2 ℝ ℝ hm f := ae_restrict_of_ae hg_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
have refine : ∀ (x : α)
  (hx :
    g x =
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x),
  Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) x)
    ((fun (x : α) ↦
        (↑(nnnorm (E := ℝ)
              ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
                  α → ℝ)
                x)) :
          ℝ≥0∞))
      x)
Tactic: refine hg_eq_restrict.mono fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 (hypothesis)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
⊢ ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ
have hg_nnnorm_eq : (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
  (↑(nnnorm (E := ℝ)
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
          x)) :
    ℝ≥0∞)
Tactic: have hg_nnnorm_eq : (fun x => (‖g x‖₊ : ℝ≥0∞)) =ᵐ[μ.restrict s] fun x =>
      (‖(condExpL2 ℝ ℝ hm f : α → ℝ) x‖₊ : ℝ≥0∞) := by
    refine hg_eq_restrict.mono fun x hx => ?_
    dsimp only
    simp_rw [hx]