awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), Measurable (α := α) (β := ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
⊢ LE.le.{u_1} (α := α → ℝ≥0∞) ((fun (n : ℕ) ↦ ((⇑(eapprox f n) : (a : α) → ℝ≥0∞) : (a : α) → ℝ≥0∞)) i)
    ((fun (n : ℕ) ↦ ((⇑(eapprox f n) : (a : α) → ℝ≥0∞) : (a : α) → ℝ≥0∞)) j)

Tactic:
monotone_eapprox f h

Premises used: MeasureTheory.SimpleFunc.monotone_eapprox
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
⊢ LE.le.{u_1} (α := α → ℝ≥0∞) ((fun (n : ℕ) ↦ ((⇑(eapprox f n) : (a : α) → ℝ≥0∞) : (a : α) → ℝ≥0∞)) i)
    ((fun (n : ℕ) ↦ ((⇑(eapprox f n) : (a : α) → ℝ≥0∞) : (a : α) → ℝ≥0∞)) j)

Tactic:
exact monotone_eapprox f h

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

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

Tactic:
ext n
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
e_s e_s₁ : SimpleFunc.lintegral (eapprox f n) μ = SimpleFunc.lintegral (eapprox f n) μ
⊢ ∫⁻ (a : α), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ∂μ = SimpleFunc.lintegral (eapprox f n) μ

Tactic:
rw [(eapprox f n).lintegral_eq_lintegral]

Premises used: MeasureTheory.SimpleFunc.eapprox, MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
rw : ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ = ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox (AEMeasurable.mk f hf) n) μ
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox (AEMeasurable.mk f hf) n) μ)
    (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox (AEMeasurable.mk f hf) n) μ)
⊢ ∫⁻ (a : α), f a ∂μ = ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox (AEMeasurable.mk f hf) n) μ

Tactic:
rw [lintegral_congr_ae hf.ae_eq_mk, lintegral_eq_iSup_eapprox_lintegral hf.measurable_mk]

Premises used: MeasureTheory.lintegral_congr_ae, AEMeasurable.ae_eq_mk, MeasureTheory.lintegral_eq_iSup_eapprox_lintegral, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
rw : SimpleFunc.lintegral (eapprox f n) μ ≤ ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ
⊢ SimpleFunc.lintegral (eapprox f n) μ ≤ ∫⁻ (x : α), f x ∂μ

Tactic:
rw [lintegral_eq_iSup_eapprox_lintegral hf]

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
n : ℕ
⊢ SimpleFunc.lintegral (eapprox f n) μ ≤ ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ

Tactic:
le_iSup (fun n ↦ (eapprox f n).lintegral μ) n

Premises used: MeasureTheory.SimpleFunc.lintegral, le_iSup, MeasureTheory.SimpleFunc.eapprox
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ SimpleFunc.lintegral (eapprox f n) μ ≤ ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ

Tactic:
exact le_iSup (fun n ↦ (eapprox f n).lintegral μ) n

Premises used: MeasureTheory.SimpleFunc.lintegral, le_iSup, MeasureTheory.SimpleFunc.eapprox
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf_meas : Measurable f
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support (M := ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
measure_support_lt_top_of_lintegral_ne_top <|
    ((lintegral_eapprox_le_lintegral hf_meas n).trans_lt hf.lt_top).ne

Premises used: MeasureTheory.lintegral_eapprox_le_lintegral, MeasureTheory.SimpleFunc.measure_support_lt_top_of_lintegral_ne_top, Ne.lt_top, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
simp :
  HAdd.hAdd (α := ℝ≥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 μ) ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a + g a), g_1.lintegral μ
⊢ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a + g a ∂μ

Tactic:
simp only [lintegral]

Premises used: MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
⊢ HAdd.hAdd (α := ℝ≥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 μ) ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a + g a), g_1.lintegral μ

Tactic:
ENNReal.biSup_add_biSup_le' (p := fun h : α →ₛ ℝ≥0∞ => h ≤ f)
    (q := fun h : α →ₛ ℝ≥0∞ => h ≤ g) ⟨0, zero_le⟩ ⟨0, zero_le⟩ fun f' hf' g' hg' => ?_

