awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
s : Set β
hs : IsClosed[inst_3] s
t : ℕ → Set β := fun (n : ℕ) ↦ closure[inst_3] (compactCovering β n) ∩ s
rw : s = (⋃ (i : ℕ), closure[inst_3] (compactCovering β i)) ∩ s
rw₁ : s = Set.univ ∩ s
⊢ s = ⋃ (n : ℕ), t n
have rw₂ : s = s
Tactic: rw [← Set.iUnion_inter, iUnion_closure_compactCovering, Set.univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
s : Set β
hs : IsClosed[inst_3] s
t : ℕ → Set β := fun (n : ℕ) ↦ closure[inst_3] (compactCovering β n) ∩ s
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in s, f x ∂μ))
have B : s = ⋃ (n : ℕ), t n
Tactic: have B : s = ⋃ n, t n := by
    rw [← Set.iUnion_inter, iUnion_closure_compactCovering, Set.univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
s : Set β
hs : IsClosed[inst_3] s
t : ℕ → Set β := fun (n : ℕ) ↦ closure[inst_3] (compactCovering β n) ∩ s
B : s = ⋃ (n : ℕ), t n
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in s, f x ∂μ))
have rw : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in ⋃ (n : ℕ), t n, f x ∂μ))
Tactic: rw [B]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
s : Set β
hs : IsClosed[inst_3] s
t : ℕ → Set β := fun (n : ℕ) ↦ closure[inst_3] (compactCovering β n) ∩ s
B : s = ⋃ (n : ℕ), t n
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in ⋃ (n : ℕ), t n, f x ∂μ))
have hsm : ∀ (i : ℕ), MeasurableSet (t i)
Tactic: apply tendsto_setIntegral_of_monotone
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
s : Set β
hs : IsClosed[inst_3] s
t : ℕ → Set β := fun (n : ℕ) ↦ closure[inst_3] (compactCovering β n) ∩ s
B : s = ⋃ (n : ℕ), t n
hsm : ∀ (i : ℕ), MeasurableSet (t i)
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in ⋃ (n : ℕ), t n, f x ∂μ))
have h_mono : Monotone t
Tactic: apply tendsto_setIntegral_of_monotone
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
s : Set β
hs : IsClosed[inst_3] s
t : ℕ → Set β := fun (n : ℕ) ↦ closure[inst_3] (compactCovering β n) ∩ s
B : s = ⋃ (n : ℕ), t n
hsm : ∀ (i : ℕ), MeasurableSet (t i)
h_mono : Monotone t
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in ⋃ (n : ℕ), t n, f x ∂μ))
have hfi : IntegrableOn f (⋃ (n : ℕ), t n) μ
Tactic: apply tendsto_setIntegral_of_monotone
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
s : Set β
hs : IsClosed[inst_3] s
t : ℕ → Set β := fun (n : ℕ) ↦ closure[inst_3] (compactCovering β n) ∩ s
B : s = ⋃ (n : ℕ), t n
m n : ℕ
hmn : m ≤ n
⊢ t m ≤ t n
have h_mono : closure[inst_3] (compactCovering β m) ∩ s ⊆ closure[inst_3] (compactCovering β n) ∩ s
Tactic: simp only [t, Set.le_iff_subset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : LocallyIntegrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
⊢ f =ᶠ[ae μ] 0
have rw : f =ᶠ[ae (μ.restrict (⋃ (n : ℕ), closure[inst_3] (compactCovering β n)))] 0
Tactic: rw [← μ.restrict_univ, ← iUnion_closure_compactCovering]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : LocallyIntegrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
⊢ f =ᶠ[ae (μ.restrict (⋃ (n : ℕ), closure[inst_3] (compactCovering β n)))] 0
have apply : ∀ (n : ℕ), ∀ᵐ (x : β) ∂μ.restrict (closure[inst_3] (compactCovering β n)), f x = 0 x
Tactic: apply (ae_restrict_iUnion_iff _ _).2 (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : LocallyIntegrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
n : ℕ
⊢ ∀ᵐ (x : β) ∂μ.restrict (closure[inst_3] (compactCovering β n)), f x = 0 x
have hf₁ : Integrable f (μ.restrict (closure[inst_3] (compactCovering β n)))
Tactic: apply ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : LocallyIntegrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
n : ℕ
hf₁ : Integrable f (μ.restrict (closure[inst_3] (compactCovering β n)))
⊢ ∀ᵐ (x : β) ∂μ.restrict (closure[inst_3] (compactCovering β n)), f x = 0 x
have h'f₁ : ∀ (s : Set β),
  IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ.restrict (closure[inst_3] (compactCovering β n))) 0
Tactic: apply ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : LocallyIntegrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
n : ℕ
s : Set β
hs : IsCompact s
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ.restrict (closure[inst_3] (compactCovering β n))) 0
have h'f₁ : Eq.{u_2 + 1} (α := E) (∫ (x : β) in s ∩ closure[inst_3] (compactCovering β n), f x ∂μ) 0
Tactic: rw [Measure.restrict_restrict' measurableSet_closure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst : LinearOrder β
inst_1 : TopologicalSpace β
inst_2 : OrderTopology β
inst_3 : FirstCountableTopology β
f : α → β
c : β
⊢ (∀ᵐ (x : α) ∂μ, c ≤ f x) ↔ ∀ b < c, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
have simp_rw : (∀ b < c, ∀ᵐ (x : α) ∂μ, b < f x) ↔
  ∀ b < c, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [eventually_const_le_iff_forall_lt_eventually_const_lt, ae_iff, not_lt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst : LinearOrder β
inst_1 : TopologicalSpace β
inst_2 : OrderTopology β
inst_3 : FirstCountableTopology β
f : α → β
c : β
simp_rw :
  (∀ b < c, ∀ᵐ (x : α) ∂μ, b < f x) ↔
    ∀ b < c, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∀ᵐ (x : α) ∂μ, c ≤ f x) ↔ ∀ b < c, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
have simp_rw₁ : (∀ b < c, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬b < f a} : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  ∀ b < c, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [eventually_const_le_iff_forall_lt_eventually_const_lt, ae_iff, not_lt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
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
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have s_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have s_lt_top : μ s < ∞ :=
      (measure_mono (Set.inter_subset_right)).trans_lt (measure_spanningSets_lt_top μ p)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
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, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ + 0
have rw : ∫⁻ (x : α) in toMeasurable μ s, f x ∂μ ≤ ∫⁻ (x : α) in toMeasurable μ s, g x ∂μ
Tactic: rw [add_zero, ← Measure.restrict_toMeasurable s_lt_top.ne]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
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 ∂μ
have refine : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine h _ (measurableSet_toMeasurable ..) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
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∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have A : ∫⁻ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
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
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have B : ∫⁻ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
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 ∂μ ≠ ∞
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have this : HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ 0
Tactic: have : (ε : ℝ≥0∞) * μ s ≤ 0 := ENNReal.le_of_add_le_add_left B A
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
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 ∂μ
⊢ f ≤ᶠ[ae μ] g
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
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∞)
⊢ f ≤ᶠ[ae μ] g
have obtain : ∀ (u : ℕ → ℝ≥0), StrictAnti u → ∀ (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)), 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
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
⊢ f ≤ᶠ[ae μ] g
have μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have μs : ∀ n, μ (s n) = 0 := fun n => A _ _ _ (u_pos n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
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
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), s n) x
have hx₁ : g x < f x
Tactic: simp only [Set.mem_compl_iff, Set.mem_setOf, not_le] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
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
have this : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
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∞)))
⊢ ∀ᶠ (n : ℕ) in atTop, g x + (↑(u n) : ℝ≥0∞) ≤ f x
have this₁ : Tendsto (fun (n : ℕ) ↦ g x + (↑(u n) : ℝ≥0∞)) atTop (𝓝 (g x))
Tactic: simp only [ENNReal.coe_zero, add_zero] at this
Cleared hypotheses: this