awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
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∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
have hμs₁ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [trim_measurableSet_eq hm hs] at hμs
Cleared hypotheses: hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
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∞)
⊢ IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
have rw : Integrable (AEStronglyMeasurable.mk g hgm) ((μ.restrict s).trim hm)
Tactic: rw [IntegrableOn, restrict_trim hm _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
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).trim hm)
have refine : Integrable (AEStronglyMeasurable.mk g hgm) (μ.restrict s)
Tactic: refine Integrable.trim hm ?_ hgm.stronglyMeasurable_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
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)
⊢ AEStronglyMeasurable.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable.mk g hgm
have 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)
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
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∞)
⊢ 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)
have hμs₁ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [trim_measurableSet_eq hm hs] at hμs
Cleared hypotheses: hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
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') (∫ (x : α) in s, AEStronglyMeasurable.mk f hfm x ∂μ.trim hm)
    (∫ (x : α) in s, AEStronglyMeasurable.mk g hgm x ∂μ.trim hm)
have rw : Eq.{u_3 + 1} (α := F') (∫ (a : α) in s, f a ∂μ) (∫ (a : α) in s, g a ∂μ)
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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
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)
⊢ AEStronglyMeasurable.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable.mk g hgm
have 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)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
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∞)
⊢ LE.le (α := ℝ) (∫ (x : α) in s, ‖g x‖ ∂μ) (∫ (x : α) in s, ‖f x‖ ∂μ)
have 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)
Tactic: rw [integral_norm_eq_pos_sub_neg hgi, integral_norm_eq_pos_sub_neg hfi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
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∞)
⊢ 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)
have h_meas_nonneg_g : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
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}
⊢ 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)
have h_meas_nonneg_f : MeasurableSet.{u_1} (α := α) {x : α | 0 ≤ f x}
Tactic: have h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x} :=
    stronglyMeasurable_const.measurableSet_le hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
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}
⊢ 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)
have h_meas_nonpos_g : 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 _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (hypothesis)
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}
⊢ 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)
have h_meas_nonpos_f : MeasurableSet.{u_1} (α := α) {x : α | f x ≤ 0}
Tactic: have h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0} :=
    hf.measurableSet_le stronglyMeasurable_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
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)
have refine_1 : LE.le (α := ℝ) (∫ (x : α) in {x : α | 0 ≤ g x}, g x ∂μ.restrict s) (∫ (x : α) in {x : α | 0 ≤ f x}, f x ∂μ.restrict s)
Tactic: refine sub_le_sub ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
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)
⊢ 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)
have refine_2 : LE.le (α := ℝ) (∫ (x : α) in {x : α | f x ≤ 0}, f x ∂μ.restrict s) (∫ (x : α) in {x : α | g x ≤ 0}, g x ∂μ.restrict s)
Tactic: refine sub_le_sub ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
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}
⊢ LE.le (α := ℝ) (∫ (x : α) in {x : α | 0 ≤ g x}, g x ∂μ.restrict s) (∫ (x : α) in {x : α | 0 ≤ f x}, f x ∂μ.restrict s)
have refine_1 : LE.le (α := ℝ) (∫ (x : α) in {x : α | 0 ≤ g x}, f x ∂μ.restrict s) (∫ (x : α) in {x : α | 0 ≤ f x}, f x ∂μ.restrict s)
Tactic: rw [Measure.restrict_restrict (hm _ h_meas_nonneg_g), Measure.restrict_restrict h_meas_nonneg_f,
      hgf _ (@MeasurableSet.inter α m _ _ h_meas_nonneg_g hs)
        ((measure_mono Set.inter_subset_right).trans_lt (lt_top_iff_ne_top.mpr hμs)),
      ← Measure.restrict_restrict (hm _ h_meas_nonneg_g), ←
      Measure.restrict_restrict h_meas_nonneg_f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
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}
⊢ LE.le (α := ℝ) (∫ (x : α) in {x : α | f x ≤ 0}, f x ∂μ.restrict s) (∫ (x : α) in {x : α | g x ≤ 0}, g x ∂μ.restrict s)
have refine_2 : LE.le (α := ℝ) (∫ (x : α) in {x : α | f x ≤ 0}, f x ∂μ.restrict s) (∫ (x : α) in {x : α | g x ≤ 0}, f x ∂μ.restrict s)
Tactic: rw [Measure.restrict_restrict (hm _ h_meas_nonpos_g), Measure.restrict_restrict h_meas_nonpos_f,
      hgf _ (@MeasurableSet.inter α m _ _ h_meas_nonpos_g hs)
        ((measure_mono Set.inter_subset_right).trans_lt (lt_top_iff_ne_top.mpr hμs)),
      ← Measure.restrict_restrict (hm _ h_meas_nonpos_g), ←
      Measure.restrict_restrict h_meas_nonpos_f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
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∞)
⊢ ∫⁻ (x : α) in s, ‖g x‖ₑ ∂μ ≤ ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ
have rw : LE.le (α := ℝ) (∫ (x : α) in s, ‖g x‖ ∂μ) (∫ (x : α) in s, ‖f x‖ ∂μ)
Tactic: rw [← ofReal_integral_norm_eq_lintegral_enorm hfi, ←
    ofReal_integral_norm_eq_lintegral_enorm hgi, ENNReal.ofReal_le_ofReal_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique (goal)
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 : LE.le (α := ℝ) (∫ (x : α) in s, ‖g x‖ ∂μ) (∫ (x : α) in s, ‖f x‖ ∂μ)
⊢ ∫⁻ (x : α) in s, ‖g x‖ₑ ∂μ ≤ ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ
have rw₁ : LE.le (α := ℝ) 0 (∫ (x : α) in s, ‖f x‖ ∂μ)
Tactic: rw [← ofReal_integral_norm_eq_lintegral_enorm hfi, ←
    ofReal_integral_norm_eq_lintegral_enorm hgi, ENNReal.ofReal_le_ofReal_iff]