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∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ⨆ (n : ℕ), ∫⁻ (x : α), f n x ∂μ
have rw : ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ
Tactic: rw [← lintegral_iSup' hf h_mono]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ
have refine : F =ᶠ[ae μ] fun (a : α) ↦ ⨆ (n : ℕ), f n a
Tactic: refine lintegral_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
⊢ F =ᶠ[ae μ] fun (a : α) ↦ ⨆ (n : ℕ), f n a
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ F x = (fun (a : α) ↦ (⨆ (n : ℕ), f n a : ℝ≥0∞)) x) x}
                x}
          x}
    a
Tactic: filter_upwards [h_mono, h_tendsto] with _ hx_mono hx_tendsto using
    tendsto_nhds_unique hx_tendsto (tendsto_atTop_iSup hx_mono)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∫⁻ (x : α), f n x ∂μ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))) x} x →
                Membership.mem (γ := Set α)
                  {x : α | (fun (x : α) ↦ F x = (fun (a : α) ↦ (⨆ (n : ℕ), f n a : ℝ≥0∞)) x) x} x}
            x}
      a
⊢ F =ᶠ[ae μ] fun (a : α) ↦ ⨆ (n : ℕ), f n a
have h₁ : ∀ (a : α),
  (Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ f n a) → Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 (F a)) → F a = ⨆ (n : ℕ), f n a
