awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x : X | R < f x} μ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞) (0 : ℝ≥0∞)
this : IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ
⊢ IntegrableOn (ε := ℝ) (fun (a : X) ↦ f a - R) {x : X | R < f x} μ

Tactic:
Integrable.sub hfint this

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x : X | R < f x} μ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞) (0 : ℝ≥0∞)
this : IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ
⊢ IntegrableOn (ε := ℝ) (fun (a : X) ↦ f a - R) {x : X | R < f x} μ

Tactic:
exact Integrable.sub hfint this

Premises used: MeasureTheory.Integrable.sub
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
f : X → E
hf_meas : StronglyMeasurable f
s : Set X
hs : MeasurableSet s
rwa : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂(μ.restrict s).trim hm) (∫ (x : X) in s, f x ∂μ.trim hm)
rwa₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂(μ.restrict s).trim hm) (∫ (x : X), f x ∂(μ.restrict s).trim hm)
rwa₂ : MeasurableSet s
rwa₃ : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂(μ.restrict s).trim hm) (∫ (x : X), f x ∂(μ.restrict s).trim hm)
rwa₄ rwa₅ rwa₆ : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, f x ∂μ.trim hm)

Tactic:
rwa [integral_trim hm hf_meas, restrict_trim hm μ]

Premises used: MeasureTheory.restrict_trim, MeasureTheory.integral_trim
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x y : X
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Icc x y, f t ∂μ) (∫ (t : X) in Ioc x y, f t ∂μ)

Tactic:
setIntegral_congr_set (Ioc_ae_eq_Icc' hx).symm

Premises used: MeasureTheory.Ioc_ae_eq_Icc', MeasureTheory.setIntegral_congr_set, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x y : X
hy : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {y} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Icc x y, f t ∂μ) (∫ (t : X) in Ico x y, f t ∂μ)

Tactic:
setIntegral_congr_set (Ico_ae_eq_Icc' hy).symm

Premises used: MeasureTheory.Ico_ae_eq_Icc', MeasureTheory.setIntegral_congr_set, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x y : X
hy : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {y} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ioc x y, f t ∂μ) (∫ (t : X) in Ioo x y, f t ∂μ)

Tactic:
setIntegral_congr_set (Ioo_ae_eq_Ioc' hy).symm

Premises used: MeasureTheory.setIntegral_congr_set, Filter.EventuallyEq.symm, MeasureTheory.Ioo_ae_eq_Ioc'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x y : X
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ico x y, f t ∂μ) (∫ (t : X) in Ioo x y, f t ∂μ)

Tactic:
setIntegral_congr_set (Ioo_ae_eq_Ico' hx).symm

Premises used: MeasureTheory.Ioo_ae_eq_Ico', MeasureTheory.setIntegral_congr_set, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x y : X
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
hy : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {y} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Icc x y, f t ∂μ) (∫ (t : X) in Ioo x y, f t ∂μ)

Tactic:
setIntegral_congr_set (Ioo_ae_eq_Icc' hx hy).symm

Premises used: MeasureTheory.Ioo_ae_eq_Icc', MeasureTheory.setIntegral_congr_set, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x : X
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Iic x, f t ∂μ) (∫ (t : X) in Iio x, f t ∂μ)

Tactic:
setIntegral_congr_set (Iio_ae_eq_Iic' hx).symm

Premises used: MeasureTheory.Iio_ae_eq_Iic', MeasureTheory.setIntegral_congr_set, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x : X
hx : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ici x, f t ∂μ) (∫ (t : X) in Ioi x, f t ∂μ)

Tactic:
setIntegral_congr_set (Ioi_ae_eq_Ici' hx).symm

Premises used: MeasureTheory.setIntegral_congr_set, MeasureTheory.Ioi_ae_eq_Ici', Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x y : X
inst_3 : NoAtoms μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Icc x y, f t ∂μ) (∫ (t : X) in Ioc x y, f t ∂μ)

Tactic:
integral_Icc_eq_integral_Ioc' <| measure_singleton x

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.integral_Icc_eq_integral_Ioc'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x y : X
inst_3 : NoAtoms μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Icc x y, f t ∂μ) (∫ (t : X) in Ico x y, f t ∂μ)

Tactic:
integral_Icc_eq_integral_Ico' <| measure_singleton y

