awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
refine :
  ∀ (s : Set α) (hs : MeasurableSet s),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, (g - f) x ∂μ)
⊢ 0 ≤ᶠ[ae μ] g - f

Tactic:
refine ae_nonneg_of_forall_setIntegral_nonneg (hg.sub hf) fun s hs => ?_

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
s : Set α
hs : MeasurableSet s
rw :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    LE.le (α := ℝ) (∫ (a : α) in s, f a ∂μ) (∫ (a : α) in s, g a ∂μ)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, (g - f) x ∂μ)

Tactic:
rw [integral_sub' hg.integrableOn hf.integrableOn, sub_nonneg]

Premises used: MeasureTheory.integral_sub', MeasureTheory.Integrable.integrableOn, sub_nonneg
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
s : Set α
hs : MeasurableSet s
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    LE.le (α := ℝ) (∫ (a : α) in s, f a ∂μ) (∫ (a : α) in s, g a ∂μ)

Tactic:
hf_le s hs
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
s : Set α
hs : MeasurableSet s
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    LE.le (α := ℝ) (∫ (a : α) in s, f a ∂μ) (∫ (a : α) in s, g a ∂μ)

Tactic:
exact hf_le s hs
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
⊢ 0 ≤ᶠ[ae (μ.restrict t)] f

Tactic:
ae_nonneg_of_forall_setIntegral_nonneg hf fun s hs h's => ?_

Premises used: MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
refine :
  ∀ (s : Set α) (hs : MeasurableSet s)
    (h's : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ.restrict t)
⊢ 0 ≤ᶠ[ae (μ.restrict t)] f

Tactic:
refine ae_nonneg_of_forall_setIntegral_nonneg hf fun s hs h's => ?_

Premises used: MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
s : Set α
hs : MeasurableSet s
h's : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
simp_rw : LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ.restrict t)

Tactic:
simp_rw [Measure.restrict_restrict hs]

Premises used: MeasureTheory.Measure.restrict_restrict
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
s : Set α
hs : MeasurableSet s
h's : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
apply : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)

Tactic:
apply hf_zero s hs
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
s : Set α
hs : MeasurableSet s
h's : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h's : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [Measure.restrict_apply hs] at h's

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∀ᵐ (x : α) ∂μ.restrict s, 0 x ≤ f x
⊢ 0 ≤ᶠ[ae μ] f

Tactic:
apply ae_of_forall_measure_lt_top_ae_restrict

Premises used: MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α
t_meas : MeasurableSet t
t_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
⊢ ∀ᵐ (x : α) ∂μ.restrict t, 0 x ≤ f x

Tactic:
apply ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter (hf_int_finite t t_meas t_lt_top)

Premises used: MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α
t_meas : MeasurableSet t
t_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
s_meas : MeasurableSet s
h :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α
t_meas : MeasurableSet t
t_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
s_meas : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)

Tactic:
hf_zero _ (s_meas.inter t_meas)
      (lt_of_le_of_lt (measure_mono (Set.inter_subset_right)) t_lt_top)

Premises used: lt_of_le_of_lt, MeasureTheory.measure_mono, Set.inter_subset_right, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α
t_meas : MeasurableSet t
t_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
s_meas : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)

Tactic:
exact
    hf_zero _ (s_meas.inter t_meas)
      (lt_of_le_of_lt (measure_mono (Set.inter_subset_right)) t_lt_top)

Premises used: lt_of_le_of_lt, MeasureTheory.measure_mono, Set.inter_subset_right, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
suffices : 0 ≤ᶠ[ae (μ.restrict t)] f
⊢ 0 ≤ᶠ[ae μ] f

Tactic:
suffices 0 ≤ᵐ[μ.restrict t] f from
    ae_of_ae_restrict_of_ae_restrict_compl _ this hf.ae_eq_zero_compl.symm.le
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
⊢ SigmaFinite (μ.restrict t)

Tactic:
haveI : SigmaFinite (μ.restrict t) := hf.sigmaFinite_restrict
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
⊢ 0 ≤ᶠ[ae (μ.restrict t)] f

Tactic:
ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite (fun s hs hμts => ?_) fun s hs hμts => ?_

Premises used: MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
refine_1 :
  ∀ (s : Set α) (hs : MeasurableSet s)
    (hμts : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    IntegrableOn f s (μ.restrict t)
refine_2 :
  ∀ (s : Set α) (hs : MeasurableSet s)
    (hμts : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ.restrict t)
⊢ 0 ≤ᶠ[ae (μ.restrict t)] f

Tactic:
refine
    ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite (fun s hs hμts => ?_) fun s hs hμts => ?_

Premises used: MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg_of_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμts : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 : Integrable f (μ.restrict (s ∩ t))
⊢ IntegrableOn f s (μ.restrict t)

Tactic:
rw [IntegrableOn, Measure.restrict_restrict hs]

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Measure.restrict_restrict
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμts : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply hs] at hμts

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμts : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable f (μ.restrict (s ∩ t))

Tactic:
hf_int_finite (s ∩ t) (hs.inter hf.measurableSet) hμts

Premises used: MeasureTheory.AEFinStronglyMeasurable.measurableSet, MeasureTheory.IntegrableOn, Inter.inter, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμts : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable f (μ.restrict (s ∩ t))

Tactic:
exact hf_int_finite (s ∩ t) (hs.inter hf.measurableSet) hμts

Premises used: MeasureTheory.AEFinStronglyMeasurable.measurableSet, Inter.inter, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμts : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 : LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ.restrict t)

Tactic:
rw [Measure.restrict_restrict hs]

Premises used: MeasureTheory.Measure.restrict_restrict
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμts : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)

Tactic:
hf_zero (s ∩ t) (hs.inter hf.measurableSet) hμts

Premises used: MeasureTheory.AEFinStronglyMeasurable.measurableSet, Inter.inter, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμts : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)

Tactic:
exact hf_zero (s ∩ t) (hs.inter hf.measurableSet) hμts

Premises used: MeasureTheory.AEFinStronglyMeasurable.measurableSet, Inter.inter, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 0 ≤ᶠ[ae (μ.restrict t)] f

Tactic:
ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter
      (hf_int_finite t ht (lt_top_iff_ne_top.mpr hμt)) fun s hs _ => ?_

Premises used: Iff.mpr, lt_top_iff_ne_top, MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
t₁ :
  ∀ (s : Set α) (hs : MeasurableSet s),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) →
      LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
⊢ 0 ≤ᶠ[ae (μ.restrict t)] f

Tactic:
refine
    ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter
      (hf_int_finite t ht (lt_top_iff_ne_top.mpr hμt)) fun s hs _ => ?_

Premises used: Iff.mpr, lt_top_iff_ne_top, MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)

Tactic:
hf_zero (s ∩ t) (hs.inter ht) ?_

Premises used: Inter.inter, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h refine : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)

Tactic:
refine hf_zero (s ∩ t) (hs.inter ht) ?_

Premises used: Inter.inter, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono Set.inter_subset_right).trans_lt (lt_top_iff_ne_top.mpr hμt)

Premises used: Iff.mpr, lt_top_iff_ne_top, MeasureTheory.measure_mono, LE.le.trans_lt, Set.inter_subset_right