-- Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
theorem ae_nonneg_of_forall_setIntegral_nonneg (hf : Integrable f μ)
    (hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → 0 ≤ ∫ x in s, f x ∂μ) : 0 ≤ᵐ[μ] f

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ b

Tactic:
exact Eventually.of_forall fun x hxs => hxs

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
⊢ 0 ≤ᶠ[ae μ] f

Tactic:
simp_rw [EventuallyLE, Pi.zero_apply]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
⊢ ∀ᵐ (x : α) ∂μ, 0 ≤ f x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
⊢ ∀ b < 0, μ {x | f x ≤ b} = 0

Tactic:
intro b hb_neg

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
⊢ μ {x | f x ≤ b} = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
H : μ {x | f x ≤ b} ≠ 0
⊢ 0 ≤ ∫ (x : α) in toMeasurable μ s, f x ∂μ

Tactic:
exact hf_zero _ (measurableSet_toMeasurable ..) (by rwa [measure_toMeasurable])

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
H : μ {x | f x ≤ b} ≠ 0
⊢ μ (toMeasurable μ s) < ⊤

Tactic:
rwa [measure_toMeasurable]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
⊢ μ {x | f x ≤ b} = 0

Tactic:
have h_int_gt : (∫ x in s, f x ∂μ) ≤ b * (μ s).toReal := by
  have h_const_le : (∫ x in s, f x ∂μ) ≤ ∫ _ in s, b ∂μ := by
    refine setIntegral_mono_ae_restrict hf.integrableOn (integrableOn_const.mpr (Or.inr mus)) ?_
    rw [EventuallyLE, ae_restrict_iff₀ (hs.mono μ.restrict_le_self)]
    exact Eventually.of_forall fun x hxs => hxs
  rwa [setIntegral_const, smul_eq_mul, mul_comm] at h_const_le

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
h_int_gt : ∫ (x : α) in s, f x ∂μ ≤ b * (μ s).toReal
⊢ μ {x | f x ≤ b} = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
⊢ f ≤ᶠ[ae (μ.restrict s)] fun x => b

Tactic:
rw [EventuallyLE, ae_restrict_iff₀ (hs.mono μ.restrict_le_self)]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ b

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
h_const_le : ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, b ∂μ
⊢ ∫ (x : α) in s, f x ∂μ ≤ b * (μ s).toReal

Tactic:
rwa [setIntegral_const, smul_eq_mul, mul_comm] at h_const_le

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
⊢ μ {x | f x ≤ b} = 0

Tactic:
have hs : NullMeasurableSet s μ := nullMeasurableSet_le hf.1.aemeasurable aemeasurable_const

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
⊢ μ {x | f x ≤ b} = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
⊢ ∫ (x : α) in s, f x ∂μ ≤ b * (μ s).toReal

Tactic:
have h_const_le : (∫ x in s, f x ∂μ) ≤ ∫ _ in s, b ∂μ := by
  refine setIntegral_mono_ae_restrict hf.integrableOn (integrableOn_const.mpr (Or.inr mus)) ?_
  rw [EventuallyLE, ae_restrict_iff₀ (hs.mono μ.restrict_le_self)]
  exact Eventually.of_forall fun x hxs => hxs

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
h_const_le : ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, b ∂μ
⊢ ∫ (x : α) in s, f x ∂μ ≤ b * (μ s).toReal

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
⊢ μ {x | f x ≤ b} = 0

Tactic:
have mus : μ s < ∞ := Integrable.measure_le_lt_top hf hb_neg

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
⊢ μ {x | f x ≤ b} = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
H : μ {x | f x ≤ b} ≠ 0
⊢ 0 ≤ ∫ (x : α) in s, f x ∂μ

Tactic:
rw [← μ.restrict_toMeasurable mus.ne]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
H : μ {x | f x ≤ b} ≠ 0
⊢ 0 ≤ ∫ (x : α) in toMeasurable μ s, f x ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
⊢ ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, b ∂μ

Tactic:
refine setIntegral_mono_ae_restrict hf.integrableOn (integrableOn_const.mpr (Or.inr mus)) ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ⊤
⊢ f ≤ᶠ[ae (μ.restrict s)] fun x => b