awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | f a = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ∞

Tactic:
simp_rw [ae_iff, not_ne_iff]

Premises used: not_ne_iff, MeasureTheory.ae_iff
-- 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 = ∞}
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | f a = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_eq_top_of_lintegral_ne_top hf h

Premises used: MeasureTheory.measure_eq_top_of_lintegral_ne_top
-- 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 = ∞}
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | f a = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_eq_top_of_lintegral_ne_top hf h

Premises used: MeasureTheory.measure_eq_top_of_lintegral_ne_top
-- 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∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
inl :
  ∀ (hμ₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)
inr :
  ∀ (hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)

Tactic:
obtain hμ₁ | hμ₁ := eq_or_ne (μ s) ∞

Premises used: eq_or_ne, Top.top, DFunLike.coe
-- 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∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)

Tactic:
simp [setLAverage_eq, hμ₁]

Premises used: MeasureTheory.setLAverage_eq
-- 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∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
inr :
  ∀ (g : α → ℝ≥0∞) (hg : Measurable g) (hgf : g ≤ f) (hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ),
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)

Tactic:
obtain ⟨g, hg, hgf, hfg⟩ := exists_measurable_le_lintegral_eq (μ.restrict s) f

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.exists_measurable_le_lintegral_eq
-- 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∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
simp_rw :
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (a : α) in s, f a ∂μ) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (a : α) in s, g a ∂μ) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ

Tactic:
simp_rw [laverage_eq, hfg]

Premises used: MeasureTheory.laverage_eq
-- 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∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ

Tactic:
have hfg' : ⨍⁻ a in s, f a ∂μ = ⨍⁻ a in s, g a ∂μ := by simp_rw [laverage_eq, hfg]
-- 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∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
⊢ ∫⁻ (a : α) in s, g a ∂μ ≠ ∞

Tactic:
rw [hfg] at hint
-- 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∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
hint₁ : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
⊢ Measurable g

Tactic:
rw [hfg] at hint
-- 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∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
hint₁ : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg₁ : Measurable g
⊢ g ≤ f

Tactic:
rw [hfg] at hint
-- 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∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
hint₁ : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg₁ : Measurable g
hgf₁ : g ≤ f
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Tactic:
rw [hfg] at hint
-- 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∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
hint₁ : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg₁ : Measurable g
hgf₁ : g ≤ f
hfg₁ : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ

Tactic:
rw [hfg] at hint
-- 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∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal} : ℝ≥0∞)

Tactic:
have :=
    measure_setAverage_le_pos hμ hμ₁ (integrable_toReal_of_lintegral_ne_top hg.aemeasurable hint)
-- 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∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal} : ℝ≥0∞)
inr : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)

Tactic:
simp_rw [← setOf_inter_eq_sep, ← Measure.restrict_apply₀' hs, hfg']

Premises used: 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∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞}) :
      ℝ≥0∞)

Tactic:
rw [← setOf_inter_eq_sep, ← Measure.restrict_apply₀' hs, ←
    measure_diff_null (measure_eq_top_of_lintegral_ne_top hg.aemeasurable hint)] at this

Premises used: Measurable.aemeasurable, MeasureTheory.measure_diff_null, MeasureTheory.Measure.restrict_apply₀', MeasureTheory.measure_eq_top_of_lintegral_ne_top, 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∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞}) :
      ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ 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∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞}) :
      ℝ≥0∞)
inr :
  Subset.{u_1} (α := Set α) ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞})
    {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a}
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ 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∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞}) :
      ℝ≥0∞)
x : α
hfx : ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal
hx : x ∉ {x : α | g x = ∞}
inr :
  ∀ (hfx : ⨍⁻ (x : α) in s, g x ∂μ ≤ g x) (hx : x ∉ {x : α | g x = ∞}),
    Membership.mem (γ := Set α) {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a} x
inr₁ : ∀ᵐ (x : α) ∂μ.restrict s, g x ≠ ∞
⊢ Membership.mem (γ := Set α) {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a} x

Tactic:
rw [← toReal_laverage hg.aemeasurable, toReal_le_toReal (setLAverage_lt_top hint).ne hx] at hfx

