awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable (AEStronglyMeasurable.mk g hgm) (μ.restrict s)

Tactic:
Integrable.congr (hg_int_finite s hs hμs) (ae_restrict_of_ae hgm.ae_eq_mk)

Premises used: MeasureTheory.ae_restrict_of_ae, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.Integrable.congr
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable (AEStronglyMeasurable.mk g hgm) (μ.restrict s)

Tactic:
exact Integrable.congr (hg_int_finite s hs hμs) (ae_restrict_of_ae hgm.ae_eq_mk)

Premises used: MeasureTheory.ae_restrict_of_ae, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.Integrable.congr
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
⊢ ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)

Tactic:
have hg_mk_int_finite (s) :
      MeasurableSet[m] s → μ.trim hm s < ∞ → @IntegrableOn _ _ m _ _ (hgm.mk g) s (μ.trim hm) := by
    intro hs hμs
    rw [trim_measurableSet_eq hm hs] at hμs
    rw [IntegrableOn, restrict_trim hm _ hs]
    refine Integrable.trim hm ?_ hgm.stronglyMeasurable_mk
    exact Integrable.congr (hg_int_finite s hs hμs) (ae_restrict_of_ae hgm.ae_eq_mk)
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [trim_measurableSet_eq hm hs] at hμs

Premises used: MeasureTheory.trim_measurableSet_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : Eq.{u_3 + 1} (α := F') (∫ (a : α) in s, f a ∂μ) (∫ (a : α) in s, g a ∂μ)
⊢ Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, AEStronglyMeasurable.mk f hfm x ∂μ.trim hm)
    (∫ (x : α) in s, AEStronglyMeasurable.mk g hgm x ∂μ.trim hm)

Tactic:
rw [restrict_trim hm _ hs, ← integral_trim hm hfm.stronglyMeasurable_mk, ←
      integral_trim hm hgm.stronglyMeasurable_mk,
      integral_congr_ae (ae_restrict_of_ae hfm.ae_eq_mk.symm),
      integral_congr_ae (ae_restrict_of_ae hgm.ae_eq_mk.symm)]

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.ae_restrict_of_ae, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.restrict_trim, Filter.EventuallyEq.symm, MeasureTheory.integral_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := F') (∫ (a : α) in s, f a ∂μ) (∫ (a : α) in s, g a ∂μ)

Tactic:
hfg_eq s hs hμs
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := F') (∫ (a : α) in s, f a ∂μ) (∫ (a : α) in s, g a ∂μ)

Tactic:
exact hfg_eq s hs hμs
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
⊢ ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, AEStronglyMeasurable.mk f hfm x ∂μ.trim hm)
          (∫ (x : α) in s, AEStronglyMeasurable.mk g hgm x ∂μ.trim hm)

Tactic:
have hfg_mk_eq :
    ∀ s : Set α,
      MeasurableSet[m] s →
        μ.trim hm s < ∞ → ∫ x in s, hfm.mk f x ∂μ.trim hm = ∫ x in s, hgm.mk g x ∂μ.trim hm := by
    intro s hs hμs
    rw [trim_measurableSet_eq hm hs] at hμs
    rw [restrict_trim hm _ hs, ← integral_trim hm hfm.stronglyMeasurable_mk, ←
      integral_trim hm hgm.stronglyMeasurable_mk,
      integral_congr_ae (ae_restrict_of_ae hfm.ae_eq_mk.symm),
      integral_congr_ae (ae_restrict_of_ae hgm.ae_eq_mk.symm)]
    exact hfg_eq s hs hμs
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
hfg_mk_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, AEStronglyMeasurable.mk f hfm x ∂μ.trim hm)
          (∫ (x : α) in s, AEStronglyMeasurable.mk g hgm x ∂μ.trim hm)
⊢ AEStronglyMeasurable.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable.mk g hgm

Tactic:
ae_eq_of_forall_setIntegral_eq_of_sigmaFinite hf_mk_int_finite hg_mk_int_finite hfg_mk_eq

Premises used: MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F'
inst_1 : NormedSpace ℝ F'
inst_2 : CompleteSpace F'
hm : m ≤ m0
inst_3 : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
hfg_mk_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := F') (∫ (x : α) in s, AEStronglyMeasurable.mk f hfm x ∂μ.trim hm)
          (∫ (x : α) in s, AEStronglyMeasurable.mk g hgm x ∂μ.trim hm)
