awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
neg : norm.{u_3} (E := E) 0 ≤ C * μ.real s
⊢ norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s

Tactic:
rw [integral_non_aestronglyMeasurable hfm]

Premises used: MeasureTheory.integral_non_aestronglyMeasurable
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
apply : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ᵐ (x : X) ∂μ, x ∈ s

Tactic:
apply frequently_ae_mem_iff.mpr

Premises used: Iff.mpr, MeasureTheory.frequently_ae_mem_iff
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
contrapose :
  ∀ (hfm : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), AEStronglyMeasurable f (μ.restrict s)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
contrapose hfm
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
simp [Measure.restrict_eq_zero.mpr hfm]

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_eq_zero
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
⊢ ∃ᵐ (x : X) ∂μ, x ∈ s

Tactic:
have : ∃ᵐ (x : X) ∂μ, x ∈ s := by
      apply frequently_ae_mem_iff.mpr
      contrapose hfm
      simp [Measure.restrict_eq_zero.mpr hfm]
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
this : ∃ᵐ (x : X) ∂μ, x ∈ s
neg : ∀ (x : X) (hx : x ∈ s) (h'x : x ∈ s → ‖f x‖ ≤ C), norm.{u_3} (E := E) 0 ≤ C * μ.real s
⊢ norm.{u_3} (E := E) 0 ≤ C * μ.real s

Tactic:
rcases (this.and_eventually hC).exists with ⟨x, hx, h'x⟩

Premises used: Filter.Frequently.and_eventually, Filter.Frequently.exists
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
this : ∃ᵐ (x : X) ∂μ, x ∈ s
x : X
hx : x ∈ s
h'x : x ∈ s → ‖f x‖ ≤ C
⊢ 0 ≤ C

Tactic:
have : 0 ≤ C := (norm_nonneg _).trans (h'x 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
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
this_1 : ∃ᵐ (x : X) ∂μ, x ∈ s
x : X
hx : x ∈ s
h'x : x ∈ s → ‖f x‖ ≤ C
this : 0 ≤ C
neg : 0 ≤ C * μ.real s
⊢ norm.{u_3} (E := E) 0 ≤ C * μ.real s

Tactic:
simp only [norm_zero, ge_iff_le]

Premises used: ge_iff_le, norm_zero
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
this_1 : ∃ᵐ (x : X) ∂μ, x ∈ s
x : X
hx : x ∈ s
h'x : x ∈ s → ‖f x‖ ≤ C
this : 0 ≤ C
⊢ 0 ≤ C * μ.real s

Tactic:
positivity
-- 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
s : Set X
μ : Measure X
C : ℝ
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hC : ∀ x ∈ s, ‖f x‖ ≤ C
⊢ norm.{u_3} (E := E) (∫ (x : X) in s, f x ∂μ) ≤ C * μ.real s

Tactic:
norm_setIntegral_le_of_norm_le_const_ae' hs (Eventually.of_forall hC)

Premises used: MeasureTheory.norm_setIntegral_le_of_norm_le_const_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
f : X → E
μ : Measure X
inst_2 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
rw : ∫ (x : X), f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in sᶜ, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
rw₁ : ∫ (x : X), f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, f x ∂μ)
rw₂ rw₃ : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X), f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ

Tactic:
rw [sub_eq_iff_eq_add, add_comm, integral_add_compl hs hf1]

Premises used: MeasureTheory.integral_add_compl, add_comm, sub_eq_iff_eq_add
-- 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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
⊢ HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ

Tactic:
have h0 : ∫ (x : X), f x ∂μ - ∫ x in s, f x ∂μ = ∫ x in sᶜ, f x ∂μ := by
    rw [sub_eq_iff_eq_add, add_comm, integral_add_compl hs hf1]
-- 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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
⊢ LE.le (α := ℝ) (∫ (x : X) in sᶜ, ‖f x‖ ∂μ) (∫ (x : X) in sᶜ, C ∂μ)

Tactic:
have h1 : ∫ x in sᶜ, ‖f x‖ ∂μ ≤ ∫ _ in sᶜ, C ∂μ :=
    integral_mono_ae hf1.norm.restrict (integrable_const C) (ae_restrict_of_ae hf)
-- 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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
h1 : LE.le (α := ℝ) (∫ (x : X) in sᶜ, ‖f x‖ ∂μ) (∫ (x : X) in sᶜ, C ∂μ)
rw : μ.real sᶜ • C = μ.real sᶜ * C
rw₁ rw₂ : μ.real sᶜ * C = μ.real sᶜ * C
⊢ ∫ (x : X) in sᶜ, C ∂μ = μ.real sᶜ * C

