awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
i j : ℕ
h : i ≤ j
⊢ LE.le (α := ℝ≥0∞) ((fun (n : ℕ) ↦ SimpleFunc.lintegral (eapprox g n) μ) i)
    ((fun (n : ℕ) ↦ SimpleFunc.lintegral (eapprox g n) μ) j)

Tactic:
exact SimpleFunc.lintegral_mono (monotone_eapprox _ h) le_rfl

Premises used: le_rfl, MeasureTheory.SimpleFunc.monotone_eapprox, MeasureTheory.SimpleFunc.lintegral_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
rw :
  HAdd.hAdd (α := ℝ≥0∞) (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ)
      (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox g n) μ) =
    (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ) + ∫⁻ (a : α), g a ∂μ
rw₁ rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ)
      (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox g n) μ) =
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ)
      (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox g n) μ)
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ)
      (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox g n) μ) =
    ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
rw [lintegral_eq_iSup_eapprox_lintegral hf, lintegral_eq_iSup_eapprox_lintegral hg]

Premises used: MeasureTheory.lintegral_eq_iSup_eapprox_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
le_antisymm ?_ (le_lintegral_add _ _)

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

Tactic:
refine le_antisymm ?_ (le_lintegral_add _ _)

Premises used: le_antisymm, MeasureTheory.le_lintegral_add
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
rcases :
  ∀ (φ : α → ℝ≥0∞) (hφm : Measurable φ) (hφ_le : φ ≤ fun (a : α) ↦ f a + g a)
    (hφ_eq : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), φ a ∂μ),
    ∫⁻ (a : α), f a + g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), f a + g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
rcases exists_measurable_le_lintegral_eq μ fun a => f a + g a with ⟨φ, hφm, hφ_le, hφ_eq⟩

Premises used: HAdd.hAdd, MeasureTheory.exists_measurable_le_lintegral_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ fun (a : α) ↦ f a + g a
hφ_eq : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), φ a ∂μ

Tactic:
hφ_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ fun (a : α) ↦ f a + g a
hφ_eq : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ ∫⁻ (a : α), φ a ∂μ ≤ ∫⁻ (a : α), f a + (φ a - f a) ∂μ

Tactic:
lintegral_mono fun a => le_add_tsub

Premises used: MeasureTheory.lintegral_mono, le_add_tsub
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ fun (a : α) ↦ f a + g a
hφ_eq : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ ∫⁻ (a : α), f a + (φ a - f a) ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), φ a - f a ∂μ

Tactic:
lintegral_add_aux hf (hφm.sub hf)

Premises used: Measurable.sub, MeasureTheory.lintegral_add_aux
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ fun (a : α) ↦ f a + g a
hφ_eq : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), φ a ∂μ
bc : ∀ (a : α), φ a - f a ≤ g a
⊢ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), φ a - f a ∂μ ≤ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
gcongr with a
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ fun (a : α) ↦ f a + g a
hφ_eq : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), φ a ∂μ
a : α
⊢ φ a - f a ≤ g a

Tactic:
tsub_le_iff_left.2 <| hφ_le _

Premises used: Iff.mpr, tsub_le_iff_left
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ fun (a : α) ↦ f a + g a
hφ_eq : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), φ a ∂μ
a : α
⊢ φ a - f a ≤ g a

Tactic:
exact tsub_le_iff_left.2 <| hφ_le _

Premises used: Iff.mpr, tsub_le_iff_left
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ fun (a : α) ↦ f a + g a
hφ_eq : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), φ a ∂μ
f₁ : ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), φ a - f a ∂μ ≤ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), f a + g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
calc
    ∫⁻ a, f a + g a ∂μ = ∫⁻ a, φ a ∂μ := hφ_eq
    _ ≤ ∫⁻ a, f a + (φ a - f a) ∂μ := lintegral_mono fun a => le_add_tsub
    _ = ∫⁻ a, f a ∂μ + ∫⁻ a, φ a - f a ∂μ := lintegral_add_aux hf (hφm.sub hf)
    _ ≤ ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ := by gcongr with a; exact tsub_le_iff_left.2 <| hφ_le _

Premises used: Measurable.sub, MeasureTheory.lintegral_add_aux, MeasureTheory.lintegral_mono, le_add_tsub
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
rw : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ + ∫⁻ (a : α), g a ∂μ
rw₁ : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a + g a ∂μ
rw₂ rw₃ : ∫⁻ (a : α), AEMeasurable.mk f hf a + g a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a + g a ∂μ
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
rw [lintegral_congr_ae hf.ae_eq_mk, ← lintegral_add_left hf.measurable_mk,
    lintegral_congr_ae (hf.ae_eq_mk.fun_add (ae_eq_refl g))]