Tactic: filter_upwards [h_mono, h_tendsto] with _ hx_mono hx_tendsto using
    tendsto_nhds_unique hx_tendsto (tendsto_atTop_iSup hx_mono)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have let : ∀ (s : Set α)
  (hs :
    {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
      MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
Tactic: let ⟨s, hs⟩ := exists_measurable_superset_of_null (ae_iff.1 (ae_all_iff.2 h_mono))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
Tactic: have g_eq_f : ∀ᵐ a ∂μ, ∀ n, g n a = f n a :=
    (measure_eq_zero_iff_ae_notMem.1 hs.2.2).mono fun a ha n => if_neg ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have f₁ : ∀ (n : ℕ) (a : α), g n a ≤ g (n + 1) a
Tactic: calc
    ∫⁻ a, ⨆ n, f n a ∂μ = ∫⁻ a, ⨆ n, g n a ∂μ :=
      lintegral_congr_ae <| g_eq_f.mono fun a ha => by simp only [ha]
    _ = ⨆ n, ∫⁻ a, g n a ∂μ :=
      (lintegral_iSup (fun n => measurable_const.piecewise hs.2.1 (hf n))
        (monotone_nat_of_le_succ fun n a => ?_))
    _ = ⨆ n, ∫⁻ a, f n a ∂μ := by simp only [lintegral_congr_ae (g_eq_f.mono fun _a ha => ha _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
⊢ (if a ∈ s then 0 else f n a) ≤ if a ∈ s then 0 else f (n + 1) a
have pos : ∀ (h : a ∈ s), LE.le (α := ℝ≥0∞) 0 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
pos : ∀ (h : a ∈ s), LE.le (α := ℝ≥0∞) 0 0
⊢ (if a ∈ s then 0 else f n a) ≤ if a ∈ s then 0 else f (n + 1) a
have neg : ∀ (h : a ∉ s), f n a ≤ f (n + 1) a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
h : a ∉ s
⊢ f n a ≤ f (n + 1) a
have this : a ∉ {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a}
Tactic: have := Set.notMem_subset hs.1 h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs :
  {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
    MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
h : a ∉ s
this : a ∉ {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a}
⊢ f n a ≤ f (n + 1) a
have this₁ : ∀ (x : ℕ), f x a ≤ f x.succ a
Tactic: simp only [not_forall, not_le, mem_setOf_eq, not_exists, not_lt] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have let : ∀ (s : Set α)
  (hs :
    {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
      MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
Tactic: classical
  let ⟨s, hs⟩ := exists_measurable_superset_of_null (ae_iff.1 (ae_all_iff.2 h_mono))
  let g n a := if a ∈ s then 0 else f n a
  have g_eq_f : ∀ᵐ a ∂μ, ∀ n, g n a = f n a :=
    (measure_eq_zero_iff_ae_notMem.1 hs.2.2).mono fun a ha n => if_neg ha
  calc
    ∫⁻ a, ⨆ n, f n a ∂μ = ∫⁻ a, ⨆ n, g n a ∂μ :=
      lintegral_congr_ae <| g_eq_f.mono fun a ha => by simp only [ha]
    _ = ⨆ n, ∫⁻ a, g n a ∂μ :=
      (lintegral_iSup (fun n => measurable_const.piecewise hs.2.1 (hf n))
        (monotone_nat_of_le_succ fun n a => ?_))
    _ = ⨆ n, ∫⁻ a, f n a ∂μ := by simp only [lintegral_congr_ae (g_eq_f.mono fun _a ha => ha _)]
  simp only [g]
  split_ifs with h
  · rfl
  · have := Set.notMem_subset hs.1 h
    simp only [not_forall, not_le, mem_setOf_eq, not_exists, not_lt] at this
    exact this n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
let let₁ let₂ let₃ :
  ∀ (s : Set α)
    (hs :
      {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
        MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have let₄ : ∀ (s : Set α)
  (hs :
    {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
      MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  let g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a;
  ∀ (g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a),
    ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
Tactic: classical
  let ⟨s, hs⟩ := exists_measurable_superset_of_null (ae_iff.1 (ae_all_iff.2 h_mono))
  let g n a := if a ∈ s then 0 else f n a
  have g_eq_f : ∀ᵐ a ∂μ, ∀ n, g n a = f n a :=
    (measure_eq_zero_iff_ae_notMem.1 hs.2.2).mono fun a ha n => if_neg ha
  calc
    ∫⁻ a, ⨆ n, f n a ∂μ = ∫⁻ a, ⨆ n, g n a ∂μ :=
      lintegral_congr_ae <| g_eq_f.mono fun a ha => by simp only [ha]
    _ = ⨆ n, ∫⁻ a, g n a ∂μ :=
      (lintegral_iSup (fun n => measurable_const.piecewise hs.2.1 (hf n))
        (monotone_nat_of_le_succ fun n a => ?_))
    _ = ⨆ n, ∫⁻ a, f n a ∂μ := by simp only [lintegral_congr_ae (g_eq_f.mono fun _a ha => ha _)]
  simp only [g]
  split_ifs with h
  · rfl
  · have := Set.notMem_subset hs.1 h
    simp only [not_forall, not_le, mem_setOf_eq, not_exists, not_lt] at this
    exact this n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
let let₁ let₂ let₃ :
  ∀ (s : Set α)
    (hs :
      {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
        MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
let₄ :
  ∀ (s : Set α)
    (hs :
      {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
        MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    let g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a;
    ∀ (g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a),
      ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have let₅ : ∀ (s : Set α)
  (hs :
    {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
      MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  let g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a;
  ∀ (g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a) (n : ℕ) (a : α), g n a ≤ g (n + 1) a
Tactic: classical
  let ⟨s, hs⟩ := exists_measurable_superset_of_null (ae_iff.1 (ae_all_iff.2 h_mono))
  let g n a := if a ∈ s then 0 else f n a
  have g_eq_f : ∀ᵐ a ∂μ, ∀ n, g n a = f n a :=
    (measure_eq_zero_iff_ae_notMem.1 hs.2.2).mono fun a ha n => if_neg ha
  calc
    ∫⁻ a, ⨆ n, f n a ∂μ = ∫⁻ a, ⨆ n, g n a ∂μ :=
      lintegral_congr_ae <| g_eq_f.mono fun a ha => by simp only [ha]
    _ = ⨆ n, ∫⁻ a, g n a ∂μ :=
      (lintegral_iSup (fun n => measurable_const.piecewise hs.2.1 (hf n))
        (monotone_nat_of_le_succ fun n a => ?_))
    _ = ⨆ n, ∫⁻ a, f n a ∂μ := by simp only [lintegral_congr_ae (g_eq_f.mono fun _a ha => ha _)]
  simp only [g]
  split_ifs with h
  · rfl
  · have := Set.notMem_subset hs.1 h
    simp only [not_forall, not_le, mem_setOf_eq, not_exists, not_lt] at this
    exact this n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
let let₁ let₂ let₃ :
  ∀ (s : Set α)
    (hs :
      {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
        MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
let₄ :
  ∀ (s : Set α)
    (hs :
      {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
        MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    let g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a;
    ∀ (g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a),
      ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
let₅ :
  ∀ (s : Set α)
    (hs :
      {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
        MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    let g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a;
    ∀ (g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a) (n : ℕ) (a : α), g n a ≤ g (n + 1) a
let₆ :
  ∀ (s : Set α)
    (hs :
      {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
        MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    let g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a;
    ∀ (g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a) (n : ℕ) (a : α),
      (if a ∈ s then 0 else f n a) ≤ if a ∈ s then 0 else f (n + 1) a
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have pos : ∀ (s : Set α)
  (hs :
    {a : α | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧
      MeasurableSet s ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  let g : (n : ℕ) → (a : α) → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ if a ∈ s then 0 else f n a;
  ∀ (g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a) (n : ℕ) (a : α) (h : a ∈ s), LE.le (α := ℝ≥0∞) 0 0
Tactic: classical
  let ⟨s, hs⟩ := exists_measurable_superset_of_null (ae_iff.1 (ae_all_iff.2 h_mono))
  let g n a := if a ∈ s then 0 else f n a
  have g_eq_f : ∀ᵐ a ∂μ, ∀ n, g n a = f n a :=
    (measure_eq_zero_iff_ae_notMem.1 hs.2.2).mono fun a ha n => if_neg ha
  calc
    ∫⁻ a, ⨆ n, f n a ∂μ = ∫⁻ a, ⨆ n, g n a ∂μ :=
      lintegral_congr_ae <| g_eq_f.mono fun a ha => by simp only [ha]
    _ = ⨆ n, ∫⁻ a, g n a ∂μ :=
      (lintegral_iSup (fun n => measurable_const.piecewise hs.2.1 (hf n))
        (monotone_nat_of_le_succ fun n a => ?_))
    _ = ⨆ n, ∫⁻ a, f n a ∂μ := by simp only [lintegral_congr_ae (g_eq_f.mono fun _a ha => ha _)]
  simp only [g]
  split_ifs with h
  · rfl
  · have := Set.notMem_subset hs.1 h
    simp only [not_forall, not_le, mem_setOf_eq, not_exists, not_lt] at this
    exact this n
-- 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 : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
⊢ ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
have intro : ∀ (val : Encodable β), ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
Tactic: cases nonempty_encodable β
-- 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 : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
⊢ ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
have intro : IsEmpty β → ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
Tactic: cases isEmpty_or_nonempty β
-- 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 : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
intro : IsEmpty β → ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
⊢ ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
have intro₁ : Nonempty β → ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
Tactic: cases isEmpty_or_nonempty β
-- 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 : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
⊢ ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
have intro : ∀ (inhabited_h : Inhabited β), ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
Tactic: inhabit β
-- 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 : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
a : α
⊢ Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
    (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)
have refine : ∀ (b : β), f b a ≤ ⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a
Tactic: refine le_antisymm (iSup_le fun b => ?_) (iSup_le fun n => le_iSup (fun n => f n a) _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
⊢ ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
have this : ∀ (a : α),
  Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
    (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)
Tactic: have : ∀ a, ⨆ b, f b a = ⨆ n, f (h_directed.sequence f n) a := by
    intro a
    refine le_antisymm (iSup_le fun b => ?_) (iSup_le fun n => le_iSup (fun n => f n a) _)
    exact le_iSup_of_le (encode b + 1) (h_directed.le_sequence b a)
-- 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 : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
      (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)
⊢ Eq (α := ℝ≥0∞)
    (⨆ (n : ℕ), ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ)
    (⨆ (b : β), ∫⁻ (a : α), f b a ∂μ)
have refine_1 : ∀ (n : ℕ),
  ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ ≤
    ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
Tactic: refine le_antisymm (iSup_le fun n => ?_) (iSup_le fun b => ?_)
-- 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 : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
      (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)
refine_1 :
  ∀ (n : ℕ),
    ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ ≤
      ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
⊢ Eq (α := ℝ≥0∞)
    (⨆ (n : ℕ), ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ)
    (⨆ (b : β), ∫⁻ (a : α), f b a ∂μ)
have refine_2 : ∀ (b : β),
  ∫⁻ (a : α), f b a ∂μ ≤
    ⨆ (n : ℕ), ∫⁻ (a : α), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ
Tactic: refine le_antisymm (iSup_le fun n => ?_) (iSup_le fun b => ?_)
-- 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 : ∀ (b : β), Measurable (f b)
h_directed : Directed (fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f
val : Encodable β
h : Nonempty β
inhabited_h : Inhabited β
this :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (⨆ (b : β), f b a)
      (⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a)
⊢ ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ = ⨆ (b : β), ∫⁻ (a : α), f b a ∂μ
have f₁ : ∫⁻ (a : α), ⨆ (b : β), f b a ∂μ =
  ∫⁻ (a : α), ⨆ (n : ℕ), f (Directed.sequence (r := fun (x1 x2 : α → ℝ≥0∞) ↦ x1 ≤ x2) f h_directed n) a ∂μ
Tactic: calc
    ∫⁻ a, ⨆ b, f b a ∂μ = ∫⁻ a, ⨆ n, f (h_directed.sequence f n) a ∂μ := by simp only [this]
    _ = ⨆ n, ∫⁻ a, f (h_directed.sequence f n) a ∂μ :=
      (lintegral_iSup (fun n => hf _) h_directed.sequence_mono)
    _ = ⨆ b, ∫⁻ a, f b a ∂μ := by
      refine le_antisymm (iSup_le fun n => ?_) (iSup_le fun b => ?_)
      · exact le_iSup (fun b => ∫⁻ a, f b a ∂μ) _
      · exact le_iSup_of_le (encode b + 1) (lintegral_mono <| h_directed.le_sequence b)