awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Finset β
f : β → α → ℝ≥0∞
hf : ∀ b ∈ s, AEMeasurable (f b) μ
⊢ ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
have empty : ∀ (hf : ∀ (b : β), Membership.mem (γ := Finset β) ∅ b → AEMeasurable (f b) μ),
  ∫⁻ (a : α), ∑ b ∈ ∅, f b a ∂μ = ∑ b ∈ ∅, ∫⁻ (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]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 ∂μ
⊢ ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
have 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 a s, AEMeasurable (f b) μ),
  ∫⁻ (a_1 : α), ∑ b ∈ insert a s, f b a_1 ∂μ = ∑ b ∈ insert a 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]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Finset β
f : β → α → ℝ≥0∞
hf : ∀ b ∈ s, AEMeasurable (f b) μ
⊢ ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
have empty : ∀ (hf : ∀ (b : β), Membership.mem (γ := Finset β) ∅ b → AEMeasurable (f b) μ),
  ∫⁻ (a : α), ∑ b ∈ ∅, f b a ∂μ = ∑ b ∈ ∅, ∫⁻ (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]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 ∂μ
⊢ ∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
have 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 a s, AEMeasurable (f b) μ),
  ∫⁻ (a_1 : α), ∑ b ∈ insert a s, f b a_1 ∂μ = ∑ b ∈ insert a 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]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∫⁻ (a : α), ∑' (i : β), f i a ∂μ = ∑' (i : β), ∫⁻ (a : α), f i a ∂μ
have simp : ∫⁻ (a : α), ⨆ (s : Finset β), ∑ i ∈ s, f i a ∂μ = ⨆ (s : Finset β), ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ
Tactic: simp only [ENNReal.tsum_eq_iSup_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∫⁻ (a : α), ⨆ (s : Finset β), ∑ i ∈ s, f i a ∂μ = ⨆ (s : Finset β), ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ
have rw : Eq (α := ℝ≥0∞) (⨆ (b : Finset β), ∫⁻ (a : α), ∑ i ∈ b, f i a ∂μ) (⨆ (s : Finset β), ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ)
Tactic: rw [lintegral_iSup_directed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 ∂μ)
⊢ ∫⁻ (a : α), ⨆ (s : Finset β), ∑ i ∈ s, f i a ∂μ = ⨆ (s : Finset β), ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ
have hf₁ : ∀ (b : Finset β), AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ∑ i ∈ b, f i a) μ
Tactic: rw [lintegral_iSup_directed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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) μ
⊢ ∫⁻ (a : α), ⨆ (s : Finset β), ∑ i ∈ s, f i a ∂μ = ⨆ (s : Finset β), ∑ i ∈ s, ∫⁻ (a : α), f i a ∂μ
have h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) fun (s : Finset β) (a : α) ↦ ∑ i ∈ s, f i a
Tactic: rw [lintegral_iSup_directed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
s t : Finset β
⊢ ∃ (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)
have 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))
Tactic: use s ∪ t
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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)) ∧
    (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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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∞)) 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))
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i) μ
⊢ ∫⁻ (a : α), ∑' (i : β), f i a ∂μ = ∑' (i : β), ∫⁻ (a : α), f i a ∂μ
have simp : ∫⁻ (a : α), ⨆ (s : Finset β), ∑ i ∈ s, f i a ∂μ = ⨆ (s : Finset β), ∑ i ∈ s, ∫⁻ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 ∂μ
have simp₁ : Eq (α := ℝ≥0∞) (⨆ (b : Finset β), ∫⁻ (a : α), ∑ i ∈ b, f i a ∂μ) (⨆ (s : Finset β), ∑ i ∈ s, ∫⁻ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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 ∂μ)
⊢ ∫⁻ (a : α), ∑' (i : β), f i a ∂μ = ∑' (i : β), ∫⁻ (a : α), f i a ∂μ
have hf₁ : ∀ (b : Finset β), AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ∑ i ∈ b, 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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) μ
⊢ ∫⁻ (a : α), ∑' (i : β), f i a ∂μ = ∑' (i : β), ∫⁻ (a : α), f i a ∂μ
have h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) fun (s : Finset β) (a : α) ↦ ∑ i ∈ s, 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), r * f a ∂μ =
    ∫⁻ (a : α), ⨆ (n : ℕ), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable 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
have e_f : ∀ (a : α), r * f a = ⨆ (n : ℕ), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f 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 α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ r * f a = ⨆ (n : ℕ), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a
have 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)
Tactic: rw [← iSup_eapprox_apply hf, ENNReal.mul_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ =
    ⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ
have rw : Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ)
  (⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ)
Tactic: rw [lintegral_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
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) μ)
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ =
    ⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ
have hf₁ : ∀ (n : ℕ), Measurable (α := α) (β := ℝ≥0∞) (⇑(HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f 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 α
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∞)
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ =
    ⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ
have h_mono : Monotone.{0, u_1} (β := α → ℝ≥0∞) fun (n : ℕ) ↦
  (⇑(HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f 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 α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ)
    (⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ)
have 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) μ
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ Eq (α := ℕ → ℝ≥0∞)
    (fun (n : ℕ) ↦ ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ)
    fun (n : ℕ) ↦ r * SimpleFunc.lintegral (eapprox f n) μ
have e_s : ∀ (n : ℕ),
  ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ =
    r * SimpleFunc.lintegral (eapprox f n) μ
Tactic: funext n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
⊢ ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ =
    r * SimpleFunc.lintegral (eapprox f n) μ
have e_s : ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ =
  (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n)).lintegral μ
