-- Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean
theorem ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ [SigmaFinite μ]
    {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
    (h : ∀ s, MeasurableSet s → μ s < ∞ → ∫⁻ x in s, f x ∂μ ≤ ∫⁻ x in s, g x ∂μ) :
    f ≤ᵐ[μ] g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε → μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : ℕ → Set α := fun n => {x | g x + ↑(u n) ≤ f x ∧ g x ≤ ↑↑n} ∩ spanningSets μ n
μs : ∀ (n : ℕ), μ (s n) = 0
B : {x | f x ≤ g x}ᶜ ⊆ ⋃ n, s n
⊢ ∑' (n : ℕ), μ (s n) = 0

Tactic:
simp only [μs, tsum_zero]

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε → μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : ℕ → Set α := fun n => {x | g x + ↑(u n) ≤ f x ∧ g x ≤ ↑↑n} ∩ spanningSets μ n
μs : ∀ (n : ℕ), μ (s n) = 0
B : {x | f x ≤ g x}ᶜ ⊆ ⋃ n, s n
⊢ μ {x | (fun x => f x ≤ g x) x}ᶜ ≤ 0

Tactic:
calc
  μ {x : α | (fun x : α => f x ≤ g x) x}ᶜ ≤ μ (⋃ n, s n) := measure_mono B
  _ ≤ ∑' n, μ (s n) := measure_iUnion_le _
  _ = 0 := by simp only [μs, tsum_zero]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
⊢ f ≤ᶠ[ae μ] g

Tactic:
have A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε →
    μ ({x | g x + ε ≤ f x ∧ g x ≤ N} ∩ spanningSets μ p) = 0 := by
  intro ε N p εpos
  let s := {x | g x + ε ≤ f x ∧ g x ≤ N} ∩ spanningSets μ p
  have s_lt_top : μ s < ∞ :=
    (measure_mono (Set.inter_subset_right)).trans_lt (measure_spanningSets_lt_top μ p)
  have A : (∫⁻ x in s, g x ∂μ) + ε * μ s ≤ (∫⁻ x in s, g x ∂μ) + 0 :=
    calc
      (∫⁻ x in s, g x ∂μ) + ε * μ s = (∫⁻ x in s, g x ∂μ) + ∫⁻ _ in s, ε ∂μ := by
        simp only [lintegral_const, Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply]
      _ = ∫⁻ x in s, g x + ε ∂μ := (lintegral_add_right _ measurable_const).symm
      _ ≤ ∫⁻ x in s, f x ∂μ :=
        setLIntegral_mono_ae hf.restrict <| ae_of_all _ fun x hx => hx.1.1
      _ ≤ (∫⁻ x in s, g x ∂μ) + 0 := by
        rw [add_zero, ← Measure.restrict_toMeasurable s_lt_top.ne]
        refine h _ (measurableSet_toMeasurable ..) ?_
        rwa [measure_toMeasurable]
  have B : (∫⁻ x in s, g x ∂μ) ≠ ∞ :=
    (setLIntegral_lt_top_of_le_nnreal s_lt_top.ne ⟨N, fun _ h ↦ h.1.2⟩).ne
  have : (ε : ℝ≥0∞) * μ s ≤ 0 := ENNReal.le_of_add_le_add_left B A
  simpa only [ENNReal.coe_eq_zero, nonpos_iff_eq_zero, mul_eq_zero, εpos.ne', false_or]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε → μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
⊢ f ≤ᶠ[ae μ] g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
⊢ μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0

Tactic:
let s := {x | g x + ε ≤ f x ∧ g x ≤ N} ∩ spanningSets μ p

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p
⊢ μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0

Proof state:
case intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε → μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ f ≤ᶠ[ae μ] g

Tactic:
let s := fun n : ℕ => {x | g x + u n ≤ f x ∧ g x ≤ (n : ℝ≥0)} ∩ spanningSets μ n

Result:
case intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε → μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : ℕ → Set α := fun n => {x | g x + ↑(u n) ≤ f x ∧ g x ≤ ↑↑n} ∩ spanningSets μ n
⊢ f ≤ᶠ[ae μ] g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε → μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : ℕ → Set α := fun n => {x | g x + ↑(u n) ≤ f x ∧ g x ≤ ↑↑n} ∩ spanningSets μ n
μs : ∀ (n : ℕ), μ (s n) = 0
x : α
hx : x ∈ {x | f x ≤ g x}ᶜ
⊢ x ∈ ⋃ n, s n

Tactic:
simp only [Set.mem_compl_iff, Set.mem_setOf, not_le] at hx

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε → μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : ℕ → Set α := fun n => {x | g x + ↑(u n) ≤ f x ∧ g x ≤ ↑↑n} ∩ spanningSets μ n
μs : ∀ (n : ℕ), μ (s n) = 0
x : α
hx : g x < f x
⊢ x ∈ ⋃ n, s n

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p
s_lt_top : μ s < ⊤
A : ∫⁻ (x : α) in s, g x ∂μ + ↑ε * μ s ≤ ∫⁻ (x : α) in s, g x ∂μ + 0
B : ∫⁻ (x : α) in s, g x ∂μ ≠ ⊤
⊢ μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0

Tactic:
have : (ε : ℝ≥0∞) * μ s ≤ 0 := ENNReal.le_of_add_le_add_left B A

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p
s_lt_top : μ s < ⊤
A : ∫⁻ (x : α) in s, g x ∂μ + ↑ε * μ s ≤ ∫⁻ (x : α) in s, g x ∂μ + 0
B : ∫⁻ (x : α) in s, g x ∂μ ≠ ⊤
this : ↑ε * μ s ≤ 0
⊢ μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0