awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p
s_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in toMeasurable μ s, f x ∂μ ≤ ∫⁻ (x : α) in toMeasurable μ s, g x ∂μ

Tactic:
h _ (measurableSet_toMeasurable ..) ?_

Premises used: MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p
s_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in toMeasurable μ s, f x ∂μ ≤ ∫⁻ (x : α) in toMeasurable μ s, g x ∂μ

Tactic:
refine h _ (measurableSet_toMeasurable ..) ?_

Premises used: MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p
s_lt_top rwa rwa₁ rwa₂ rwa₃ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [measure_toMeasurable]

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p
s_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, g x ∂μ + HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    ∫⁻ (x : α) in s, g x ∂μ + 0

Tactic:
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]
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p
s_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (x : α) in s, g x ∂μ + HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    ∫⁻ (x : α) in s, g x ∂μ + 0
⊢ ∫⁻ (x : α) in s, g x ∂μ ≠ ∞

Tactic:
have B : (∫⁻ x in s, g x ∂μ) ≠ ∞ :=
      (setLIntegral_lt_top_of_le_nnreal s_lt_top.ne ⟨N, fun _ h ↦ h.1.2⟩).ne
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p
s_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (x : α) in s, g x ∂μ + HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    ∫⁻ (x : α) in s, g x ∂μ + 0
B : ∫⁻ (x : α) in s, g x ∂μ ≠ ∞
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ 0

Tactic:
have : (ε : ℝ≥0∞) * μ s ≤ 0 := ENNReal.le_of_add_le_add_left B A
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p
s_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∫⁻ (x : α) in s, g x ∂μ + HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    ∫⁻ (x : α) in s, g x ∂μ + 0
B : ∫⁻ (x : α) in s, g x ∂μ ≠ ∞
this : HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ 0
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simpa only [ENNReal.coe_eq_zero, nonpos_iff_eq_zero, mul_eq_zero, εpos.ne', false_or]

Premises used: false_or, ENNReal.coe_eq_zero, mul_eq_zero, LT.lt.ne', nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
⊢ ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)

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]
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
⊢ ∃ (u : ℕ → ℝ≥0), StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0)

Tactic:
exists_seq_strictAnti_tendsto (0 : ℝ≥0)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
obtain : ∀ (u : ℕ → ℝ≥0), StrictAnti u → ∀ (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)), f ≤ᶠ[ae μ] g
⊢ f ≤ᶠ[ae μ] g

Tactic:
obtain ⟨u, _, u_pos, u_lim⟩ :
    ∃ u : ℕ → ℝ≥0, StrictAnti u ∧ (∀ n, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ≥0)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
⊢ ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have μs : ∀ n, μ (s n) = 0 := fun n => A _ _ _ (u_pos n)
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : Membership.mem (γ := Set α) {x : α | f x ≤ g x}ᶜ x
⊢ g x < f x

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

Premises used: not_le, Set.mem_setOf, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : g x < f x
⊢ Tendsto (fun (n : ℕ) ↦ g x + (↑(u n) : ℝ≥0∞)) atTop (𝓝 (g x + (↑0 : ℝ≥0∞)))

Tactic:
have : Tendsto (fun n => g x + u n) atTop (𝓝 (g x + (0 : ℝ≥0))) :=
        tendsto_const_nhds.add (ENNReal.tendsto_coe.2 u_lim)
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : g x < f x
this : Tendsto (fun (n : ℕ) ↦ g x + (↑(u n) : ℝ≥0∞)) atTop (𝓝 (g x + (↑0 : ℝ≥0∞)))
⊢ Tendsto (fun (n : ℕ) ↦ g x + (↑(u n) : ℝ≥0∞)) atTop (𝓝 (g x))

Tactic:
simp only [ENNReal.coe_zero, add_zero] at this

Premises used: ENNReal.coe_zero, add_zero
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : g x < f x
this : Tendsto (fun (n : ℕ) ↦ g x + (↑(u n) : ℝ≥0∞)) atTop (𝓝 (g x))
⊢ ∀ᶠ (n : ℕ) in atTop, g x + (↑(u n) : ℝ≥0∞) ≤ f x

