awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
x : α
hx : f x < ⨍ (a : α) in s, f a ∂μ
⊢ Membership.mem (γ := Set α) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} x

Tactic:
hx.le

Premises used: Set.Mem, setOf, LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
x : α
hx : f x < ⨍ (a : α) in s, f a ∂μ
⊢ Membership.mem (γ := Set α) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} x

Tactic:
exact hx.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ) s μ

Tactic:
hf.sub (integrableOn_const hμ₁)

Premises used: MeasureTheory.IntegrableOn.sub, MeasureTheory.integrableOn_const
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ) s μ

Tactic:
exact hf.sub (integrableOn_const hμ₁)

Premises used: MeasureTheory.IntegrableOn.sub, MeasureTheory.integrableOn_const
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
refine_3 :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((support (M := ℝ) fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ)ᶜ ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((support (M := ℝ) fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ) ∩ s) : ℝ≥0∞)

Tactic:
rwa [pos_iff_ne_zero, inter_comm, ← diff_compl, ← diff_inter_self_eq_diff, measure_diff_null]

Premises used: Set.inter_comm, Set.diff_inter_self_eq_diff, MeasureTheory.measure_diff_null, pos_iff_ne_zero, Set.diff_compl
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((support (M := ℝ) fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ)ᶜ ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
measure_mono_null ?_ (measure_inter_eq_zero_of_restrict H)

Premises used: MeasureTheory.Measure.measure_inter_eq_zero_of_restrict, MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
refine_3 :
  (support (M := ℝ) fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ)ᶜ ∩ s ⊆ {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} ∩ s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((support (M := ℝ) fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ)ᶜ ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
refine measure_mono_null ?_ (measure_inter_eq_zero_of_restrict H)

Premises used: MeasureTheory.Measure.measure_inter_eq_zero_of_restrict, MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ (support (M := ℝ) fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ)ᶜ ∩ s ⊆ {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} ∩ s

Tactic:
inter_subset_inter_left _ fun a ha => (sub_eq_zero.1 <| of_not_not ha).le

Premises used: sub_eq_zero, Eq.le, Set.inter_subset_inter_left, Iff.mp, of_not_not
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ (support (M := ℝ) fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ)ᶜ ∩ s ⊆ {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} ∩ s

Tactic:
exact inter_subset_inter_left _ fun a ha => (sub_eq_zero.1 <| of_not_not ha).le

Premises used: sub_eq_zero, Eq.le, Set.inter_subset_inter_left, Iff.mp, of_not_not
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)

Tactic:
simpa [integral_neg, neg_div] using measure_le_setAverage_pos hμ hμ₁ hf.neg

Premises used: neg_div, MeasureTheory.integral_neg, MeasureTheory.measure_le_setAverage_pos, MeasureTheory.IntegrableOn.neg
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
⊢ ∃ x ∈ s, f x ≤ ⨍ (a : α) in s, f a ∂μ

Tactic:
let ⟨x, hx, h⟩ := nonempty_of_measure_ne_zero (measure_le_setAverage_pos hμ hμ₁ hf).ne'
  ⟨x, hx, h⟩

Premises used: MeasureTheory.nonempty_of_measure_ne_zero, Membership.mem, Exists, MeasureTheory.Measure.restrict, MeasureTheory.measure_le_setAverage_pos, LE.le, MeasureTheory.average, LT.lt.ne', And, And.intro, Exists.intro, _private.0.MeasureTheory.exists_le_setAverage.match_1
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
⊢ ∃ x ∈ s, ⨍ (a : α) in s, f a ∂μ ≤ f x

Tactic:
let ⟨x, hx, h⟩ := nonempty_of_measure_ne_zero (measure_setAverage_le_pos hμ hμ₁ hf).ne'
  ⟨x, hx, h⟩

Premises used: MeasureTheory.nonempty_of_measure_ne_zero, Membership.mem, Exists, MeasureTheory.Measure.restrict, LE.le, MeasureTheory.average, _private.0.MeasureTheory.exists_setAverage_le.match_1, LT.lt.ne', And, And.intro, Exists.intro, MeasureTheory.measure_setAverage_le_pos
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α), f a ∂μ} : ℝ≥0∞)

Tactic:
simpa using measure_le_setAverage_pos (Measure.measure_univ_ne_zero.2 hμ) (measure_ne_top _ _)
    hf.integrableOn

