awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)
refine_3 : Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm) (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
⊢ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) a ∂μ

Tactic:
rw [lintegral_iSup (fun n => Measurable.mono (hf n) hm le_rfl) hf_mono]

Premises used: le_rfl, MeasureTheory.lintegral_iSup, Measurable.mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)
refine_3 : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ.trim hm) (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)

Tactic:
congr with n
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)
n : ℕ
⊢ ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ

Tactic:
hf_prop n
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f_1 : α → ℝ≥0∞
hf_1 : Measurable f_1
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
hf_mono : Monotone f
hf_prop : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)
n : ℕ
⊢ ∫⁻ (a : α), f n a ∂μ.trim hm = ∫⁻ (a : α), f n a ∂μ

Tactic:
exact hf_prop n
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
rw : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
rw₁ : ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ.trim hm = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
rw₂ rw₃ : ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ

Tactic:
rw [lintegral_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk), lintegral_congr_ae hf.ae_eq_mk,
    lintegral_trim hm hf.measurable_mk]

Premises used: MeasureTheory.lintegral_congr_ae, MeasureTheory.lintegral_trim, MeasureTheory.ae_eq_of_ae_eq_trim, AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
rw : ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (a : α), f a ∂(μ.restrict s).trim hm
rw₁ : AEMeasurable f ((μ.restrict s).trim hm)
⊢ ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (x : α) in s, f x ∂μ

Tactic:
rw [← lintegral_trim_ae hm]

Premises used: MeasureTheory.lintegral_trim_ae
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
rw rw₁ : ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (a : α) in s, f a ∂μ.trim hm
⊢ ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (a : α), f a ∂(μ.restrict s).trim hm

Tactic:
rw [← restrict_trim hm _ hs]

Premises used: MeasureTheory.restrict_trim
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
rw : AEMeasurable f ((μ.trim hm).restrict s)
⊢ AEMeasurable f ((μ.restrict s).trim hm)

Tactic:
rw [← restrict_trim hm _ hs]

Premises used: MeasureTheory.restrict_trim
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f ((μ.trim hm).restrict s)

Tactic:
hf.restrict

Premises used: AEMeasurable.restrict
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f ((μ.trim hm).restrict s)

Tactic:
exact hf.restrict

Premises used: AEMeasurable.restrict
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, f x ∂μ.trim hm = ∫⁻ (x : α) in s, f x ∂μ

Tactic:
setLIntegral_trim_ae _ hf.aemeasurable hs

Premises used: Measurable.aemeasurable, MeasureTheory.setLIntegral_trim_ae
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
μ : Measure α
rw :
  ⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ (f : (a : α) → ℝ≥0∞) a), g.lintegral μ =
    f.lintegral μ
⊢ ∫⁻ (a : α), (f : (a : α) → ℝ≥0∞) a ∂μ = f.lintegral μ

Tactic:
rw [MeasureTheory.lintegral]

Premises used: MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
μ : Measure α
⊢ ⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ (f : (a : α) → ℝ≥0∞) a), g.lintegral μ =
    f.lintegral μ

Tactic:
le_antisymm (iSup₂_le fun g hg => lintegral_mono hg <| le_rfl)
    (le_iSup₂_of_le f le_rfl le_rfl)

Premises used: iSup₂_le, le_rfl, le_antisymm, MeasureTheory.SimpleFunc.lintegral_mono, le_iSup₂_of_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
μ : Measure α
⊢ ⨆ (g : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ (f : (a : α) → ℝ≥0∞) a), g.lintegral μ =
    f.lintegral μ

Tactic:
exact le_antisymm (iSup₂_le fun g hg => lintegral_mono hg <| le_rfl)
    (le_iSup₂_of_le f le_rfl le_rfl)