Tactic:
rw [setIntegral_const C, smul_eq_mul]

Premises used: smul_eq_mul, MeasureTheory.setIntegral_const
-- 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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
h1 : LE.le (α := ℝ) (∫ (x : X) in sᶜ, ‖f x‖ ∂μ) (∫ (x : X) in sᶜ, C ∂μ)
⊢ ∫ (x : X) in sᶜ, C ∂μ = μ.real sᶜ * C

Tactic:
have h2 : ∫ _ in sᶜ, C ∂μ = μ.real sᶜ * C := by
    rw [setIntegral_const C, smul_eq_mul]
-- 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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
h1 : LE.le (α := ℝ) (∫ (x : X) in sᶜ, ‖f x‖ ∂μ) (∫ (x : X) in sᶜ, C ∂μ)
h2 : ∫ (x : X) in sᶜ, C ∂μ = μ.real sᶜ * C
rw : norm.{u_3} (E := E) (∫ (x : X) in sᶜ, f x ∂μ) ≤ ∫ (x : X) in sᶜ, C ∂μ
⊢ ‖HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)‖ ≤ μ.real sᶜ * C

Tactic:
rw [h0, ← h2]
-- 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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
h1 : LE.le (α := ℝ) (∫ (x : X) in sᶜ, ‖f x‖ ∂μ) (∫ (x : X) in sᶜ, C ∂μ)
h2 : ∫ (x : X) in sᶜ, C ∂μ = μ.real sᶜ * C
⊢ norm.{u_3} (E := E) (∫ (x : X) in sᶜ, f x ∂μ) ≤ ∫ (x : X) in sᶜ, C ∂μ

Tactic:
le_trans (norm_integral_le_integral_norm f) h1

Premises used: MeasureTheory.norm_integral_le_integral_norm, le_trans
-- 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 : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ) = ∫ (x : X) in sᶜ, f x ∂μ
h1 : LE.le (α := ℝ) (∫ (x : X) in sᶜ, ‖f x‖ ∂μ) (∫ (x : X) in sᶜ, C ∂μ)
h2 : ∫ (x : X) in sᶜ, C ∂μ = μ.real sᶜ * C
⊢ norm.{u_3} (E := E) (∫ (x : X) in sᶜ, f x ∂μ) ≤ ∫ (x : X) in sᶜ, C ∂μ

Tactic:
exact le_trans (norm_integral_le_integral_norm f) h1

Premises used: MeasureTheory.norm_integral_le_integral_norm, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᶠ[ae (μ.restrict s)] f
hfi : IntegrableOn f s μ
⊢ Eq (α := ℝ) (∫ (x : X) in s, f x ∂μ) 0 ↔ f =ᶠ[ae (μ.restrict s)] 0

Tactic:
integral_eq_zero_iff_of_nonneg_ae hf hfi

Premises used: MeasureTheory.integral_eq_zero_iff_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᶠ[ae (μ.restrict s)] f
hfi : IntegrableOn f s μ
rw : NullMeasurableSet (support f) (μ.restrict s)
⊢ LT.lt (α := ℝ) 0 (∫ (x : X) in s, f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (support f ∩ s) : ℝ≥0∞)

Tactic:
rw [integral_pos_iff_support_of_nonneg_ae hf hfi, Measure.restrict_apply₀]

Premises used: MeasureTheory.integral_pos_iff_support_of_nonneg_ae, MeasureTheory.Measure.restrict_apply₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᶠ[ae (μ.restrict s)] f
hfi : IntegrableOn f s μ
⊢ NullMeasurableSet (f ⁻¹' {0}ᶜ) (μ.restrict s)

Tactic:
hfi.aestronglyMeasurable.aemeasurable.nullMeasurable (measurableSet_singleton 0).compl

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.nullMeasurable, MeasurableSingletonClass.measurableSet_singleton, MeasurableSet.compl, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᶠ[ae (μ.restrict s)] f
hfi : IntegrableOn f s μ
⊢ NullMeasurableSet (f ⁻¹' {0}ᶜ) (μ.restrict s)

Tactic:
exact hfi.aestronglyMeasurable.aemeasurable.nullMeasurable (measurableSet_singleton 0).compl

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.nullMeasurable, MeasurableSingletonClass.measurableSet_singleton, MeasurableSet.compl, OfNat.ofNat
-- 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∞)
⊢ IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ

Tactic:
⟨aestronglyMeasurable_const, lt_of_le_of_lt ?_ hfint.2⟩

Premises used: lt_of_le_of_lt, MeasureTheory.aestronglyMeasurable_const, MeasureTheory.Integrable, MeasureTheory.IntegrableOn, And.right, And.intro
-- 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∞)
refine :
  ∫⁻ (a : X) in {x : X | R < f x}, enorm (E := ℝ) ((fun (x : X) ↦ R) a) ∂μ ≤ ∫⁻ (a : X) in {x : X | R < f x}, ‖f a‖ₑ ∂μ
