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 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∞)
⊢ Integrable ((↑(↑f : α →ₘ[μ] E') : α → E') - (↑(↑g : α →ₘ[μ] E') : α → E')) (μ.restrict s)

Tactic:
(hf_int_finite s hs hμs).sub (hg_int_finite s hs hμs)

Premises used: MeasureTheory.IntegrableOn.sub, MeasureTheory.IntegrableOn
-- 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∞)
⊢ Integrable ((↑(↑f : α →ₘ[μ] E') : α → E') - (↑(↑g : α →ₘ[μ] E') : α → E')) (μ.restrict s)

Tactic:
exact (hf_int_finite s hs hμs).sub (hg_int_finite s hs hμs)

Premises used: MeasureTheory.IntegrableOn.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') μ
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 α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(f - g) : α →ₘ[μ] E') : α → E') s μ

Tactic:
have hfg_int : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn (⇑(f - g)) s μ := by
    intro s hs hμs
    rw [IntegrableOn, integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub f g))]
    exact (hf_int_finite s hs hμs).sub (hg_int_finite 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
hfg_int :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(f - g) : α →ₘ[μ] E') : α → E') s μ
⊢ (↑(↑(f - g) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0

Tactic:
Lp.ae_eq_zero_of_forall_setIntegral_eq_zero' 𝕜 hm (f - g) hp_ne_zero hp_ne_top hfg_int hfg'
    <| (hf_meas.sub hg_meas).congr (Lp.coeFn_sub f g).symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero', MeasureTheory.AEStronglyMeasurable.sub, HSub.hSub, 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') μ
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
hfg_int :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (↑(↑(f - g) : α →ₘ[μ] E') : α → E') s μ
⊢ (↑(↑(f - g) : α →ₘ[μ] E') : α → E') =ᶠ[ae μ] 0

Tactic:
exact Lp.ae_eq_zero_of_forall_setIntegral_eq_zero' 𝕜 hm (f - g) hp_ne_zero hp_ne_top hfg_int hfg'
    <| (hf_meas.sub hg_meas).congr (Lp.coeFn_sub f g).symm

Premises used: MeasureTheory.AEStronglyMeasurable.congr, MeasureTheory.Lp.ae_eq_zero_of_forall_setIntegral_eq_zero', MeasureTheory.AEStronglyMeasurable.sub, HSub.hSub, MeasureTheory.Lp.coeFn_sub, Filter.EventuallyEq.symm
-- 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 μ
rw : AEStronglyMeasurable.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable.mk g hgm
⊢ f =ᶠ[ae μ] g

Tactic:
rw [← ae_eq_trim_iff_of_aestronglyMeasurable hm hfm hgm]

Premises used: MeasureTheory.ae_eq_trim_iff_of_aestronglyMeasurable
-- 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 μ
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 μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : Integrable (AEStronglyMeasurable.mk f hfm) ((μ.restrict s).trim hm)
⊢ IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)

Tactic:
rw [IntegrableOn, restrict_trim hm _ hs]

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.restrict_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 μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable (AEStronglyMeasurable.mk f hfm) ((μ.restrict s).trim hm)

Tactic:
Integrable.trim hm ?_ hfm.stronglyMeasurable_mk

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.Integrable.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 μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine : Integrable (AEStronglyMeasurable.mk f hfm) (μ.restrict s)
⊢ Integrable (AEStronglyMeasurable.mk f hfm) ((μ.restrict s).trim hm)

Tactic:
refine Integrable.trim hm ?_ hfm.stronglyMeasurable_mk

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.Integrable.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 μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable (AEStronglyMeasurable.mk f hfm) (μ.restrict s)

Tactic:
Integrable.congr (hf_int_finite s hs hμs) (ae_restrict_of_ae hfm.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 μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable (AEStronglyMeasurable.mk f hfm) (μ.restrict s)

Tactic:
exact Integrable.congr (hf_int_finite s hs hμs) (ae_restrict_of_ae hfm.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 μ
⊢ ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)

Tactic:
have hf_mk_int_finite (s) :
      MeasurableSet[m] s → μ.trim hm s < ∞ → @IntegrableOn _ _ m _ _ (hfm.mk f) 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 ?_ hfm.stronglyMeasurable_mk
    exact Integrable.congr (hf_int_finite s hs hμs) (ae_restrict_of_ae hfm.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)
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)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : Integrable (AEStronglyMeasurable.mk g hgm) ((μ.restrict s).trim hm)
⊢ IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)

Tactic:
rw [IntegrableOn, restrict_trim hm _ hs]

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.restrict_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)
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)

Tactic:
Integrable.trim hm ?_ hgm.stronglyMeasurable_mk

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.Integrable.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)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine : Integrable (AEStronglyMeasurable.mk g hgm) (μ.restrict s)
⊢ Integrable (AEStronglyMeasurable.mk g hgm) ((μ.restrict s).trim hm)

Tactic:
refine Integrable.trim hm ?_ hgm.stronglyMeasurable_mk

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.Integrable.trim