-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
      ε / 2
g : (n : ℕ) → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)
f₁ :
  ENNReal.toReal
      ((μ : (a : Set X) → ℝ≥0∞)
        (((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n) ∪
          (⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) ≤
    ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) +
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n))
⊢ μ.real ((⋃ (i : ℕ), f i) ∆ ⋃ n ∈ Finset.range (N + 1), g n) < ε
have f₂ : ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) +
    ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) <
  ε
Tactic: calc
          μ.real ((⋃ n, f n) ∆ (⋃ n ∈ (Finset.range (N + 1)), g n))
            ≤ (μ ((⋃ n, f n) \ ((⋃ n ∈ (Finset.range (N + 1)), f n)) ∪
              ((⋃ n ∈ (Finset.range (N + 1)), f n) ∆
              (⋃ n ∈ (Finset.range (N + 1)), g ↑n)))).toReal :=
                toReal_mono (measure_ne_top _ _)
                  (measure_mono <| symmDiff_of_ge (iUnion_subset <|
                  fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i)) ▸ symmDiff_triangle ..)
          _ ≤ (μ ((⋃ n, f n) \
              ((⋃ n ∈ (Finset.range (N + 1)), f n)))).toReal +
              (μ ((⋃ n ∈ (Finset.range (N + 1)), f n) ∆
              (⋃ n ∈ (Finset.range (N + 1)), g ↑n))).toReal := by
                rw [← toReal_add (measure_ne_top _ _) (measure_ne_top _ _)]
                exact toReal_mono (add_ne_top.2 ⟨measure_ne_top _ _, measure_ne_top _ _⟩) <|
                  measure_union_le _ _
          _ < ε := by
                rw [← add_halves ε]
                apply _root_.add_lt_add
                · rw [measure_diff (h_fin := measure_ne_top _ _),
                    toReal_sub_of_le (ha := measure_ne_top _ _)]
                  · apply lt_of_le_of_lt (sub_le_dist ..)
                    simp only [Finset.mem_range, Nat.lt_add_one_iff]
                    exact (dist_comm (α := ℝ) .. ▸ hN N (le_refl N))
                  · exact measure_mono <| iUnion_subset <|
                      fun i ↦ iUnion_subset fun _ ↦ subset_iUnion f i
                  · exact iUnion_subset <| fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i)
                  · exact MeasurableSet.biUnion (countable_coe_iff.1 inferInstance)
                      (fun n _ ↦ (hf n).1.nullMeasurableSet)
                · calc
                    (μ ((⋃ n ∈ (Finset.range (N + 1)), f n) ∆
                    (⋃ n ∈ (Finset.range (N + 1)), g ↑n))).toReal
                      ≤ μ.real (⋃ n ∈ (Finset.range (N + 1)), f n ∆ g n) :=
                          toReal_mono (measure_ne_top _ _) (measure_mono biSup_symmDiff_biSup_le)
                    _ ≤ ∑ n ∈ Finset.range (N + 1), μ.real (f n ∆ g n) := by
                          simp_rw [measureReal_def, ← toReal_sum (fun _ _ ↦ measure_ne_top _ _)]
                          exact toReal_mono (ne_of_lt <| sum_lt_top.2 fun _ _ ↦ measure_lt_top μ _)
                            (measure_biUnion_finset_le _ _)
                    _ < ∑ n ∈ Finset.range (N + 1), (ε / (2 * (N + 1))) :=
                          Finset.sum_lt_sum (fun i _ ↦ le_of_lt (hg i)) ⟨0, by simp, hg 0⟩
                    _ ≤ ε / 2 := by
                          simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul,
                            Nat.cast_add, Nat.cast_one]
                          rw [div_mul_eq_div_mul_one_div, ← mul_assoc, mul_comm ((N : ℝ) + 1),
                            mul_assoc]
                          exact mul_le_of_le_one_right (by linarith [ε_pos]) <|
                            le_of_eq <| mul_one_div_cancel <| Nat.cast_add_one_ne_zero _