Premises used: Iff.mpr, MeasureTheory.Measure.measure_univ_ne_zero, MeasureTheory.measure_ne_top, MeasureTheory.measure_le_setAverage_pos, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ⨍ (a : α), f a ∂μ ≤ f x} : ℝ≥0∞)

Tactic:
simpa using measure_setAverage_le_pos (Measure.measure_univ_ne_zero.2 hμ) (measure_ne_top _ _)
    hf.integrableOn

Premises used: Iff.mpr, MeasureTheory.Measure.measure_univ_ne_zero, MeasureTheory.measure_ne_top, MeasureTheory.Integrable.integrableOn, MeasureTheory.measure_setAverage_le_pos
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
⊢ ∃ (x : α), f x ≤ ⨍ (a : α), f a ∂μ

Tactic:
let ⟨x, hx⟩ := nonempty_of_measure_ne_zero (measure_le_average_pos hμ hf).ne'
  ⟨x, hx⟩

Premises used: MeasureTheory.nonempty_of_measure_ne_zero, Exists, LE.le, MeasureTheory.average, LT.lt.ne', _private.0.MeasureTheory.exists_le_average.match_1, Exists.intro, MeasureTheory.measure_le_average_pos
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
⊢ ∃ (x : α), ⨍ (a : α), f a ∂μ ≤ f x

Tactic:
let ⟨x, hx⟩ := nonempty_of_measure_ne_zero (measure_average_le_pos hμ hf).ne'
  ⟨x, hx⟩

Premises used: MeasureTheory.nonempty_of_measure_ne_zero, Exists, LE.le, MeasureTheory.average, LT.lt.ne', Exists.intro, MeasureTheory.measure_average_le_pos, _private.0.MeasureTheory.exists_average_le.match_1
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α), f a ∂μ} : ℝ≥0∞)

Tactic:
have := measure_le_average_pos hμ hf
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α), f a ∂μ} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≤ ⨍ (a : α), f a ∂μ} \ N) : ℝ≥0∞)

Tactic:
rw [← measure_diff_null hN] at this

Premises used: MeasureTheory.measure_diff_null
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≤ ⨍ (a : α), f a ∂μ} \ N) : ℝ≥0∞)
obtain :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | f x ≤ ⨍ (a : α), f a ∂μ} x) (hxN : x ∉ N),
    ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ
⊢ ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ

Tactic:
obtain ⟨x, hx, hxN⟩ := nonempty_of_measure_ne_zero this.ne'

Premises used: MeasureTheory.nonempty_of_measure_ne_zero, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≤ ⨍ (a : α), f a ∂μ} \ N) : ℝ≥0∞)
x : α
hx : Membership.mem (γ := Set α) {x : α | f x ≤ ⨍ (a : α), f a ∂μ} x
hxN : x ∉ N
⊢ ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ

Tactic:
⟨x, hxN, hx⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≤ ⨍ (a : α), f a ∂μ} \ N) : ℝ≥0∞)
x : α
hx : Membership.mem (γ := Set α) {x : α | f x ≤ ⨍ (a : α), f a ∂μ} x
hxN : x ∉ N
⊢ ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ

Tactic:
exact ⟨x, hxN, hx⟩
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ x ∉ N, ⨍ (a : α), f a ∂μ ≤ f x

Tactic:
simpa [integral_neg, neg_div] using exists_notMem_null_le_average hμ hf.neg hN

Premises used: neg_div, MeasureTheory.Integrable.neg, MeasureTheory.exists_notMem_null_le_average, MeasureTheory.integral_neg
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ∫ (a : α), f a ∂μ} : ℝ≥0∞)

Tactic:
simpa only [average_eq_integral] using
    measure_le_average_pos (IsProbabilityMeasure.ne_zero μ) hf

Premises used: MeasureTheory.average_eq_integral, MeasureTheory.IsProbabilityMeasure.ne_zero, MeasureTheory.measure_le_average_pos
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ∫ (a : α), f a ∂μ ≤ f x} : ℝ≥0∞)

Tactic:
simpa only [average_eq_integral] using
    measure_average_le_pos (IsProbabilityMeasure.ne_zero μ) hf

Premises used: MeasureTheory.average_eq_integral, MeasureTheory.IsProbabilityMeasure.ne_zero, MeasureTheory.measure_average_le_pos
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ ∃ (x : α), f x ≤ ∫ (a : α), f a ∂μ

Tactic:
simpa only [average_eq_integral] using exists_le_average (IsProbabilityMeasure.ne_zero μ) hf