Premises used: MeasureTheory.ae_eq_refl, MeasureTheory.lintegral_add_left, MeasureTheory.lintegral_congr_ae, Filter.EventuallyEq.fun_add, AEMeasurable.ae_eq_mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
simpa only [add_comm] using lintegral_add_left' hg f

Premises used: MeasureTheory.lintegral_add_left', add_comm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
lintegral_add_right' f hg.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_add_right'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Membership.mem (γ := Finset β) ∅ b → AEMeasurable (f b) μ
⊢ ∫⁻ (a : α), ∑ b ∈ ∅, f b a ∂μ = ∑ b ∈ ∅, ∫⁻ (a : α), f b a ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f : β → α → ℝ≥0∞
a : β
s : Finset β
has : a ∉ s
ih : ∀ (hf : ∀ b ∈ s, AEMeasurable (f b) μ), ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
hf : ∀ b ∈ Insert.insert a s, AEMeasurable (f b) μ
insert : ∫⁻ (a_1 : α), f a a_1 + ∑ b ∈ s, f b a_1 ∂μ = ∫⁻ (a_1 : α), f a a_1 ∂μ + ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
⊢ ∫⁻ (a_1 : α), ∑ b ∈ Insert.insert a s, f b a_1 ∂μ = ∑ b ∈ Insert.insert a s, ∫⁻ (a : α), f b a ∂μ

Tactic:
simp only [Finset.sum_insert has]

Premises used: Finset.sum_insert
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f : β → α → ℝ≥0∞
a : β
s : Finset β
has : a ∉ s
ih : ∀ (hf : ∀ b ∈ s, AEMeasurable (f b) μ), ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
hf : ∀ b ∈ insert a s, AEMeasurable (f b) μ
⊢ AEMeasurable (f a) μ ∧ ∀ x ∈ s, AEMeasurable (f x) μ

Tactic:
rw [Finset.forall_mem_insert] at hf

Premises used: Finset.forall_mem_insert
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f : β → α → ℝ≥0∞
a : β
s : Finset β
has : a ∉ s
ih : ∀ (hf : ∀ b ∈ s, AEMeasurable (f b) μ), ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
hf : AEMeasurable (f a) μ ∧ ∀ x ∈ s, AEMeasurable (f x) μ
insert :
  ∫⁻ (a_1 : α), f a a_1 ∂μ + ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∫⁻ (a_1 : α), f a a_1 ∂μ + ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
insert₁ insert₂ :
  ∫⁻ (a_1 : α), f a a_1 ∂μ + ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ = ∫⁻ (a_1 : α), f a a_1 ∂μ + ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
⊢ ∫⁻ (a_1 : α), f a a_1 + ∑ b ∈ s, f b a_1 ∂μ = ∫⁻ (a_1 : α), f a a_1 ∂μ + ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ

Tactic:
rw [lintegral_add_left' hf.1, ih hf.2]

Premises used: MeasureTheory.lintegral_add_left', And.right, And.left
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Finset β
f : β → α → ℝ≥0∞
hf : ∀ b ∈ s, AEMeasurable (f b) μ
empty :
  ∀ (hf : ∀ (b : β), Membership.mem (γ := Finset β) ∅ b → AEMeasurable (f b) μ),
    ∫⁻ (a : α), ∑ b ∈ ∅, f b a ∂μ = ∑ b ∈ ∅, ∫⁻ (a : α), f b a ∂μ
insert :
  ∀ (a : β) (s : Finset β) (has : a ∉ s)
    (ih : ∀ (hf : ∀ b ∈ s, AEMeasurable (f b) μ), ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ)
    (hf : ∀ b ∈ Insert.insert a s, AEMeasurable (f b) μ),
    ∫⁻ (a_1 : α), ∑ b ∈ Insert.insert a s, f b a_1 ∂μ = ∑ b ∈ Insert.insert a s, ∫⁻ (a : α), f b a ∂μ
⊢ ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert a s has ih =>
    simp only [Finset.sum_insert has]
    rw [Finset.forall_mem_insert] at hf
    rw [lintegral_add_left' hf.1, ih hf.2]

Premises used: Finset.forall_mem_insert, Insert.insert
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Finset β
f : β → α → ℝ≥0∞
hf : ∀ b ∈ s, AEMeasurable (f b) μ
empty :
  ∀ (hf : ∀ (b : β), Membership.mem (γ := Finset β) ∅ b → AEMeasurable (f b) μ),
    ∫⁻ (a : α), ∑ b ∈ ∅, f b a ∂μ = ∑ b ∈ ∅, ∫⁻ (a : α), f b a ∂μ
insert :
  ∀ (a : β) (s : Finset β) (has : a ∉ s)
    (ih : ∀ (hf : ∀ b ∈ s, AEMeasurable (f b) μ), ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ)
    (hf : ∀ b ∈ Insert.insert a s, AEMeasurable (f b) μ),
    ∫⁻ (a_1 : α), ∑ b ∈ Insert.insert a s, f b a_1 ∂μ = ∑ b ∈ Insert.insert a s, ∫⁻ (a : α), f b a ∂μ
⊢ ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s has ih =>
    simp only [Finset.sum_insert has]
    rw [Finset.forall_mem_insert] at hf
    rw [lintegral_add_left' hf.1, ih hf.2]

Premises used: Finset.forall_mem_insert, Insert.insert
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Finset β
f : β → α → ℝ≥0∞
hf : ∀ b ∈ s, Measurable (f b)
⊢ ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ

Tactic:
lintegral_finsetSum' s fun b hb => (hf b hb).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_finsetSum'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
simp : ∫⁻ (a : α), ⨆ (s : Finset β), ∑ i ∈ s, f i a ∂μ = ⨆ (s : Finset β), ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ
⊢ ∫⁻ (a : α), ∑' (i : β), f i a ∂μ = ∑' (i : β), ∫⁻ (a : α), f i a ∂μ

Tactic:
simp only [ENNReal.tsum_eq_iSup_sum]

Premises used: ENNReal.tsum_eq_iSup_sum
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
rw : Eq (α := ℝ≥0∞) (⨆ (b : Finset β), ∫⁻ (a : α), ∑ i ∈ b, f i a ∂μ) (⨆ (s : Finset β), ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ)
hf₁ : ∀ (b : Finset β), AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ∑ i ∈ b, f i a) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) fun (s : Finset β) (a : α) ↦ ∑ i ∈ s, f i a
⊢ ∫⁻ (a : α), ⨆ (s : Finset β), ∑ i ∈ s, f i a ∂μ = ⨆ (s : Finset β), ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ

Tactic:
rw [lintegral_iSup_directed]

Premises used: MeasureTheory.lintegral_iSup_directed
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ Eq (α := ℝ≥0∞) (⨆ (b : Finset β), ∫⁻ (a : α), ∑ i ∈ b, f i a ∂μ) (⨆ (s : Finset β), ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ)

Tactic:
simp [lintegral_finsetSum' _ fun i _ => hf i]

Premises used: MeasureTheory.lintegral_finsetSum'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
b : Finset β
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ∑ i ∈ b, f i a) μ

Tactic:
Finset.aemeasurable_fun_sum _ fun i _ => hf i

Premises used: Finset.aemeasurable_fun_sum
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
b : Finset β
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ∑ i ∈ b, f i a) μ

Tactic:
exact Finset.aemeasurable_fun_sum _ fun i _ => hf i

Premises used: Finset.aemeasurable_fun_sum
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
h :
  (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) s)
      ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) (s ∪ t)) ∧
    (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) t)
      ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) (s ∪ t))
⊢ ∃ (z : Finset β),
    (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) s)
        ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) z) ∧
      (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) t)
        ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) z)

Tactic:
use s ∪ t
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
h :
  (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) s)
    ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) (s ∪ t))
h₁ :
  (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) t)
    ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) (s ∪ t))
⊢ (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) s)
      ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) (s ∪ t)) ∧
    (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) t)
      ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) (s ∪ t))

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) s)
    ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) (s ∪ t))

Tactic:
fun a => Finset.sum_le_sum_of_subset Finset.subset_union_left

Premises used: Finset.subset_union_left, Finset.sum_le_sum_of_subset
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) s)
    ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) (s ∪ t))

Tactic:
exact fun a => Finset.sum_le_sum_of_subset Finset.subset_union_left

Premises used: Finset.subset_union_left, Finset.sum_le_sum_of_subset
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) t)
    ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) (s ∪ t))

Tactic:
fun a => Finset.sum_le_sum_of_subset Finset.subset_union_right