⊢ IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ

Tactic:
refine ⟨aestronglyMeasurable_const, lt_of_le_of_lt ?_ hfint.2⟩
-- 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∞)
⊢ ∫⁻ (a : X) in {x : X | R < f x}, enorm (E := ℝ) ((fun (x : X) ↦ R) a) ∂μ ≤ ∫⁻ (a : X) in {x : X | R < f x}, ‖f a‖ₑ ∂μ

Tactic:
setLIntegral_mono_ae hfint.1.enorm <| ae_of_all _ fun x hx => ?_

Premises used: MeasureTheory.setLIntegral_mono_ae, And.left, MeasureTheory.ae_of_all, MeasureTheory.AEStronglyMeasurable.enorm
-- 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∞)
refine : ∀ (x : X) (hx : Membership.mem (γ := Set X) {x : X | R < f x} x), enorm (E := ℝ) ((fun (x : X) ↦ R) x) ≤ ‖f x‖ₑ
⊢ ∫⁻ (a : X) in {x : X | R < f x}, enorm (E := ℝ) ((fun (x : X) ↦ R) a) ∂μ ≤ ∫⁻ (a : X) in {x : X | R < f x}, ‖f a‖ₑ ∂μ

Tactic:
refine setLIntegral_mono_ae hfint.1.enorm <| ae_of_all _ fun x hx => ?_

Premises used: MeasureTheory.setLIntegral_mono_ae, And.left, MeasureTheory.ae_of_all, MeasureTheory.AEStronglyMeasurable.enorm
-- 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∞)
x : X
hx : Membership.mem (γ := Set X) {x : X | R < f x} x
simp : NNReal.mk R hR ≤ NNReal.mk (f x) ⋯
⊢ enorm (E := ℝ) ((fun (x : X) ↦ R) x) ≤ ‖f x‖ₑ

Tactic:
simp only [ENNReal.coe_le_coe, Real.nnnorm_of_nonneg hR, enorm_eq_nnnorm,
      Real.nnnorm_of_nonneg (hR.trans <| le_of_lt hx)]

Premises used: le_of_lt, ENNReal.coe_le_coe, enorm_eq_nnnorm, Real.nnnorm_of_nonneg, LE.le.trans
-- 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∞)
x : X
hx : Membership.mem (γ := Set X) {x : X | R < f x} x
⊢ NNReal.mk R hR ≤ NNReal.mk (f x) ⋯

Tactic:
le_of_lt hx

Premises used: le_of_lt
-- 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∞)
x : X
hx : Membership.mem (γ := Set X) {x : X | R < f x} x
⊢ NNReal.mk R hR ≤ NNReal.mk (f x) ⋯

Tactic:
exact le_of_lt hx

Premises used: le_of_lt
-- 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∞)
⊢ IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ

Tactic:
have : IntegrableOn (fun _ => R) {x | ↑R < f x} μ := by
    refine ⟨aestronglyMeasurable_const, lt_of_le_of_lt ?_ hfint.2⟩
    refine setLIntegral_mono_ae hfint.1.enorm <| ae_of_all _ fun x hx => ?_
    simp only [ENNReal.coe_le_coe, Real.nnnorm_of_nonneg hR, enorm_eq_nnnorm,
      Real.nnnorm_of_nonneg (hR.trans <| le_of_lt hx)]
    exact le_of_lt hx
-- 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} μ
rw :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) ((support (M := ℝ) fun (a : X) ↦ f a - R) ∩ {x : X | R < f x}) : ℝ≥0∞)
hf : (ae (μ.restrict {x : X | R < f x})).EventuallyLE (β := ℝ) 0 fun (a : X) ↦ f a - R
hfi : IntegrableOn (ε := ℝ) (fun (a : X) ↦ f a - R) {x : X | R < f x} μ
⊢ μ.real {x : X | R < f x} * R < ∫ (x : X) in {x : X | R < f x}, f x ∂μ