⊢ AEStronglyMeasurable.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable.mk g hgm

Tactic:
exact ae_eq_of_forall_setIntegral_eq_of_sigmaFinite hf_mk_int_finite hg_mk_int_finite hfg_mk_eq

Premises used: MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  HSub.hSub (α := ℝ) (∫ (x : α) in {x : α | 0 ≤ g x}, g x ∂μ.restrict s)
      (∫ (x : α) in {x : α | g x ≤ 0}, g x ∂μ.restrict s) ≤
    HSub.hSub (α := ℝ) (∫ (x : α) in {x : α | 0 ≤ f x}, f x ∂μ.restrict s)
      (∫ (x : α) in {x : α | f x ≤ 0}, f x ∂μ.restrict s)
⊢ LE.le (α := ℝ) (∫ (x : α) in s, ‖g x‖ ∂μ) (∫ (x : α) in s, ‖f x‖ ∂μ)

Tactic:
rw [integral_norm_eq_pos_sub_neg hgi, integral_norm_eq_pos_sub_neg hfi]

Premises used: MeasureTheory.integral_norm_eq_pos_sub_neg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ g x}

Tactic:
have h_meas_nonneg_g : MeasurableSet[m] {x | 0 ≤ g x} :=
    (@stronglyMeasurable_const _ _ m _ _).measurableSet_le hg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas_nonneg_g : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ g x}
⊢ MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ f x}

Tactic:
have h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x} :=
    stronglyMeasurable_const.measurableSet_le hf
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas_nonneg_g : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ f x}
⊢ MeasurableSet.{u_1} (α := α) {x : α | g x ≤ 0}

Tactic:
have h_meas_nonpos_g : MeasurableSet[m] {x | g x ≤ 0} :=
    hg.measurableSet_le (@stronglyMeasurable_const _ _ m _ _)
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas_nonneg_g : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet.{u_1} (α := α) {x : α | g x ≤ 0}
⊢ MeasurableSet.{u_1} (α := α) {x : α | f x ≤ 0}

Tactic:
have h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0} :=
    hf.measurableSet_le stronglyMeasurable_const
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas_nonneg_g : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet.{u_1} (α := α) {x : α | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ 0}
⊢ HSub.hSub (α := ℝ) (∫ (x : α) in {x : α | 0 ≤ g x}, g x ∂μ.restrict s)
      (∫ (x : α) in {x : α | g x ≤ 0}, g x ∂μ.restrict s) ≤
    HSub.hSub (α := ℝ) (∫ (x : α) in {x : α | 0 ≤ f x}, f x ∂μ.restrict s)
      (∫ (x : α) in {x : α | f x ≤ 0}, f x ∂μ.restrict s)

Tactic:
sub_le_sub ?_ ?_

Premises used: sub_le_sub
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f g : α → ℝ
hf : StronglyMeasurable f
hfi : IntegrableOn f s μ
hg : StronglyMeasurable g
hgi : IntegrableOn g s μ
hgf :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, f x ∂μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_meas_nonneg_g : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ g x}
h_meas_nonneg_f : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ f x}
h_meas_nonpos_g : MeasurableSet.{u_1} (α := α) {x : α | g x ≤ 0}
h_meas_nonpos_f : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ 0}
refine_1 :
  LE.le (α := ℝ) (∫ (x : α) in {x : α | 0 ≤ g x}, g x ∂μ.restrict s) (∫ (x : α) in {x : α | 0 ≤ f x}, f x ∂μ.restrict s)
refine_2 :
  LE.le (α := ℝ) (∫ (x : α) in {x : α | f x ≤ 0}, f x ∂μ.restrict s) (∫ (x : α) in {x : α | g x ≤ 0}, g x ∂μ.restrict s)
⊢ HSub.hSub (α := ℝ) (∫ (x : α) in {x : α | 0 ≤ g x}, g x ∂μ.restrict s)
      (∫ (x : α) in {x : α | g x ≤ 0}, g x ∂μ.restrict s) ≤
    HSub.hSub (α := ℝ) (∫ (x : α) in {x : α | 0 ≤ f x}, f x ∂μ.restrict s)
      (∫ (x : α) in {x : α | f x ≤ 0}, f x ∂μ.restrict s)

Tactic:
refine sub_le_sub ?_ ?_

Premises used: sub_le_sub