Premises used: MeasureTheory.integral_Icc_eq_integral_Ico', MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x y : X
inst_3 : NoAtoms μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ioc x y, f t ∂μ) (∫ (t : X) in Ioo x y, f t ∂μ)

Tactic:
integral_Ioc_eq_integral_Ioo' <| measure_singleton y

Premises used: MeasureTheory.integral_Ioc_eq_integral_Ioo', MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x y : X
inst_3 : NoAtoms μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ico x y, f t ∂μ) (∫ (t : X) in Ioo x y, f t ∂μ)

Tactic:
integral_Ico_eq_integral_Ioo' <| measure_singleton x

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.integral_Ico_eq_integral_Ioo'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x y : X
inst_3 : NoAtoms μ
rw : Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ioo x y, f t ∂μ) (∫ (t : X) in Ioc x y, f t ∂μ)
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ioo x y, f t ∂μ) (∫ (t : X) in Ioo x y, f t ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ico x y, f t ∂μ) (∫ (t : X) in Ioc x y, f t ∂μ)

Tactic:
rw [integral_Ico_eq_integral_Ioo, integral_Ioc_eq_integral_Ioo]

Premises used: MeasureTheory.integral_Ioc_eq_integral_Ioo, MeasureTheory.integral_Ico_eq_integral_Ioo
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x y : X
inst_3 : NoAtoms μ
rw : Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ico x y, f t ∂μ) (∫ (t : X) in Ioo x y, f t ∂μ)
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ioo x y, f t ∂μ) (∫ (t : X) in Ioo x y, f t ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Icc x y, f t ∂μ) (∫ (t : X) in Ioo x y, f t ∂μ)

Tactic:
rw [integral_Icc_eq_integral_Ico, integral_Ico_eq_integral_Ioo]

Premises used: MeasureTheory.integral_Ico_eq_integral_Ioo, MeasureTheory.integral_Icc_eq_integral_Ico
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x : X
inst_3 : NoAtoms μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Iic x, f t ∂μ) (∫ (t : X) in Iio x, f t ∂μ)

Tactic:
integral_Iic_eq_integral_Iio' <| measure_singleton x

Premises used: MeasureTheory.integral_Iic_eq_integral_Iio', MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
inst_2 : PartialOrder X
x : X
inst_3 : NoAtoms μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (t : X) in Ici x, f t ∂μ) (∫ (t : X) in Ioi x, f t ∂μ)

Tactic:
integral_Ici_eq_integral_Ioi' <| measure_singleton x

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.integral_Ici_eq_integral_Ioi'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f : X → E
s t : Set X
inst_5 : OrderClosedTopology E
hfi : IntegrableOn f t μ
hf : 0 ≤ᶠ[ae (μ.restrict t)] f
hst : s ≤ᶠ[ae μ] t
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in t, f x ∂μ)

Tactic:
integral_mono_measure (Measure.restrict_mono_ae hst) hf hfi

Premises used: MeasureTheory.Measure.restrict_mono_ae, MeasureTheory.integral_mono_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f : X → E
s : Set X
inst_5 : OrderClosedTopology E
hfi : Integrable f μ
hf : 0 ≤ᶠ[ae μ] f
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X), f x ∂μ)

Tactic:
integral_mono_measure (Measure.restrict_le_self) hf hfi

Premises used: MeasureTheory.integral_mono_measure, MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
h : f ≤ᶠ[ae (μ.restrict s)] g
pos : ∀ (hE : CompleteSpace E), LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)
neg : ∀ (hE : ¬CompleteSpace E), LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
h : f ≤ᶠ[ae (μ.restrict s)] g
hE : CompleteSpace E
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)

Tactic:
integral_mono_ae hf hg h

Premises used: MeasureTheory.integral_mono_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
h : f ≤ᶠ[ae (μ.restrict s)] g
hE : CompleteSpace E
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)

Tactic:
exact integral_mono_ae hf hg h

Premises used: MeasureTheory.integral_mono_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
h : f ≤ᶠ[ae (μ.restrict s)] g
hE : ¬CompleteSpace E
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)

Tactic:
simp [integral, hE]

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
h : f ≤ᶠ[ae μ] g
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)

Tactic:
setIntegral_mono_ae_restrict hf hg (ae_restrict_of_ae h)

Premises used: MeasureTheory.ae_restrict_of_ae, MeasureTheory.setIntegral_mono_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : MeasurableSet s
h : ∀ x ∈ s, f x ≤ g x
⊢ f ≤ᶠ[ae (μ.restrict s)] g