Premises used: MeasureTheory.average_eq_integral, MeasureTheory.IsProbabilityMeasure.ne_zero, MeasureTheory.exists_le_average
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ ∃ (x : α), ∫ (a : α), f a ∂μ ≤ f x

Tactic:
simpa only [average_eq_integral] using exists_average_le (IsProbabilityMeasure.ne_zero μ) hf

Premises used: MeasureTheory.exists_average_le, MeasureTheory.average_eq_integral, MeasureTheory.IsProbabilityMeasure.ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst : IsProbabilityMeasure μ
hf : Integrable f μ
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ x ∉ N, f x ≤ ∫ (a : α), f a ∂μ

Tactic:
simpa only [average_eq_integral] using
    exists_notMem_null_le_average (IsProbabilityMeasure.ne_zero μ) hf hN

Premises used: MeasureTheory.exists_notMem_null_le_average, MeasureTheory.average_eq_integral, MeasureTheory.IsProbabilityMeasure.ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst : IsProbabilityMeasure μ
hf : Integrable f μ
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ x ∉ N, ∫ (a : α), f a ∂μ ≤ f x

Tactic:
simpa only [average_eq_integral] using
    exists_notMem_null_average_le (IsProbabilityMeasure.ne_zero μ) hf hN

Premises used: MeasureTheory.average_eq_integral, MeasureTheory.IsProbabilityMeasure.ne_zero, MeasureTheory.exists_notMem_null_average_le
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : AEMeasurable f (μ.restrict s)
inl :
  ∀ (h : ∫⁻ (a : α) in s, f a ∂μ = ∞),
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)
inr :
  ∀ (h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞),
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)

Tactic:
obtain h | h := eq_or_ne (∫⁻ a in s, f a ∂μ) ∞

Premises used: MeasureTheory.Measure.restrict, eq_or_ne, Top.top, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ = ∞
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)

Tactic:
simpa [mul_top, hμ₁, laverage, h, top_div_of_ne_top hμ₁, pos_iff_ne_zero] using hμ

Premises used: ENNReal.top_div_of_ne_top, MeasureTheory.laverage, ENNReal.mul_top, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} : ℝ≥0∞)

Tactic:
have := measure_le_setAverage_pos hμ hμ₁ (integrable_toReal_of_lintegral_ne_top hf h)
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} : ℝ≥0∞)
inr : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)

Tactic:
rw [← setOf_inter_eq_sep, ← Measure.restrict_apply₀
    (hf.aestronglyMeasurable.nullMeasurableSet_le aestronglyMeasurable_const)]

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.aestronglyMeasurable_const, MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_le, MeasureTheory.Measure.restrict_apply₀, Set.setOf_inter_eq_sep
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x : α | f x = ∞}) :
      ℝ≥0∞)

Tactic:
rw [← setOf_inter_eq_sep, ← Measure.restrict_apply₀
    (hf.ennreal_toReal.aestronglyMeasurable.nullMeasurableSet_le aestronglyMeasurable_const),
    ← measure_diff_null (measure_eq_top_of_lintegral_ne_top hf h)] at this

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.aestronglyMeasurable_const, MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_le, MeasureTheory.measure_diff_null, MeasureTheory.Measure.restrict_apply₀, MeasureTheory.measure_eq_top_of_lintegral_ne_top, AEMeasurable.ennreal_toReal, Set.setOf_inter_eq_sep
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x : α | f x = ∞}) :
      ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)

Tactic:
this.trans_le (measure_mono ?_)

Premises used: LT.lt.trans_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x : α | f x = ∞}) :
      ℝ≥0∞)
inr :
  Subset.{u_1} (α := Set α) ({a : α | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x : α | f x = ∞})
    {a : α | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ}
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)

Tactic:
refine this.trans_le (measure_mono ?_)

Premises used: LT.lt.trans_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x : α | f x = ∞}) :
      ℝ≥0∞)
x : α
hfx : (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ
hx : x ∉ {x : α | f x = ∞}
inr : ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ∞
⊢ Membership.mem (γ := Set α) {a : α | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ} x

Tactic:
rwa [← toReal_laverage hf, toReal_le_toReal hx (setLAverage_lt_top h).ne] at hfx

Premises used: MeasureTheory.toReal_laverage, ENNReal.toReal_le_toReal, MeasureTheory.setLAverage_lt_top, LT.lt.ne