Premises used: iSup₂_le, le_rfl, le_antisymm, MeasureTheory.SimpleFunc.lintegral_mono, le_iSup₂_of_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
f g : α → ℝ≥0∞
hfg : f ≤ g
rw :
  LE.le (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
    (⨆ (g_1 : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ g a), g_1.lintegral ν)
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂ν

Tactic:
rw [lintegral, lintegral]

Premises used: MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
f g : α → ℝ≥0∞
hfg : f ≤ g
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
    (⨆ (g_1 : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ g a), g_1.lintegral ν)

Tactic:
iSup_mono fun φ => iSup_mono' fun hφ => ⟨le_trans hφ hfg, lintegral_mono (le_refl φ) hμν⟩

Premises used: le_refl, iSup_mono', MeasureTheory.SimpleFunc.lintegral_mono, Exists.intro, iSup_mono, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
f g : α → ℝ≥0∞
hfg : f ≤ g
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
    (⨆ (g_1 : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ g a), g_1.lintegral ν)

Tactic:
exact iSup_mono fun φ => iSup_mono' fun hφ => ⟨le_trans hφ hfg, lintegral_mono (le_refl φ) hμν⟩

Premises used: iSup_mono', Exists.intro, iSup_mono, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h2 : μ ≤ ν
f g : α → ℝ≥0∞
hfg : ∀ (x : α), f x ≤ g x
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂ν

Tactic:
lintegral_mono' h2 hfg

Premises used: MeasureTheory.lintegral_mono'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ g
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ

Tactic:
lintegral_mono' (le_refl μ) hfg

Premises used: le_refl, MeasureTheory.lintegral_mono'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0
h : f ≤ g
⊢ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ ∫⁻ (a : α), (↑(g a) : ℝ≥0∞) ∂μ

Tactic:
lintegral_mono fun a => ENNReal.coe_le_coe.2 (h a)

Premises used: Iff.mpr, ENNReal.coe_le_coe, MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
a : ⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ
a₁ : ∫⁻ (a : α), f a ∂μ ≤ ⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ
⊢ ⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
iSup_le fun i => iSup_le fun _ => iSup_le fun h'i => lintegral_mono h'i

Premises used: MeasureTheory.lintegral_mono, iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
exact iSup_le fun i => iSup_le fun _ => iSup_le fun h'i => lintegral_mono h'i

Premises used: MeasureTheory.lintegral_mono, iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
a :
  LE.le (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
    (⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ)
⊢ ∫⁻ (a : α), f a ∂μ ≤ ⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ

Tactic:
rw [lintegral]

Premises used: MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
    (⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ)

Tactic:
iSup₂_le fun i hi => le_iSup₂_of_le i i.measurable <| le_iSup_of_le hi ?_

Premises used: iSup₂_le, MeasureTheory.SimpleFunc.measurable, le_iSup_of_le, le_iSup₂_of_le, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
a :
  ∀ (i : α →ₛ ℝ≥0∞) (hi : LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a),
    i.lintegral μ ≤ ∫⁻ (a : α), (i : (a : α) → ℝ≥0∞) a ∂μ
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), g.lintegral μ)
    (⨆ (g : α → ℝ≥0∞), ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ)

Tactic:
refine iSup₂_le fun i hi => le_iSup₂_of_le i i.measurable <| le_iSup_of_le hi ?_

Premises used: iSup₂_le, le_iSup_of_le, le_iSup₂_of_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
i : α →ₛ ℝ≥0∞
hi : LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
⊢ i.lintegral μ ≤ ∫⁻ (a : α), (i : (a : α) → ℝ≥0∞) a ∂μ

Tactic:
le_of_eq (i.lintegral_eq_lintegral _).symm

Premises used: le_of_eq, Eq.symm, MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
i : α →ₛ ℝ≥0∞
hi : LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
⊢ i.lintegral μ ≤ ∫⁻ (a : α), (i : (a : α) → ℝ≥0∞) a ∂μ

Tactic:
exact le_of_eq (i.lintegral_eq_lintegral _).symm

Premises used: le_of_eq, Eq.symm, MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hst : s ⊆ t
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in t, f x ∂μ

Tactic:
lintegral_mono' (Measure.restrict_mono hst (le_refl μ)) (le_refl f)

Premises used: le_refl, MeasureTheory.Measure.restrict_mono, MeasureTheory.lintegral_mono'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hst : s ≤ᶠ[ae μ] t
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in t, f x ∂μ

Tactic:
lintegral_mono' (Measure.restrict_mono' hst (le_refl μ)) (le_refl f)

Premises used: MeasureTheory.Measure.restrict_mono', le_refl, MeasureTheory.lintegral_mono'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
⊢ Monotone (lintegral μ)

Tactic:
lintegral_mono

Premises used: Monotone, MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
rw : ∫⁻ (x : α), c ∂μ = ∫⁻ (a : α), Function.const α c a ∂μ
⊢ ∫⁻ (x : α), c ∂μ = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [← SimpleFunc.const_lintegral, ← SimpleFunc.lintegral_eq_lintegral, SimpleFunc.coe_const]

Premises used: MeasureTheory.SimpleFunc.const_lintegral, MeasureTheory.SimpleFunc.coe_const, MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ ∫⁻ (x : α), c ∂μ = ∫⁻ (a : α), Function.const α c a ∂μ

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ ∫⁻ (x : α), 0 ∂μ = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ lintegral μ 0 = 0

Tactic:
lintegral_zero

Premises used: MeasureTheory.lintegral_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) univ
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∫⁻ (x : α), 1 ∂μ = (μ : (a : Set α) → ℝ≥0∞) univ

Tactic:
rw [lintegral_const, one_mul]