Tactic:
this.eventually_le_const hx

Premises used: Filter.Tendsto.eventually_le_const
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : g x < f x
this : Tendsto (fun (n : ℕ) ↦ g x + (↑(u n) : ℝ≥0∞)) atTop (𝓝 (g x))
⊢ ∀ᶠ (n : ℕ) in atTop, g x + (↑(u n) : ℝ≥0∞) ≤ f x

Tactic:
exact this.eventually_le_const hx

Premises used: Filter.Tendsto.eventually_le_const
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : g x < f x
⊢ ∀ᶠ (n : ℕ) in atTop, g x + (↑(u n) : ℝ≥0∞) ≤ f x

Tactic:
have L1 : ∀ᶠ n in atTop, g x + u n ≤ f x := by
      have : Tendsto (fun n => g x + u n) atTop (𝓝 (g x + (0 : ℝ≥0))) :=
        tendsto_const_nhds.add (ENNReal.tendsto_coe.2 u_lim)
      simp only [ENNReal.coe_zero, add_zero] at this
      exact this.eventually_le_const hx
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : g x < f x
L1 : ∀ᶠ (n : ℕ) in atTop, g x + (↑(u n) : ℝ≥0∞) ≤ f x
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑n : ℝ≥0∞)) atTop (𝓝 ∞)

Tactic:
ENNReal.tendsto_nat_nhds_top

Premises used: ENNReal.tendsto_nat_nhds_top
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : g x < f x
L1 : ∀ᶠ (n : ℕ) in atTop, g x + (↑(u n) : ℝ≥0∞) ≤ f x
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (↑n : ℝ≥0∞)) atTop (𝓝 ∞)

Tactic:
exact ENNReal.tendsto_nat_nhds_top

Premises used: ENNReal.tendsto_nat_nhds_top
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : g x < f x
L1 : ∀ᶠ (n : ℕ) in atTop, g x + (↑(u n) : ℝ≥0∞) ≤ f x
⊢ ∀ᶠ (n : ℕ) in atTop, g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)

Tactic:
have L2 : ∀ᶠ n : ℕ in (atTop : Filter ℕ), g x ≤ (n : ℝ≥0) :=
      have : Tendsto (fun n : ℕ => ((n : ℝ≥0) : ℝ≥0∞)) atTop (𝓝 ∞) := by
        simp only [ENNReal.coe_natCast]
        exact ENNReal.tendsto_nat_nhds_top
      this.eventually_const_le (hx.trans_le le_top)
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : g x < f x
L1 : ∀ᶠ (n : ℕ) in atTop, g x + (↑(u n) : ℝ≥0∞) ≤ f x
L2 : ∀ᶠ (n : ℕ) in atTop, g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)
apply : ∃ (i : ℕ), x ∈ s i
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), s n) x

Tactic:
apply Set.mem_iUnion.2

Premises used: Iff.mpr, Set.mem_iUnion
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : g x < f x
L1 : ∀ᶠ (n : ℕ) in atTop, g x + (↑(u n) : ℝ≥0∞) ≤ f x
L2 : ∀ᶠ (n : ℕ) in atTop, g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)
⊢ ∃ (i : ℕ), x ∈ s i

Tactic:
((L1.and L2).and (eventually_mem_spanningSets μ x)).exists

Premises used: MeasureTheory.eventually_mem_spanningSets, Set.Mem, setOf, Filter.Eventually.and, Set.inter, Filter.Eventually.exists
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : g x < f x
L1 : ∀ᶠ (n : ℕ) in atTop, g x + (↑(u n) : ℝ≥0∞) ≤ f x
L2 : ∀ᶠ (n : ℕ) in atTop, g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)
⊢ ∃ (i : ℕ), x ∈ s i

Tactic:
exact ((L1.and L2).and (eventually_mem_spanningSets μ x)).exists

Premises used: MeasureTheory.eventually_mem_spanningSets, Filter.Eventually.and, Filter.Eventually.exists