Premises used: zero_le, ENNReal.biSup_add_biSup_le', Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
refine :
  ∀ (f' : α →ₛ ℝ≥0∞) (hf' : (fun (h : α →ₛ ℝ≥0∞) ↦ (⇑h : (a : α) → ℝ≥0∞) ≤ f) f') (g' : α →ₛ ℝ≥0∞)
    (hg' : (fun (h : α →ₛ ℝ≥0∞) ↦ (⇑h : (a : α) → ℝ≥0∞) ≤ g) g'),
    f'.lintegral μ + g'.lintegral μ ≤
      ⨆ (g_1 : α →ₛ ℝ≥0∞),
        ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a + g a), g_1.lintegral μ
⊢ HAdd.hAdd (α := ℝ≥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 μ) ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a + g a), g_1.lintegral μ

Tactic:
refine ENNReal.biSup_add_biSup_le' (p := fun h : α →ₛ ℝ≥0∞ => h ≤ f)
    (q := fun h : α →ₛ ℝ≥0∞ => h ≤ g) ⟨0, zero_le⟩ ⟨0, zero_le⟩ fun f' hf' g' hg' => ?_

Premises used: zero_le, ENNReal.biSup_add_biSup_le', Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
f' : α →ₛ ℝ≥0∞
hf' : (fun (h : α →ₛ ℝ≥0∞) ↦ (⇑h : (a : α) → ℝ≥0∞) ≤ f) f'
g' : α →ₛ ℝ≥0∞
hg' : (fun (h : α →ₛ ℝ≥0∞) ↦ (⇑h : (a : α) → ℝ≥0∞) ≤ g) g'
⊢ f'.lintegral μ + g'.lintegral μ ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a + g a), g_1.lintegral μ

Tactic:
le_iSup₂_of_le (f' + g') (add_le_add hf' hg') (add_lintegral _ _).ge

Premises used: Eq.ge, add_le_add, MeasureTheory.SimpleFunc.add_lintegral, HAdd.hAdd, le_iSup₂_of_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
f' : α →ₛ ℝ≥0∞
hf' : (fun (h : α →ₛ ℝ≥0∞) ↦ (⇑h : (a : α) → ℝ≥0∞) ≤ f) f'
g' : α →ₛ ℝ≥0∞
hg' : (fun (h : α →ₛ ℝ≥0∞) ↦ (⇑h : (a : α) → ℝ≥0∞) ≤ g) g'
⊢ f'.lintegral μ + g'.lintegral μ ≤
    ⨆ (g_1 : α →ₛ ℝ≥0∞),
      ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g_1 : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a + g a), g_1.lintegral μ

Tactic:
exact le_iSup₂_of_le (f' + g') (add_le_add hf' hg') (add_lintegral _ _).ge

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

Tactic:
simp only [iSup_eapprox_apply, hf, hg]

