awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ ∫⁻ (a : α), ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a ∂μ = SimpleFunc.lintegral (eapprox f n) μ
have e_s : SimpleFunc.lintegral (eapprox f n) μ = SimpleFunc.lintegral (eapprox f n) μ
Tactic: rw [(eapprox f n).lintegral_eq_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (a : α), f a ∂μ = ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox (AEMeasurable.mk f hf) n) μ
have rw : ∫⁻ (a : α), AEMeasurable.mk f hf 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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) μ
⊢ ∫⁻ (a : α), f a ∂μ = ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox (AEMeasurable.mk f hf) n) μ
have rw₁ : Eq (α := ℝ≥0∞) (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox (AEMeasurable.mk f hf) n) μ)
  (⨆ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ SimpleFunc.lintegral (eapprox f n) μ ≤ ∫⁻ (x : α), f x ∂μ
have rw : SimpleFunc.lintegral (eapprox f n) μ ≤ ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ
Tactic: rw [lintegral_eq_iSup_eapprox_lintegral hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a + g a ∂μ
have 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 μ
Tactic: simp only [lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 μ
have 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 μ
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' => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ ∫⁻ (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 ∂μ
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ 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
have 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
Tactic: funext a
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
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
have 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)
Tactic: rw [ENNReal.iSup_add_iSup_of_monotone]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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)
⊢ 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
have e_f₁ : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ((eapprox f n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a
Tactic: rw [ENNReal.iSup_add_iSup_of_monotone]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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
⊢ 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
have e_f₂ : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ((eapprox g n : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a
Tactic: rw [ENNReal.iSup_add_iSup_of_monotone]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ ∫⁻ (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) μ
have 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) μ)
Tactic: rw [lintegral_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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) μ)
⊢ ∫⁻ (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) μ
have hf₁ : ∀ (n : ℕ),
  Measurable (HAdd.hAdd (α := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞) (⇑(eapprox g n) : (a : α) → ℝ≥0∞))
Tactic: rw [lintegral_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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∞))
⊢ ∫⁻ (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) μ
have h_mono : Monotone.{0, u_1} (β := α → ℝ≥0∞) fun (n : ℕ) ↦
  HAdd.hAdd (α := (a : α) → ℝ≥0∞) (⇑(eapprox f n) : (a : α) → ℝ≥0∞) (⇑(eapprox g n) : (a : α) → ℝ≥0∞)
Tactic: rw [lintegral_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ 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) μ)
have 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) μ
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ 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) μ
have 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) μ
Tactic: funext n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 ∂μ =
    SimpleFunc.lintegral (eapprox f n) μ + SimpleFunc.lintegral (eapprox g n) μ
have 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 ∂μ
Tactic: rw [← SimpleFunc.add_lintegral, ← SimpleFunc.lintegral_eq_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
i j : ℕ
h : i ≤ j
a : α
⊢ 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∞)
have h_mono : LE.le (α := ℝ≥0∞) (((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
  (((eapprox f j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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∞)
⊢ 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∞)
have h_mono₁ : LE.le (α := ℝ≥0∞) (((eapprox g i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
  (((eapprox g j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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) μ)
have refine_1 : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ SimpleFunc.lintegral (eapprox f n) μ
Tactic: refine (ENNReal.iSup_add_iSup_of_monotone ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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) μ
⊢ ⨆ (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) μ)
have refine_2 : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ SimpleFunc.lintegral (eapprox g n) μ
Tactic: refine (ENNReal.iSup_add_iSup_of_monotone ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ)
      (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox g n) μ) =
    ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
have 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 ∂μ
Tactic: rw [lintegral_eq_iSup_eapprox_lintegral hf, lintegral_eq_iSup_eapprox_lintegral hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 ∂μ
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ)
      (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox g n) μ) =
    ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
have 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) μ)
Tactic: rw [lintegral_eq_iSup_eapprox_lintegral hf, lintegral_eq_iSup_eapprox_lintegral hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 ∂μ
have refine : ∫⁻ (a : α), f a + g a ∂μ ≤ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
Tactic: refine le_antisymm ?_ (le_lintegral_add _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 ∂μ
have 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 ∂μ
Tactic: rcases exists_measurable_le_lintegral_eq μ fun a => f a + g a with ⟨φ, hφm, hφ_le, hφ_eq⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 : α), φ a - f a ∂μ ≤ ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
have bc : ∀ (a : α), φ a - f a ≤ g a
Tactic: gcongr with a
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
have f₁ : ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), φ a - f 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 _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
have rw : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf 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))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 ∂μ
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
have rw₁ : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf 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))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 ∂μ
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
have rw₂ : ∫⁻ (a : α), AEMeasurable.mk f hf a + g a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf 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))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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) μ
⊢ ∫⁻ (a_1 : α), ∑ b ∈ insert a s, f b a_1 ∂μ = ∑ b ∈ insert a s, ∫⁻ (a : α), f b a ∂μ
have 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 ∂μ
Tactic: simp only [Finset.sum_insert has]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
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) μ
⊢ ∫⁻ (a_1 : α), f a a_1 + ∑ b ∈ s, f b a_1 ∂μ = ∫⁻ (a_1 : α), f a a_1 ∂μ + ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
have hf₁ : AEMeasurable (f a) μ ∧ ∀ x ∈ s, AEMeasurable (f x) μ
Tactic: rw [Finset.forall_mem_insert] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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) μ
⊢ ∫⁻ (a_1 : α), f a a_1 + ∑ b ∈ s, f b a_1 ∂μ = ∫⁻ (a_1 : α), f a a_1 ∂μ + ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
have 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 ∂μ
Tactic: rw [lintegral_add_left' hf.1, ih hf.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 ∂μ
⊢ ∫⁻ (a_1 : α), f a a_1 + ∑ b ∈ s, f b a_1 ∂μ = ∫⁻ (a_1 : α), f a a_1 ∂μ + ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
have 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 ∂μ
Tactic: rw [lintegral_add_left' hf.1, ih hf.2]