awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h_1 : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x : α | (fun (a : α) ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ, x ∉ t
s : α →ₛ ℝ≥0∞
hfs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
a : α
h : a ∉ t
neg : (s : (a : α) → ℝ≥0∞) a ≤ g a
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0∞) a) ((s.restrict tᶜ : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((fun (a : α) ↦ g a) a : ℝ≥0∞)

Tactic:
simp only [restrict_apply s ht.compl, mem_compl_iff, h, not_true, not_false_eq_true,
        indicator_of_notMem, zero_le, not_false_eq_true, indicator_of_mem]

Premises used: zero_le, MeasurableSet.compl, Set.indicator_of_mem, MeasureTheory.SimpleFunc.restrict_apply, not_true, Set.indicator_of_notMem, not_false_eq_true, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h_1 : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x : α | (fun (a : α) ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ, x ∉ t
s : α →ₛ ℝ≥0∞
hfs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
a : α
h : a ∉ t
⊢ (s : (a : α) → ℝ≥0∞) a ≤ g a

Tactic:
le_trans (hfs a) (by_contradiction fun hnfg => h (hts hnfg))

Premises used: by_contradiction, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h_1 : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x : α | (fun (a : α) ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ, x ∉ t
s : α →ₛ ℝ≥0∞
hfs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
a : α
h : a ∉ t
⊢ (s : (a : α) → ℝ≥0∞) a ≤ g a

Tactic:
exact le_trans (hfs a) (by_contradiction fun hnfg => h (hts hnfg))

Premises used: by_contradiction, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x : α | (fun (a : α) ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ, x ∉ t
s : α →ₛ ℝ≥0∞
hfs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
a : α
hnt : a ∉ t
⊢ Eq (α := ℝ≥0∞) ((s : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((s.restrict tᶜ : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
simp [restrict_apply s ht.compl, hnt]

Premises used: MeasurableSet.compl, MeasureTheory.SimpleFunc.restrict_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
t : Set α
hts : {x : α | (fun (a : α) ↦ f a ≤ g a) x}ᶜ ⊆ t
ht : MeasurableSet t
ht0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ, x ∉ t
s : α →ₛ ℝ≥0∞
hfs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
⊢ s.lintegral μ ≤ (s.restrict tᶜ).lintegral μ

Tactic:
exact le_of_eq <| SimpleFunc.lintegral_congr <| this.mono fun a hnt => by
      simp [restrict_apply s ht.compl, hnt]

Premises used: MeasureTheory.SimpleFunc.lintegral_congr, Filter.Eventually.mono, le_of_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
rcases :
  ∀ (f' : α → ℝ≥0∞) (hf'm : Measurable f') (hle : f' ≤ f) (hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ),
    ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

Tactic:
rcases exists_measurable_le_lintegral_eq (μ.restrict s) f with ⟨f', hf'm, hle, hf'⟩

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.exists_measurable_le_lintegral_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
rw : ∫⁻ (a : α) in s, f' a ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

Tactic:
rw [hf']
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
h : ∀ᵐ (a : α) ∂μ.restrict s, f' a ≤ g a
⊢ ∫⁻ (a : α) in s, f' a ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

Tactic:
apply lintegral_mono_ae

Premises used: MeasureTheory.lintegral_mono_ae
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f' x ≤ g x
h₁ : NullMeasurableSet {x : α | f' x ≤ g x} (μ.restrict s)
⊢ ∀ᵐ (a : α) ∂μ.restrict s, f' a ≤ g a

Tactic:
rw [ae_restrict_iff₀]

Premises used: MeasureTheory.ae_restrict_iff₀
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f' x ≤ g x

Tactic:
hfg.mono fun x hx hxs ↦ (hle x).trans (hx hxs)

Premises used: Filter.Eventually.mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f' x ≤ g x

Tactic:
exact hfg.mono fun x hx hxs ↦ (hle x).trans (hx hxs)

Premises used: Filter.Eventually.mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ NullMeasurableSet {x : α | f' x ≤ g x} (μ.restrict s)

Tactic:
nullMeasurableSet_le hf'm.aemeasurable hg

Premises used: Measurable.aemeasurable, setOf, nullMeasurableSet_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : AEMeasurable g (μ.restrict s)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
f' : α → ℝ≥0∞
hf'm : Measurable f'
hle : f' ≤ f
hf' : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, f' a ∂μ
⊢ NullMeasurableSet {x : α | f' x ≤ g x} (μ.restrict s)

Tactic:
exact nullMeasurableSet_le hf'm.aemeasurable hg

Premises used: Measurable.aemeasurable, nullMeasurableSet_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hg : Measurable g
hfg : ∀ x ∈ s, f x ≤ g x
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

Tactic:
setLIntegral_mono_ae hg.aemeasurable (ae_of_all _ hfg)

Premises used: Measurable.aemeasurable, MeasureTheory.setLIntegral_mono_ae, MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

Tactic:
lintegral_mono_ae <| (ae_restrict_iff' hs).2 hfg

Premises used: Iff.mpr, MeasureTheory.lintegral_mono_ae, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hs : MeasurableSet s
hfg : ∀ x ∈ s, f x ≤ g x
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ

Tactic:
setLIntegral_mono_ae' hs (ae_of_all _ hfg)

Premises used: MeasureTheory.setLIntegral_mono_ae', MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ

Tactic:
lintegral_mono' Measure.restrict_le_self le_rfl

Premises used: le_rfl, MeasureTheory.lintegral_mono', MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ x ∈ s, f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    ∫⁻ (y : α) in s, ⨅ x ∈ s, f x ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (y : α) in s, ⨅ x ∈ s, f x ∂μ ≤ ∫⁻ (x : α) in s, f x ∂μ

Tactic:
setLIntegral_mono' hs fun x hx ↦ iInf₂_le x hx

Premises used: iInf₂_le, MeasureTheory.setLIntegral_mono'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
calc :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ x ∈ s, f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    ∫⁻ (y : α) in s, ⨅ x ∈ s, f x ∂μ
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ x ∈ s, f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ ∫⁻ (x : α) in s, f x ∂μ

Tactic:
calc (⨅ x ∈ s, f x) * μ s
  _ = ∫⁻ y in s, ⨅ x ∈ s, f x ∂μ := by simp
  _ ≤ ∫⁻ x in s, f x ∂μ := setLIntegral_mono' hs fun x hx ↦ iInf₂_le x hx

Premises used: iInf, iInf₂_le, DFunLike.coe, MeasureTheory.setLIntegral_mono'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (y : α) in s, ⨆ x ∈ s, f x ∂μ

Tactic:
setLIntegral_mono' hs fun x hx ↦ le_iSup₂ (f := fun x _ ↦ f x) x hx

Premises used: le_iSup₂, MeasureTheory.setLIntegral_mono'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (y : α) in s, ⨆ x ∈ s, f x ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨆ x ∈ s, f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
calc :
  ∫⁻ (y : α) in s, ⨆ x ∈ s, f x ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨆ x ∈ s, f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨆ x ∈ s, f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
calc ∫⁻ x in s, f x ∂μ
  _ ≤ ∫⁻ y in s, ⨆ x ∈ s, f x ∂μ :=
    setLIntegral_mono' hs fun x hx ↦ le_iSup₂ (f := fun x _ ↦ f x) x hx
  _ = (⨆ x ∈ s, f x) * μ s := by simp

Premises used: iSup, le_iSup₂, DFunLike.coe, MeasureTheory.setLIntegral_mono'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
⊢ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
le_antisymm (lintegral_mono_ae <| h.le) (lintegral_mono_ae <| h.symm.le)

Premises used: MeasureTheory.lintegral_mono_ae, Filter.EventuallyEq.le, le_antisymm, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ (a : α), f a = g a
⊢ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
simp only [h]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
h : s =ᶠ[ae μ] t
rw rw₁ : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ

Tactic:
rw [Measure.restrict_congr_set h]

Premises used: MeasureTheory.Measure.restrict_congr_set
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
rw : f =ᶠ[ae (μ.restrict s)] g
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

Tactic:
rw [lintegral_congr_ae]

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg rwa rwa₁ rwa₂ rwa₃ : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ∀ᵐ (x : α) ∂μ.restrict s, f x = g x

Tactic:
rwa [ae_restrict_iff' hs]

Premises used: MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hfg : EqOn f g s
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

Tactic:
setLIntegral_congr_fun_ae hs <| Eventually.of_forall hfg

Premises used: MeasureTheory.setLIntegral_congr_fun_ae, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
h's : EqOn f 0 s
⊢ ∫⁻ (x : α) in s, f x ∂μ = 0

Tactic:
simp [setLIntegral_congr_fun hs h's]

Premises used: MeasureTheory.setLIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : f =ᶠ[ae μ] 0
⊢ ∫⁻ (a : α), f a ∂μ = 0

Tactic:
(lintegral_congr_ae h).trans lintegral_zero

Premises used: MeasureTheory.lintegral_zero, MeasureTheory.lintegral_congr_ae, Eq.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
⟨fun h ↦ ?_, lintegral_eq_zero_of_ae_eq_zero⟩

Premises used: MeasureTheory.lintegral_eq_zero_of_ae_eq_zero, Iff.intro
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
refine : ∀ (h : ∫⁻ (a : α), f a ∂μ = 0), f =ᶠ[ae μ] 0
⊢ ∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
refine ⟨fun h ↦ ?_, lintegral_eq_zero_of_ae_eq_zero⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
ε : ℝ≥0∞
εpos : ε > 0
by_contra! : ∀ (h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)), False
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
by_contra! h'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
ε : ℝ≥0∞
εpos : ε > 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
((ENNReal.mul_pos εpos.ne' h').trans_le ?_).ne' h

Premises used: ENNReal.mul_pos, LT.lt.ne', LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
ε : ℝ≥0∞
εpos : ε > 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
refine : HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) ≤ ∫⁻ (a : α), f a ∂μ
⊢ False

Tactic:
refine ((ENNReal.mul_pos εpos.ne' h').trans_le ?_).ne' h

Premises used: ENNReal.mul_pos, LT.lt.ne', LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
ε : ℝ≥0∞
εpos : ε > 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫⁻ (x : α), f x ∂μ ≥ ∫⁻ (a : α) in {x : α | ε ≤ f x}, f a ∂μ

Tactic:
setLIntegral_le_lintegral _ _

Premises used: MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
ε : ℝ≥0∞
εpos : ε > 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫⁻ (a : α) in {x : α | ε ≤ f x}, f a ∂μ ≥ ∫⁻ (x : α) in {x : α | ε ≤ f x}, ε ∂μ

Tactic:
setLIntegral_mono_ae hf.restrict (ae_of_all μ fun _ ↦ id)

Premises used: MeasureTheory.setLIntegral_mono_ae, id, AEMeasurable.restrict, MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
ε : ℝ≥0∞
εpos : ε > 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫⁻ (x : α) in {x : α | ε ≤ f x}, ε ∂μ = HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞)

Tactic:
setLIntegral_const _ _

Premises used: MeasureTheory.setLIntegral_const
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
ε : ℝ≥0∞
εpos : ε > 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
calc
      _ ≥ ∫⁻ a in {x | ε ≤ f x}, f a ∂μ := setLIntegral_le_lintegral _ _
      _ ≥ ∫⁻ _ in {x | ε ≤ f x}, ε ∂μ :=
        setLIntegral_mono_ae hf.restrict (ae_of_all μ fun _ ↦ id)
      _ = _ := setLIntegral_const _ _

Premises used: MeasureTheory.setLIntegral_mono_ae, id, AEMeasurable.restrict, MeasureTheory.setLIntegral_const, MeasureTheory.ae_of_all, MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
⊢ ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have meas_levels_0 : ∀ ε > 0, μ { x | ε ≤ f x } = 0 := fun ε εpos ↦ by
    by_contra! h'
    refine ((ENNReal.mul_pos εpos.ne' h').trans_le ?_).ne' h
    calc
      _ ≥ ∫⁻ a in {x | ε ≤ f x}, f a ∂μ := setLIntegral_le_lintegral _ _
      _ ≥ ∫⁻ _ in {x | ε ≤ f x}, ε ∂μ :=
        setLIntegral_mono_ae hf.restrict (ae_of_all μ fun _ ↦ id)
      _ = _ := setLIntegral_const _ _
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
obtain :
  ∀ (u : ℕ → ℝ≥0∞) (bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)) (tu : Tendsto u atTop (𝓝 0)),
    f =ᶠ[ae μ] 0
⊢ f =ᶠ[ae μ] 0

Tactic:
obtain ⟨u, -, bu, tu⟩ := exists_seq_strictAnti_tendsto' (α := ℝ≥0∞) zero_lt_one

Premises used: exists_seq_strictAnti_tendsto', zero_lt_one
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : Tendsto u atTop (𝓝 0)
h₁ :
  ∀ (x : α),
    Membership.mem (γ := Set α) {x : α | f x ≠ 0} x ↔ Membership.mem (γ := Set α) (⋃ (n : ℕ), {x : α | u n ≤ f x}) x
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | f x ≠ 0} (⋃ (n : ℕ), {x : α | u n ≤ f x})

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : Tendsto u atTop (𝓝 0)
x : α
h₁ : 0 < f x ↔ ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
⊢ Membership.mem (γ := Set α) {x : α | f x ≠ 0} x ↔ Membership.mem (γ := Set α) (⋃ (n : ℕ), {x : α | u n ≤ f x}) x

Tactic:
rw [mem_iUnion, mem_setOf_eq, ← pos_iff_ne_zero]

Premises used: Set.mem_iUnion, Set.mem_setOf_eq, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : Tendsto u atTop (𝓝 0)
x : α
h₁ :
  ∀ (tu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, u n ≤ ε) (x : α),
    0 < f x ↔ ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
⊢ 0 < f x ↔ ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x

Tactic:
rw [ENNReal.tendsto_atTop_zero] at tu

Premises used: ENNReal.tendsto_atTop_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, u n ≤ ε
x : α
h₁ : 0 < f x → ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
h₂ : (∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x) → 0 < f x
⊢ 0 < f x ↔ ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, u n ≤ ε
x : α
h' : 0 < f x
h₁ : ∀ (n : ℕ) (hn : ∀ n_1 ≥ n, u n_1 ≤ f x), ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
⊢ ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x

Tactic:
obtain ⟨n, hn⟩ := tu _ h'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, u n ≤ ε
x : α
h' : 0 < f x
n : ℕ
hn : ∀ n_1 ≥ n, u n_1 ≤ f x
w : ℕ
h₁ : Membership.mem (γ := Set α) {x : α | u n ≤ f x} x
⊢ ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x

Tactic:
use n, hn _ le_rfl

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∫⁻ (a : α), f a ∂μ = 0
meas_levels_0 : ∀ ε > 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℕ → ℝ≥0∞
bu : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (u n)
tu : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, u n ≤ ε
x : α
h' : ∃ (i : ℕ), Membership.mem (γ := Set α) {x : α | u i ≤ f x} x
h₁ : ∀ (n : ℕ) (hn : Membership.mem (γ := Set α) {x : α | u n ≤ f x} x), 0 < f x
⊢ 0 < f x

Tactic:
obtain ⟨n, hn⟩ := h'