Tactic:
simp [hs, EventuallyLE, eventually_inf_principal, ae_of_all _ h]

Premises used: Filter.eventually_inf_principal, MeasureTheory.ae_of_all, Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)

Tactic:
setIntegral_mono_ae_restrict hf hg ?_

Premises used: MeasureTheory.setIntegral_mono_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
refine : f ≤ᶠ[ae (μ.restrict s)] g
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)

Tactic:
refine setIntegral_mono_ae_restrict hf hg ?_

Premises used: MeasureTheory.setIntegral_mono_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
rwa : ∀ᵐ (x : X) ∂μ.restrict s, f x ≤ g x
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ f ≤ᶠ[ae (μ.restrict s)] g

Tactic:
rwa [EventuallyLE, ae_restrict_iff' hs]

Premises used: MeasureTheory.ae_restrict_iff', Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
rw : LE.le.{u_3} (α := E) (∫ (x : X) in toMeasurable μ s, f x ∂μ) (∫ (x : X) in toMeasurable μ s, g x ∂μ)
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)

Tactic:
rw [setIntegral_congr_set hs.toMeasurable_ae_eq.symm,
    setIntegral_congr_set hs.toMeasurable_ae_eq.symm]

Premises used: MeasureTheory.setIntegral_congr_set, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in toMeasurable μ s, f x ∂μ) (∫ (x : X) in toMeasurable μ s, g x ∂μ)

Tactic:
setIntegral_mono_on_ae ?_ ?_ ?_ ?_

Premises used: MeasureTheory.setIntegral_mono_on_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
refine_1 : IntegrableOn f (toMeasurable μ s) μ
refine_2 : IntegrableOn g (toMeasurable μ s) μ
refine_3 : MeasurableSet (toMeasurable μ s)
refine_4 : ∀ᵐ (x : X) ∂μ, x ∈ toMeasurable μ s → f x ≤ g x
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in toMeasurable μ s, f x ∂μ) (∫ (x : X) in toMeasurable μ s, g x ∂μ)

Tactic:
refine setIntegral_mono_on_ae ?_ ?_ ?_ ?_

Premises used: MeasureTheory.setIntegral_mono_on_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
refine_1 refine_1₁ refine_1₂ refine_1₃ : IntegrableOn f s μ
⊢ IntegrableOn f (toMeasurable μ s) μ

Tactic:
rwa [integrableOn_congr_set_ae hs.toMeasurable_ae_eq]

Premises used: MeasureTheory.integrableOn_congr_set_ae, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
refine_2 refine_2₁ refine_2₂ refine_2₃ : IntegrableOn g s μ
⊢ IntegrableOn g (toMeasurable μ s) μ

Tactic:
rwa [integrableOn_congr_set_ae hs.toMeasurable_ae_eq]

Premises used: MeasureTheory.integrableOn_congr_set_ae, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ MeasurableSet (toMeasurable μ s)

Tactic:
measurableSet_toMeasurable μ s

Premises used: MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ MeasurableSet (toMeasurable μ s)

Tactic:
exact measurableSet_toMeasurable μ s

Premises used: MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
h₁ : ∀ (x : X) (hx : x ∈ toMeasurable μ s ↔ x ∈ s) (h : x ∈ s → f x ≤ g x), x ∈ toMeasurable μ s → f x ≤ g x
⊢ ∀ᵐ (x : X) ∂μ, x ∈ toMeasurable μ s → f x ≤ g x

Tactic:
filter_upwards [hs.toMeasurable_ae_eq.mem_iff, h] with x hx h

Premises used: Filter.EventuallyEq.mem_iff, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h_1 : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
x : X
hx : x ∈ toMeasurable μ s ↔ x ∈ s
h h₁ h₂ h₃ h₄ : x ∈ s → f x ≤ g x
⊢ x ∈ toMeasurable μ s → f x ≤ g x

Tactic:
rwa [hx]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ x ∈ s, f x ≤ g x
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)

Tactic:
setIntegral_mono_on_ae₀ hf hg hs (Eventually.of_forall h)

Premises used: MeasureTheory.setIntegral_mono_on_ae₀, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst_5 : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
h : f ≤ g
⊢ LE.le.{u_3} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)

Tactic:
integral_mono hf hg h

Premises used: MeasureTheory.integral_mono