-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_setLaverage_le_pos (hμ : μ s ≠ 0) (hs : NullMeasurableSet s μ)
    (hint : ∫⁻ a in s, f a ∂μ ≠ ∞) : 0 < μ {x ∈ s | ⨍⁻ a in s, f a ∂μ ≤ f x}

Proof state:
case inr.intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ⊤
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 : 0 < (μ.restrict s) ({a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ⊤})
x : α
hfx : x ∈ {a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal}
hx : x ∉ {x | g x = ⊤}
⊢ x ∈ {a | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a}

Tactic:
dsimp at hfx

Result:
case inr.intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ⊤
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 : 0 < (μ.restrict s) ({a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ⊤})
x : α
hfx : ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal
hx : x ∉ {x | g x = ⊤}
⊢ x ∈ {a | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a}

Proof state:
case inr.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤
hμ₁ : μ s ≠ ⊤
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 ∂μ
⊢ 0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}

Tactic:
rw [hfg] at hint

Result:
case inr.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ⊤
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 ∂μ
⊢ 0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤
hμ₁ : μ s ≠ ⊤
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:
simp_rw [laverage_eq, hfg]

Result:
no goals

Proof state:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤
hμ₁ : μ s = ⊤
⊢ 0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}

Tactic:
simp [setLaverage_eq, hμ₁]

Result:
no goals

Proof state:
case inr.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ⊤
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 : 0 < μ {x | x ∈ s ∧ ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal}
⊢ 0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}

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

Result:
case inr.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ⊤
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 : 0 < μ {x | x ∈ s ∧ ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal}
⊢ 0 < (μ.restrict s) {a | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a}

Proof state:
case inr.intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ⊤
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 : 0 < (μ.restrict s) ({a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ⊤})
x : α
hfx : ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal
hx : x ∉ {x | g x = ⊤}
⊢ x ∈ {a | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a}

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

Result:
case inr.intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ⊤
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 : 0 < (μ.restrict s) ({a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ⊤})
x : α
hfx : ⨍⁻ (x : α) in s, g x ∂μ ≤ g x
hx : x ∉ {x | g x = ⊤}
⊢ x ∈ {a | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a}

case inr.intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ⊤
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 : 0 < (μ.restrict s) ({a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ⊤})
x : α
hfx : ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal
hx : x ∉ {x | g x = ⊤}
⊢ ∀ᵐ (x : α) ∂μ.restrict s, g x ≠ ⊤

Proof state:
case inr.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ⊤
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 ∂μ
⊢ 0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}

Tactic:
have :=
  measure_setAverage_le_pos hμ hμ₁ (integrable_toReal_of_lintegral_ne_top hg.aemeasurable hint)

Result:
case inr.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ⊤
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 : 0 < μ {x | x ∈ s ∧ ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal}
⊢ 0 < μ {x | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x}

Proof state:
case inr.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ⊤
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 : 0 < (μ.restrict s) ({a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ⊤})
⊢ 0 < (μ.restrict s) {a | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a}

Tactic:
refine this.trans_le (measure_mono ?_)

Result:
case inr.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hs : NullMeasurableSet s μ
hμ₁ : μ s ≠ ⊤
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 : 0 < (μ.restrict s) ({a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ⊤})
⊢ {a | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x | g x = ⊤} ⊆ {a | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a}