Premises used: Measurable.aemeasurable, MeasureTheory.toReal_laverage, ENNReal.toReal_le_toReal, MeasureTheory.setLAverage_lt_top, LT.lt.ne
-- 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∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞}) :
      ℝ≥0∞)
x : α
hfx : ⨍⁻ (x : α) in s, g x ∂μ ≤ g x
hx : x ∉ {x : α | g x = ∞}
⊢ Membership.mem (γ := Set α) {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a} x

Tactic:
hfx.trans (hgf _)

Premises used: Set.Mem, setOf, LE.le.trans
-- 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∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞}) :
      ℝ≥0∞)
x : α
hfx : ⨍⁻ (x : α) in s, g x ∂μ ≤ g x
hx : x ∉ {x : α | g x = ∞}
⊢ Membership.mem (γ := Set α) {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a} x

Tactic:
exact hfx.trans (hgf _)

Premises used: LE.le.trans
-- 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∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞}) :
      ℝ≥0∞)
x : α
hfx : ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal
hx : x ∉ {x : α | g x = ∞}
inr : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | g a = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ.restrict s, g x ≠ ∞

Tactic:
simp_rw [ae_iff, not_ne_iff]

Premises used: not_ne_iff, MeasureTheory.ae_iff
-- 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∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞}) :
      ℝ≥0∞)
x : α
hfx : ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal
hx : x ∉ {x : α | g x = ∞}
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | g a = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_eq_top_of_lintegral_ne_top hg.aemeasurable hint

Premises used: Measurable.aemeasurable, MeasureTheory.measure_eq_top_of_lintegral_ne_top
-- 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∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞}) :
      ℝ≥0∞)
x : α
hfx : ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal
hx : x ∉ {x : α | g x = ∞}
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | g a = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_eq_top_of_lintegral_ne_top hg.aemeasurable hint

Premises used: Measurable.aemeasurable, MeasureTheory.measure_eq_top_of_lintegral_ne_top
-- 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)
⊢ ∃ x ∈ s, f x ≤ ⨍⁻ (a : α) in s, f a ∂μ

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

Premises used: MeasureTheory.measure_le_setLAverage_pos, _private.0.MeasureTheory.exists_le_setLAverage.match_1, MeasureTheory.nonempty_of_measure_ne_zero, MeasureTheory.laverage, Membership.mem, Exists, MeasureTheory.Measure.restrict, LE.le, LT.lt.ne', And, And.intro, Exists.intro
-- 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∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
⊢ ∃ x ∈ s, ⨍⁻ (a : α) in s, f a ∂μ ≤ f x

Tactic:
let ⟨x, hx, h⟩ := nonempty_of_measure_ne_zero (measure_setLAverage_le_pos hμ hs hint).ne'
  ⟨x, hx, h⟩

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

Tactic:
simpa [hint] using
    @measure_setLAverage_le_pos _ _ _ _ f (measure_univ_ne_zero.2 hμ) nullMeasurableSet_univ

Premises used: Iff.mpr, MeasureTheory.Measure.measure_univ_ne_zero, MeasureTheory.nullMeasurableSet_univ, MeasureTheory.measure_setLAverage_le_pos
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ∞
⊢ ∃ (x : α), ⨍⁻ (a : α), f a ∂μ ≤ f x

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

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

Tactic:
have := measure_laverage_le_pos hμ hint
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ∞
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ⨍⁻ (a : α), f a ∂μ ≤ f x} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | ⨍⁻ (a : α), f a ∂μ ≤ f x} \ 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 : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ∞
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | ⨍⁻ (a : α), f a ∂μ ≤ f x} \ N) : ℝ≥0∞)
obtain :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | ⨍⁻ (a : α), f a ∂μ ≤ f x} x) (hxN : x ∉ N),
    ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x
⊢ ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x

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 : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ∞
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | ⨍⁻ (a : α), f a ∂μ ≤ f x} \ N) : ℝ≥0∞)
x : α
hx : Membership.mem (γ := Set α) {x : α | ⨍⁻ (a : α), f a ∂μ ≤ f x} x
hxN : x ∉ N
⊢ ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x

Tactic:
⟨x, hxN, hx⟩

Premises used: And.intro, Exists.intro