Premises used: Finset.sum_le_sum_of_subset, Finset.subset_union_right
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) t)
    ((fun (s : Finset β) (a : α) ↦ (∑ i ∈ s, f i a : ℝ≥0∞)) (s ∪ t))

Tactic:
exact fun a => Finset.sum_le_sum_of_subset Finset.subset_union_right

Premises used: Finset.sum_le_sum_of_subset, Finset.subset_union_right
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
simp : ∫⁻ (a : α), ⨆ (s : Finset β), ∑ i ∈ s, f i a ∂μ = ⨆ (s : Finset β), ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ
simp₁ :
  Eq (α := ℝ≥0∞) (⨆ (b : Finset β), ∫⁻ (a : α), ∑ i ∈ b, f i a ∂μ) (⨆ (s : Finset β), ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ)
hf₁ : ∀ (b : Finset β), AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ∑ i ∈ b, f i a) μ
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) fun (s : Finset β) (a : α) ↦ ∑ i ∈ s, f i a
hf₂ : ∀ (b : Finset β), AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ∑ i ∈ b, f i a) μ
h_directed₁ h_directed₂ : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) fun (s : Finset β) (a : α) ↦ ∑ i ∈ s, f i a
⊢ ∫⁻ (a : α), ∑' (i : β), f i a ∂μ = ∑' (i : β), ∫⁻ (a : α), f i a ∂μ

Tactic:
classical
  simp only [ENNReal.tsum_eq_iSup_sum]
  rw [lintegral_iSup_directed]
  · simp [lintegral_finsetSum' _ fun i _ => hf i]
  · intro b
    exact Finset.aemeasurable_fun_sum _ fun i _ => hf i
  · intro s t
    use s ∪ t
    constructor
    · exact fun a => Finset.sum_le_sum_of_subset Finset.subset_union_left
    · exact fun a => Finset.sum_le_sum_of_subset Finset.subset_union_right

Premises used: MeasureTheory.lintegral_iSup_directed, Finset.aemeasurable_fun_sum, ENNReal.tsum_eq_iSup_sum, Finset.subset_union_left, Finset.sum_le_sum_of_subset, Finset.subset_union_right, MeasureTheory.lintegral_finsetSum'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
e_f :
  Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (a : α) ↦ r * f a) fun (a : α) ↦
    ⨆ (n : ℕ), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a
⊢ ∫⁻ (a : α), r * f a ∂μ =
    ∫⁻ (a : α), ⨆ (n : ℕ), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
e_f : ∀ (a : α), r * f a = ⨆ (n : ℕ), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (a : α) ↦ r * f a) fun (a : α) ↦
    ⨆ (n : ℕ), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a

Tactic:
funext a
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
a : α
e_f :
  Eq (α := ℝ≥0∞) (⨆ (i : ℕ), HMul.hMul (β := ℝ≥0∞) r (((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞))
    (⨆ (n : ℕ), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a)
⊢ r * f a = ⨆ (n : ℕ), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a

Tactic:
rw [← iSup_eapprox_apply hf, ENNReal.mul_iSup]

Premises used: MeasureTheory.SimpleFunc.iSup_eapprox_apply, ENNReal.mul_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ℕ), HMul.hMul (β := ℝ≥0∞) r (((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞))
    (⨆ (n : ℕ), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
rw :
  Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ)
    (⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ)
hf₁ :
  ∀ (n : ℕ), Measurable (α := α) (β := ℝ≥0∞) (⇑(HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n)) : (a : α) → ℝ≥0∞)
h_mono :
  Monotone.{0, u_1} (β := α → ℝ≥0∞) fun (n : ℕ) ↦
    (⇑(HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n)) : (a : α) → ℝ≥0∞)
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ =
    ⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ

Tactic:
rw [lintegral_iSup]

Premises used: MeasureTheory.lintegral_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
e_s :
  Eq (α := ℕ → ℝ≥0∞)
    (fun (n : ℕ) ↦ ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ)
    fun (n : ℕ) ↦ r * SimpleFunc.lintegral (eapprox f n) μ
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ)
    (⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
e_s :
  ∀ (n : ℕ),
    ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ =
      r * SimpleFunc.lintegral (eapprox f n) μ
⊢ Eq (α := ℕ → ℝ≥0∞)
    (fun (n : ℕ) ↦ ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ)
    fun (n : ℕ) ↦ r * SimpleFunc.lintegral (eapprox f n) μ

Tactic:
funext n