Tactic: rw [← SimpleFunc.const_mul_lintegral, ← SimpleFunc.lintegral_eq_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
e_s :
  ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ =
    (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n)).lintegral μ
⊢ ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ =
    r * SimpleFunc.lintegral (eapprox f n) μ
have e_s₁ : ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ =
  ∫⁻ (a : α), (HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n) : (a : α) → ℝ≥0∞) a ∂μ
Tactic: rw [← SimpleFunc.const_mul_lintegral, ← SimpleFunc.lintegral_eq_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
a : α
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0∞) a)
    ((fun (n : ℕ) ↦ ((⇑(HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n)) : (a : α) → ℝ≥0∞) : (a : α) → ℝ≥0∞)) i a)
    ((fun (n : ℕ) ↦ ((⇑(HMul.hMul (α := α →ₛ ℝ≥0∞) (const α r) (eapprox f n)) : (a : α) → ℝ≥0∞) : (a : α) → ℝ≥0∞)) j a)
have h_mono : HMul.hMul (β := ℝ≥0∞) r (((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞) r (((eapprox f j : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
i j : ℕ
h : i ≤ j
a : α
⊢ HMul.hMul (β := ℝ≥0∞) r (((eapprox f i : α →ₛ ℝ≥0∞) : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) r (((eapprox f 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 α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ = r * ∫⁻ (a : α), f a ∂μ
have rw : r * ⨆ (i : ℕ), SimpleFunc.lintegral (eapprox f i) μ = r * ∫⁻ (a : α), f a ∂μ
Tactic: rw [← ENNReal.mul_iSup, lintegral_eq_iSup_eapprox_lintegral hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
rw : r * ⨆ (i : ℕ), SimpleFunc.lintegral (eapprox f i) μ = r * ∫⁻ (a : α), f a ∂μ
⊢ ⨆ (n : ℕ), r * SimpleFunc.lintegral (eapprox f n) μ = r * ∫⁻ (a : α), f a ∂μ
have rw₁ : r * ⨆ (i : ℕ), SimpleFunc.lintegral (eapprox f i) μ = r * ⨆ (n : ℕ), SimpleFunc.lintegral (eapprox f n) μ
Tactic: rw [← ENNReal.mul_iSup, lintegral_eq_iSup_eapprox_lintegral hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
have A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
Tactic: have A : ∫⁻ a, f a ∂μ = ∫⁻ a, hf.mk f a ∂μ := lintegral_congr_ae hf.ae_eq_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
have B : ∫⁻ (a : α), r * f a ∂μ = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ
Tactic: have B : ∫⁻ a, r * f a ∂μ = ∫⁻ a, r * hf.mk f a ∂μ :=
    lintegral_congr_ae (EventuallyEq.fun_comp hf.ae_eq_mk _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
B : ∫⁻ (a : α), r * f a ∂μ = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
have rw : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
Tactic: rw [A, B, lintegral_const_mul _ hf.measurable_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
B : ∫⁻ (a : α), r * f a ∂μ = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ
rw : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
have rw₁ : ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ = r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
Tactic: rw [A, B, lintegral_const_mul _ hf.measurable_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
B : ∫⁻ (a : α), r * f a ∂μ = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ
rw : ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
rw₁ : ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ = r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
have rw₂ : r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ = r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
Tactic: rw [A, B, lintegral_const_mul _ hf.measurable_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ r * ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), r * f a ∂μ
have rw : ⨆ (i : α →ₛ ℝ≥0∞), r * ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), i.lintegral μ ≤
  ∫⁻ (a : α), r * f a ∂μ
Tactic: rw [lintegral, ENNReal.mul_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ ⨆ (i : α →ₛ ℝ≥0∞), r * ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑i : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), i.lintegral μ ≤
    ∫⁻ (a : α), r * f a ∂μ
have refine : ∀ (s : α →ₛ ℝ≥0∞),
  r * ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), s.lintegral μ ≤
    ∫⁻ (a : α), r * f a ∂μ
Tactic: refine iSup_le fun s => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
⊢ r * ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), s.lintegral μ ≤
    ∫⁻ (a : α), r * f a ∂μ
have rw : ∀ (i : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a), r * s.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ
Tactic: rw [ENNReal.mul_iSup, iSup_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : LE.le (α := (a : α) → ℝ≥0∞) (⇑s : (a : α) → ℝ≥0∞) fun (a : α) ↦ f a
⊢ r * s.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ
have rw : (const α r * s).lintegral μ ≤
  ⨆ (g : α →ₛ ℝ≥0∞), ⨆ (_ : LE.le (α := (a : α) → ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞) fun (a : α) ↦ r * f a), g.lintegral μ
Tactic: rw [← SimpleFunc.const_mul_lintegral, lintegral]