Tactic:
rw [← sub_pos, ← smul_eq_mul, ← setIntegral_const, ← integral_sub hfint this,
    setIntegral_pos_iff_support_of_nonneg_ae]

Premises used: sub_pos, MeasureTheory.integral_sub, MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae, smul_eq_mul, MeasureTheory.setIntegral_const
-- 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} μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞)

Tactic:
rw [← pos_iff_ne_zero] at hμ

Premises used: pos_iff_ne_zero
-- 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} μ
hμ₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞)
⊢ IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ

Tactic:
rw [← pos_iff_ne_zero] at hμ

Premises used: pos_iff_ne_zero
-- 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μ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞)
this : IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ
rwa : Subset.{u_1} (α := Set X) {x : X | R < f x} (support (M := ℝ) fun (a : X) ↦ f a - R)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) ((support (M := ℝ) fun (a : X) ↦ f a - R) ∩ {x : X | R < f x}) : ℝ≥0∞)

Tactic:
rwa [Set.inter_eq_self_of_subset_right]

Premises used: Set.inter_eq_self_of_subset_right
-- 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μ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞)
this : IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ
⊢ Subset.{u_1} (α := Set X) {x : X | R < f x} (support (M := ℝ) fun (a : X) ↦ f a - R)

Tactic:
fun x hx => Ne.symm (ne_of_lt <| sub_pos.2 hx)

Premises used: Iff.mpr, sub_pos, Set.Mem, setOf, Ne.symm, Set.Subset, Function.support, ne_of_lt, Not
-- 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μ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {x : X | R < f x} : ℝ≥0∞)
this : IntegrableOn (ε := ℝ) (fun (x : X) ↦ R) {x : X | R < f x} μ
⊢ Subset.{u_1} (α := Set X) {x : X | R < f x} (support (M := ℝ) fun (a : X) ↦ f a - R)

Tactic:
exact fun x hx => Ne.symm (ne_of_lt <| sub_pos.2 hx)

Premises used: Iff.mpr, sub_pos, Ne.symm, ne_of_lt
-- 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} μ
hf : ∀ᵐ (x : X) ∂μ, Membership.mem (γ := Set X) {x : X | R < f x} x → 0 ≤ f x - R
hf₁ : NullMeasurableSet {x : X | 0 ≤ f x - R} (μ.restrict {x : X | R < f x})
⊢ (ae (μ.restrict {x : X | R < f x})).EventuallyLE (β := ℝ) 0 fun (a : X) ↦ f a - R

Tactic:
rw [Pi.zero_def, EventuallyLE, ae_restrict_iff₀]

Premises used: Pi.zero_def, MeasureTheory.ae_restrict_iff₀, Filter.EventuallyLE
-- 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} μ
⊢ ∀ᵐ (x : X) ∂μ, Membership.mem (γ := Set X) {x : X | R < f x} x → 0 ≤ f x - R

Tactic:
Eventually.of_forall fun x hx => sub_nonneg.2 <| le_of_lt hx

Premises used: Iff.mpr, le_of_lt, Filter.Eventually.of_forall, sub_nonneg
-- 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} μ
⊢ ∀ᵐ (x : X) ∂μ, Membership.mem (γ := Set X) {x : X | R < f x} x → 0 ≤ f x - R

Tactic:
exact Eventually.of_forall fun x hx => sub_nonneg.2 <| le_of_lt hx

Premises used: Iff.mpr, le_of_lt, Filter.Eventually.of_forall, sub_nonneg
-- 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} μ
⊢ NullMeasurableSet {x : X | 0 ≤ f x - R} (μ.restrict {x : X | R < f x})

Tactic:
nullMeasurableSet_le aemeasurable_zero (hfint.1.aemeasurable.sub aemeasurable_const)

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, aemeasurable_zero, setOf, nullMeasurableSet_le, And.left, AEMeasurable.sub, aemeasurable_const
-- 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} μ
⊢ NullMeasurableSet {x : X | 0 ≤ f x - R} (μ.restrict {x : X | R < f x})

Tactic:
exact nullMeasurableSet_le aemeasurable_zero (hfint.1.aemeasurable.sub aemeasurable_const)

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, aemeasurable_zero, nullMeasurableSet_le, And.left, AEMeasurable.sub, aemeasurable_const