-- 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
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
⊢ ∫⁻ (a : α), ⨆ (n : ℕ), f n a ∂μ = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have neg : ∀ (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), f n a ≤ f (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