Premises used: MeasureTheory.SimpleFunc.iSup_eapprox_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
e_f :
  Eq.{u_1 + 1} (α := α → ℝ≥0∞)
    (fun (a : α) ↦
      HAdd.hAdd (α := ℝ≥0∞) (⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a)
        (⨆ (n : ℕ), ((eapprox g n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a))
    fun (a : α) ↦
    ⨆ (n : ℕ),
      HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
        (⇑(eapprox g n) : (a : α) → ℝ≥0∞) a
⊢ ∫⁻ (a : α),
      HAdd.hAdd (α := ℝ≥0∞) (⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a)
        (⨆ (n : ℕ), ((eapprox g n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a) ∂μ =
    ∫⁻ (a : α),
      ⨆ (n : ℕ),
        HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
          (⇑(eapprox g n) : (a : α) → ℝ≥0∞) a ∂μ

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

Tactic:
funext a
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
e_f :
  Eq (α := ℝ≥0∞)
    (⨆ (a_1 : ℕ),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f a_1 : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (((eapprox g a_1 : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞))
    (⨆ (n : ℕ),
      HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
        (⇑(eapprox g n) : (a : α) → ℝ≥0∞) a)
e_f₁ : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a
e_f₂ : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ((eapprox g n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (n : ℕ), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a)
      (⨆ (n : ℕ), ((eapprox g n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a) =
    ⨆ (n : ℕ),
      HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
        (⇑(eapprox g n) : (a : α) → ℝ≥0∞) a

Tactic:
rw [ENNReal.iSup_add_iSup_of_monotone]

Premises used: ENNReal.iSup_add_iSup_of_monotone
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
⊢ Eq (α := ℝ≥0∞)
    (⨆ (a_1 : ℕ),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f a_1 : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (((eapprox g a_1 : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞))
    (⨆ (n : ℕ),
      HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
        (⇑(eapprox g n) : (a : α) → ℝ≥0∞) a)

Tactic:
simp only [Pi.add_apply]

Premises used: Pi.add_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
i j : ℕ
h : i ≤ j
⊢ LE.le (α := ℝ≥0∞) ((fun (n : ℕ) ↦ (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)) i)
    ((fun (n : ℕ) ↦ (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)) j)

Tactic:
monotone_eapprox _ h a

Premises used: MeasureTheory.SimpleFunc.monotone_eapprox
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
i j : ℕ
h : i ≤ j
⊢ LE.le (α := ℝ≥0∞) ((fun (n : ℕ) ↦ (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)) i)
    ((fun (n : ℕ) ↦ (((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)) j)

Tactic:
exact monotone_eapprox _ h a

Premises used: MeasureTheory.SimpleFunc.monotone_eapprox
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
i j : ℕ
h : i ≤ j
⊢ LE.le (α := ℝ≥0∞) ((fun (n : ℕ) ↦ (((eapprox g n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)) i)
    ((fun (n : ℕ) ↦ (((eapprox g n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)) j)

Tactic:
monotone_eapprox _ h a

Premises used: MeasureTheory.SimpleFunc.monotone_eapprox
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
a : α
i j : ℕ
h : i ≤ j
⊢ LE.le (α := ℝ≥0∞) ((fun (n : ℕ) ↦ (((eapprox g n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)) i)
    ((fun (n : ℕ) ↦ (((eapprox g n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)) j)

Tactic:
exact monotone_eapprox _ h a

Premises used: MeasureTheory.SimpleFunc.monotone_eapprox
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
rw :
  Eq (α := ℝ≥0∞)
    (⨆ (n : ℕ),
      ∫⁻ (a : α),
        HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
          (⇑(eapprox g n) : (a : α) → ℝ≥0∞) a ∂μ)
    (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ)
hf₁ :
  ∀ (n : ℕ),
    Measurable (HAdd.hAdd (α := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞) (⇑(eapprox g n) : (a : α) → ℝ≥0∞))
h_mono :
  Monotone.{0, u_1} (β := α → ℝ≥0∞) fun (n : ℕ) ↦
    HAdd.hAdd (α := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞) (⇑(eapprox g n) : (a : α) → ℝ≥0∞)
⊢ ∫⁻ (a : α),
      ⨆ (n : ℕ),
        HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
          (⇑(eapprox g n) : (a : α) → ℝ≥0∞) a ∂μ =
    ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ

Tactic:
rw [lintegral_iSup]

Premises used: MeasureTheory.lintegral_iSup
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
e_s :
  Eq (α := ℕ → ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (a : α),
        HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
          (⇑(eapprox g n) : (a : α) → ℝ≥0∞) a ∂μ)
    fun (n : ℕ) ↦ SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ
⊢ Eq (α := ℝ≥0∞)
    (⨆ (n : ℕ),
      ∫⁻ (a : α),
        HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
          (⇑(eapprox g n) : (a : α) → ℝ≥0∞) a ∂μ)
    (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
e_s :
  ∀ (n : ℕ),
    ∫⁻ (a : α),
        HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
          (⇑(eapprox g n) : (a : α) → ℝ≥0∞) a ∂μ =
      SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ
⊢ Eq (α := ℕ → ℝ≥0∞)
    (fun (n : ℕ) ↦
      ∫⁻ (a : α),
        HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
          (⇑(eapprox g n) : (a : α) → ℝ≥0∞) a ∂μ)
    fun (n : ℕ) ↦ SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ

Tactic:
funext n
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
n : ℕ
e_s :
  ∫⁻ (a : α),
      HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
        (⇑(eapprox g n) : (a : α) → ℝ≥0∞) a ∂μ =
    ∫⁻ (a : α), (HAdd.hAdd (α := α →ₛ ℝ≥0∞) (eapprox f n) (eapprox g n) : (a : α) → ℝ≥0∞) a ∂μ
⊢ ∫⁻ (a : α),
      HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
        (⇑(eapprox g n) : (a : α) → ℝ≥0∞) a ∂μ =
    SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ

Tactic:
rw [← SimpleFunc.add_lintegral, ← SimpleFunc.lintegral_eq_lintegral]

Premises used: MeasureTheory.SimpleFunc.add_lintegral, MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
n : ℕ
⊢ ∫⁻ (a : α),
      HAdd.hAdd (α := (a : α) → ℝ≥0∞) (β := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
        (⇑(eapprox g n) : (a : α) → ℝ≥0∞) a ∂μ =
    ∫⁻ (a : α), (HAdd.hAdd (α := α →ₛ ℝ≥0∞) (eapprox f n) (eapprox g n) : (a : α) → ℝ≥0∞) a ∂μ

Tactic:
simp only [Pi.add_apply, SimpleFunc.coe_add]

Premises used: MeasureTheory.SimpleFunc.coe_add, Pi.add_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ ∀ (n : ℕ),
    Measurable (HAdd.hAdd (α := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞) (⇑(eapprox g n) : (a : α) → ℝ≥0∞))

Tactic:
fun_prop
-- 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
a : α
h_mono :
  LE.le (α := ℝ≥0∞) (((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (((eapprox f j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
h_mono₁ :
  LE.le (α := ℝ≥0∞) (((eapprox g i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (((eapprox g j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (((eapprox g i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((eapprox f j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (((eapprox g j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
gcongr
-- 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
a : α
⊢ LE.le (α := ℝ≥0∞) (((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (((eapprox f j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
monotone_eapprox _ h _

Premises used: MeasureTheory.SimpleFunc.monotone_eapprox
-- 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
a : α
⊢ LE.le (α := ℝ≥0∞) (((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (((eapprox f j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
exact monotone_eapprox _ h _

Premises used: MeasureTheory.SimpleFunc.monotone_eapprox
-- 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
a : α
⊢ LE.le (α := ℝ≥0∞) (((eapprox g i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (((eapprox g j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
monotone_eapprox _ h _

Premises used: MeasureTheory.SimpleFunc.monotone_eapprox
-- 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
a : α
⊢ LE.le (α := ℝ≥0∞) (((eapprox g i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (((eapprox g j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
exact monotone_eapprox _ h _

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

Tactic:
(ENNReal.iSup_add_iSup_of_monotone ?_ ?_).symm

Premises used: ENNReal.iSup_add_iSup_of_monotone, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
refine_1 : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ SimpleFunc.lintegral (eapprox f n) μ
refine_2 : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ SimpleFunc.lintegral (eapprox g n) μ
⊢ ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ =
    HAdd.hAdd (α := ℝ≥0∞) (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ)
      (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox g n) μ)

Tactic:
refine (ENNReal.iSup_add_iSup_of_monotone ?_ ?_).symm

Premises used: ENNReal.iSup_add_iSup_of_monotone, Eq.symm
-- 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 f n) μ) i)
    ((fun (n : ℕ) ↦ SimpleFunc.lintegral (eapprox f n) μ) j)

Tactic:
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
i j : ℕ
h : i ≤ j
⊢ LE.le (α := ℝ≥0∞) ((fun (n : ℕ) ↦ SimpleFunc.lintegral (eapprox f n) μ) i)
    ((fun (n : ℕ) ↦ SimpleFunc.lintegral (eapprox f 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
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:
SimpleFunc.lintegral_mono (monotone_eapprox _ h) le_rfl

Premises used: le_rfl, MeasureTheory.SimpleFunc.monotone_eapprox, MeasureTheory.SimpleFunc.lintegral_mono