awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') x ∂μ) 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg_restrict : (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae (μ.restrict s)] g
⊢ Eq.{u_2 + 1} (α := E') (∫ (a : α) in s, (↑(↑(↑f : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') a ∂μ) 0

Tactic:
exact hf_zero s hs hμs
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) 0
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
f_meas : ↥(lpMeas E' 𝕜 m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E' p μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E' p μ)) (lpMeas E' 𝕜 m p μ) x) f
    hf_meas
⊢ (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] (↑(↑(↑f_meas : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E')

Tactic:
simp [f_meas]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) 0
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
f_meas : ↥(lpMeas E' 𝕜 m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E' p μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E' p μ)) (lpMeas E' 𝕜 m p μ) x) f
    hf_meas
⊢ (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] (↑(↑(↑f_meas : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E')

Tactic:
have hf_f_meas : f =ᵐ[μ] f_meas := by simp [f_meas]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) 0
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
f_meas : ↥(lpMeas E' 𝕜 m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E' p μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E' p μ)) (lpMeas E' 𝕜 m p μ) x) f
    hf_meas
hf_f_meas : (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] (↑(↑(↑f_meas : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E')
⊢ (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0

Tactic:
hf_f_meas.trans ?_

Premises used: Filter.EventuallyEq.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) 0
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
f_meas : ↥(lpMeas E' 𝕜 m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E' p μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E' p μ)) (lpMeas E' 𝕜 m p μ) x) f
    hf_meas
hf_f_meas : (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] (↑(↑(↑f_meas : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E')
refine : (↑(↑(↑f_meas : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
⊢ (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0

Tactic:
refine hf_f_meas.trans ?_

Premises used: Filter.EventuallyEq.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) 0
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
f_meas : ↥(lpMeas E' 𝕜 m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E' p μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E' p μ)) (lpMeas E' 𝕜 m p μ) x) f
    hf_meas
hf_f_meas : (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] (↑(↑(↑f_meas : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E')
⊢ (↑(↑(↑f_meas : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0

Tactic:
lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero
    hm f_meas hp_ne_zero hp_ne_top hf_int_finite hf_zero

Premises used: MeasureTheory.lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ) 0
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
f_meas : ↥(lpMeas E' 𝕜 m p μ) :=
  Subtype.mk (p := fun (x : ↥(Lp E' p μ)) ↦ Membership.mem (γ := Submodule 𝕜 ↥(Lp E' p μ)) (lpMeas E' 𝕜 m p μ) x) f
    hf_meas
hf_f_meas : (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] (↑(↑(↑f_meas : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E')
⊢ (↑(↑(↑f_meas : ↥(Lp E' p μ)) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0

Tactic:
exact lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero
    hm f_meas hp_ne_zero hp_ne_top hf_int_finite hf_zero

Premises used: MeasureTheory.lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
h_sub : (↑(↑(f - g) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
rw : (↑(↑f : α →ₘ[μ] E') : α → E') - (↑(↑g : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
⊢ (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E') : α → E')

Tactic:
rw [← sub_ae_eq_zero]

Premises used: MeasureTheory.sub_ae_eq_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
h_sub : (↑(↑(f - g) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
⊢ (↑(↑f : α →ₘ[μ] E') : α → E') - (↑(↑g : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0

Tactic:
(Lp.coeFn_sub f g).symm.trans h_sub

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Lp.coeFn_sub, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
h_sub : (↑(↑(f - g) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
⊢ (↑(↑f : α →ₘ[μ] E') : α → E') - (↑(↑g : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0

Tactic:
exact (Lp.coeFn_sub f g).symm.trans h_sub

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Lp.coeFn_sub, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
suffices : (↑(↑(f - g) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0
⊢ (↑(↑f : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] (↑(↑g : α →ₘ[μ] E') : α → E')

Tactic:
suffices h_sub : ⇑(f - g) =ᵐ[μ] 0 by
    rw [← sub_ae_eq_zero]; exact (Lp.coeFn_sub f g).symm.trans h_sub
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : Eq.{u_2 + 1} (α := E') (∫ (a : α) in s, ((↑(↑f : α →ₘ[μ] E') : α → E') - (↑(↑g : α →ₘ[μ] E') : α → E')) a ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(f - g) : α →ₘ[μ] E') : α → E') x ∂μ) 0

Tactic:
rw [integral_congr_ae (ae_restrict_of_ae (Lp.coeFn_sub f g))]

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.ae_restrict_of_ae, MeasureTheory.Lp.coeFn_sub
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  HSub.hSub (α := E') (∫ (a : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') a ∂μ)
      (∫ (a : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') a ∂μ) =
    0
⊢ Eq.{u_2 + 1} (α := E') (∫ (a : α) in s, ((↑(↑f : α →ₘ[μ] E') : α → E') - (↑(↑g : α →ₘ[μ] E') : α → E')) a ∂μ) 0

Tactic:
rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)]

Premises used: MeasureTheory.integral_sub'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HSub.hSub (α := E') (∫ (a : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') a ∂μ)
      (∫ (a : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') a ∂μ) =
    0

Tactic:
sub_eq_zero.mpr (hfg s hs hμs)

Premises used: Iff.mpr, sub_eq_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HSub.hSub (α := E') (∫ (a : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') a ∂μ)
      (∫ (a : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') a ∂μ) =
    0

Tactic:
exact sub_eq_zero.mpr (hfg s hs hμs)

Premises used: Iff.mpr, sub_eq_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
⊢ ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(f - g) : α →ₘ[μ] E') : α → E') x ∂μ) 0

Tactic:
have hfg' : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 := by
    intro s hs hμs
    rw [integral_congr_ae (ae_restrict_of_ae (Lp.coeFn_sub f g))]
    rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)]
    exact sub_eq_zero.mpr (hfg s hs hμs)
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E'
inst_2 : InnerProductSpace 𝕜 E'
inst_3 : CompleteSpace E'
inst_4 : NormedSpace ℝ E'
hm : m ≤ m0
f g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑f : α →ₘ[μ] E') : α → E') s μ
hg_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (↑(↑g : α →ₘ[μ] E') : α → E') s μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E') : α → E') x ∂μ)
          (∫ (x : α) in s, (↑(↑g : α →ₘ[μ] E') : α → E') x ∂μ)
hf_meas : AEStronglyMeasurable (↑(↑f : α →ₘ[μ] E') : α → E') μ
hg_meas : AEStronglyMeasurable (↑(↑g : α →ₘ[μ] E') : α → E') μ
hfg' :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E') (∫ (x : α) in s, (↑(↑(f - g) : α →ₘ[μ] E') : α → E') x ∂μ) 0
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : Integrable ((↑(↑f : α →ₘ[μ] E') : α → E') - (↑(↑g : α →ₘ[μ] E') : α → E')) (μ.restrict s)
⊢ IntegrableOn (↑(↑(f - g) : α →ₘ[μ] E') : α → E') s μ

Tactic:
rw [IntegrableOn, integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub f g))]

Premises used: MeasureTheory.integrable_congr, MeasureTheory.IntegrableOn, MeasureTheory.ae_restrict_of_ae, MeasureTheory.Lp.coeFn_sub