-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_le_setAverage_pos (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ∞) (hf : IntegrableOn f s μ) :
    0 < μ ({x ∈ s | f x ≤ ⨍ a in s, f a ∂μ})

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : μ {x | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
⊢ False

Tactic:
replace H : (μ.restrict s) {x | f x ≤ ⨍ a in s, f a ∂μ} = 0 := by
  rwa [restrict_apply₀, inter_comm]
  exact AEStronglyMeasurable.nullMeasurableSet_le hf.1 aestronglyMeasurable_const

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
⊢ False

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
⊢ False

Tactic:
refine (integral_sub_average (μ.restrict s) f).not_gt ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
⊢ 0 < ∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : μ {x | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
⊢ NullMeasurableSet {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} (μ.restrict s)

Tactic:
exact AEStronglyMeasurable.nullMeasurableSet_le hf.1 aestronglyMeasurable_const

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
x : α
hx : x ∈ {x | (fun x => 0 x ≤ (fun x => f x - ⨍ (a : α) in s, f a ∂μ) x) x}ᶜ
⊢ x ∈ {x | f x ≤ ⨍ (a : α) in s, f a ∂μ}

Tactic:
simp only [Pi.zero_apply, sub_nonneg, mem_compl_iff, mem_setOf_eq, not_le] at hx

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
x : α
hx : f x < ⨍ (a : α) in s, f a ∂μ
⊢ x ∈ {x | f x ≤ ⨍ (a : α) in s, f a ∂μ}

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
⊢ 0 ≤ᶠ[ae (μ.restrict s)] fun x => f x - ⨍ (a : α) in s, f a ∂μ

Tactic:
refine measure_mono_null (fun x hx ↦ ?_) H

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
x : α
hx : x ∈ {x | (fun x => 0 x ≤ (fun x => f x - ⨍ (a : α) in s, f a ∂μ) x) x}ᶜ
⊢ x ∈ {x | f x ≤ ⨍ (a : α) in s, f a ∂μ}

Proof state:
case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
⊢ 0 < μ ((support fun x => f x - ⨍ (a : α) in s, f a ∂μ) ∩ s)

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

Result:
case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
⊢ μ ((support fun x => f x - ⨍ (a : α) in s, f a ∂μ)ᶜ ∩ s) = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : μ {x | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
⊢ (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0

Tactic:
rwa [restrict_apply₀, inter_comm]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : μ {x | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
⊢ NullMeasurableSet {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} (μ.restrict s)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
⊢ 0 < ∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ

Tactic:
refine (setIntegral_pos_iff_support_of_nonneg_ae ?_ ?_).2 ?_

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
⊢ 0 ≤ᶠ[ae (μ.restrict s)] fun x => f x - ⨍ (a : α) in s, f a ∂μ

case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
⊢ IntegrableOn (fun x => f x - ⨍ (a : α) in s, f a ∂μ) s μ

case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
⊢ 0 < μ ((support fun x => f x - ⨍ (a : α) in s, f a ∂μ) ∩ s)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
⊢ False

Tactic:
haveI := Fact.mk hμ₁.lt_top

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
⊢ False

Proof state:
case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
⊢ (support 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

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
⊢ 0 < μ {x | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ}

Tactic:
refine pos_iff_ne_zero.2 fun H => ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : μ {x | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
⊢ False

Proof state:
case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
⊢ μ ((support fun x => f x - ⨍ (a : α) in s, f a ∂μ)ᶜ ∩ s) = 0

Tactic:
refine measure_mono_null ?_ (measure_inter_eq_zero_of_restrict H)

Result:
case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
⊢ (support fun x => f x - ⨍ (a : α) in s, f a ∂μ)ᶜ ∩ s ⊆ {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} ∩ s

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
x : α
hx : f x < ⨍ (a : α) in s, f a ∂μ
⊢ x ∈ {x | f x ≤ ⨍ (a : α) in s, f a ∂μ}

Tactic:
exact hx.le

Result:
no goals