Premises used: MeasureTheory.lintegral_const, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0∞
rw :
  HMul.hMul (β := ℝ≥0∞) c ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, c ∂μ = HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [lintegral_const, Measure.restrict_apply_univ]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.Measure.restrict_apply_univ
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, 1 ∂μ = (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
rw [setLIntegral_const, one_mul]

Premises used: MeasureTheory.setLIntegral_const, one_mul
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ (x : α), f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    ∫⁻ (y : α), ⨅ (x : α), f x ∂μ

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

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
x : α
⊢ ⨅ (x : α), f x ≤ f x

Tactic:
iInf_le _ _

Premises used: iInf_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
x : α
⊢ ⨅ (x : α), f x ≤ f x

Tactic:
exact iInf_le _ _

Premises used: iInf_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
calc :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ (x : α), f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    ∫⁻ (y : α), ⨅ (x : α), f x ∂μ
calc₁ : ∫⁻ (y : α), ⨅ (x : α), f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (⨅ (x : α), f x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ≤ ∫⁻ (x : α), f x ∂μ

Tactic:
calc (⨅ x, f x) * μ .univ
  _ = ∫⁻ y, ⨅ x, f x ∂μ := by simp
  _ ≤ ∫⁻ x, f x ∂μ := by gcongr; exact iInf_le _ _

Premises used: iInf, Set.univ, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfg : ∀ (x : α), f x ≤ ⨆ (x : α), f x
⊢ ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (y : α), ⨆ (x : α), f x ∂μ

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
x : α
⊢ f x ≤ ⨆ (x : α), f x

Tactic:
le_iSup _ _

Premises used: le_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
x : α
⊢ f x ≤ ⨆ (x : α), f x

Tactic:
exact le_iSup _ _

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

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

Tactic:
calc ∫⁻ x, f x ∂μ
  _ ≤ ∫⁻ y, ⨆ x, f x ∂μ := by gcongr; exact le_iSup _ _
  _ = (⨆ x, f x) * μ .univ := by simp

Premises used: iSup, Set.univ, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inl : ∀ (h₀ : ∫⁻ (a : α), f a ∂μ = 0), ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
inr : ∀ (h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0), ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
rcases eq_or_ne (∫⁻ a, f a ∂μ) 0 with h₀ | h₀

Premises used: eq_or_ne, OfNat.ofNat, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
⟨0, measurable_zero, zero_le, h₀.trans lintegral_zero.symm⟩

Premises used: zero_le, MeasureTheory.lintegral_zero, measurable_zero, And.intro, Exists.intro, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
exact ⟨0, measurable_zero, zero_le, h₀.trans lintegral_zero.symm⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
inr :
  ∀ (L : ℕ → ℝ≥0∞),
    StrictMono L →
      ∀ (hLf : ∀ (n : ℕ), L n ∈ Ioo ⊥ (∫⁻ (a : α), f a ∂μ)) (hL_tendsto : Tendsto L atTop (𝓝 (∫⁻ (a : α), f a ∂μ))),
        ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
rcases exists_seq_strictMono_tendsto' h₀.bot_lt with ⟨L, _, hLf, hL_tendsto⟩

Premises used: exists_seq_strictMono_tendsto', Ne.bot_lt
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
L : ℕ → ℝ≥0∞
left : StrictMono L
hLf : ∀ (n : ℕ), L n ∈ Ioo ⊥ (∫⁻ (a : α), f a ∂μ)
hL_tendsto : Tendsto L atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
n : ℕ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ L n < ∫⁻ (a : α), g a ∂μ

Tactic:
simpa only [← iSup_lintegral_measurable_le_eq_lintegral f, lt_iSup_iff, exists_prop] using
      (hLf n).2

Premises used: MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral, exists_prop, And.right, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
L : ℕ → ℝ≥0∞
left : StrictMono L
hLf : ∀ (n : ℕ), L n ∈ Ioo ⊥ (∫⁻ (a : α), f a ∂μ)
hL_tendsto : Tendsto L atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
⊢ ∀ (n : ℕ), ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ L n < ∫⁻ (a : α), g a ∂μ

Tactic:
have : ∀ n, ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f ∧ L n < ∫⁻ a, g a ∂μ := by
    intro n
    simpa only [← iSup_lintegral_measurable_le_eq_lintegral f, lt_iSup_iff, exists_prop] using
      (hLf n).2
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
L : ℕ → ℝ≥0∞
left : StrictMono L
hLf : ∀ (n : ℕ), L n ∈ Ioo ⊥ (∫⁻ (a : α), f a ∂μ)
hL_tendsto : Tendsto L atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
this : ∀ (n : ℕ), ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ L n < ∫⁻ (a : α), g a ∂μ
inr :
  ∀ (g : (n : ℕ) → α → ℝ≥0∞) (hgm : ∀ (n : ℕ), Measurable (g n)) (hgf : ∀ (n : ℕ), g n ≤ f)
    (hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ),
    ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
choose g hgm hgf hLg using this
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
L : ℕ → ℝ≥0∞
left : StrictMono L
hLf : ∀ (n : ℕ), L n ∈ Ioo ⊥ (∫⁻ (a : α), f a ∂μ)
hL_tendsto : Tendsto L atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
g : (n : ℕ) → α → ℝ≥0∞
hgm : ∀ (n : ℕ), Measurable (g n)
hgf : ∀ (n : ℕ), g n ≤ f
hLg : ∀ (n : ℕ), L n < ∫⁻ (a : α), g n a ∂μ
⊢ ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
⟨fun x => ⨆ n, g n x, .iSup hgm, fun x => iSup_le fun n => hgf n x, le_antisymm ?_ ?_⟩

Premises used: iSup, Measurable.iSup, le_antisymm, And.intro, Exists.intro, iSup_le