-- Mathlib/MeasureTheory/Covering/Vitali.lean
theorem exists_disjoint_covering_ae
    [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α]
    [SecondCountableTopology α] (μ : Measure α) [IsLocallyFiniteMeasure μ] (s : Set α) (t : Set ι)
    (C : ℝ≥0) (r : ι → ℝ) (c : ι → α) (B : ι → Set α) (hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a))
    (μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ C * μ (B a))
    (ht : ∀ a ∈ t, (interior (B a)).Nonempty) (h't : ∀ a ∈ t, IsClosed (B a))
    (hf : ∀ x ∈ s, ∀ ε > (0 : ℝ), ∃ a ∈ t, r a ≤ ε ∧ c a = x) :
    ∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ⊤
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
x✝ : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : μ (closedBall x K) < ⊤
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : ∑' (a : ↑v), μ (B ↑a) < ⊤
w : Finset ↑v
hw : ∑' (a : { a // a ∉ w }), μ (B ↑↑a) < ε / ↑C
⊢ μ ((s \ ⋃ a ∈ u, B a) ∩ ball x (R x)) ≤ ε

Tactic:
have M : (s \ ⋃ a ∈ u, B a) ∩
    ball x (R x) ⊆ ⋃ a : { a // a ∉ w }, closedBall (c a) (3 * r a) := by
  intro z hz
  set k := ⋃ (a : v) (_ : a ∈ w), B a
  have k_closed : IsClosed k := isClosed_biUnion_finset fun i _ => h't _ (ut (vu i.2))
  have z_notmem_k : z ∉ k := by
    simp only [k, not_exists, exists_prop, mem_iUnion, mem_sep_iff, forall_exists_index,
      SetCoe.exists, not_and, exists_and_right, Subtype.coe_mk]
    intro b hbv _ h'z
    have : z ∈ (s \ ⋃ a ∈ u, B a) ∩ ⋃ a ∈ u, B a :=
      mem_inter (mem_of_mem_inter_left hz) (mem_biUnion (vu hbv) h'z)
    simpa only [diff_inter_self]
  have : ball x (R x) \ k ∈ 𝓝 z := by
    apply IsOpen.mem_nhds (isOpen_ball.sdiff k_closed) _
    exact (mem_diff _).2 ⟨mem_of_mem_inter_right hz, z_notmem_k⟩
  obtain ⟨d, dpos, hd⟩ : ∃ d, 0 < d ∧ closedBall z d ⊆ ball x (R x) \ k :=
    nhds_basis_closedBall.mem_iff.1 this
  obtain ⟨a, hat, ad, rfl⟩ : ∃ a ∈ t, r a ≤ min d (R z) ∧ c a = z :=
    hf z ((mem_diff _).1 (mem_of_mem_inter_left hz)).1 (min d (R z)) (lt_min dpos (hR0 z))
  have ax : B a ⊆ ball x (R x) := by
    refine (hB a hat).trans ?_
    refine Subset.trans ?_ (hd.trans Set.diff_subset)
    exact closedBall_subset_closedBall (ad.trans (min_le_left _ _))
  obtain ⟨b, bu, ab, bdiam⟩ : ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b :=
    hu a ⟨hat, ad.trans (min_le_right _ _)⟩
  have bv : b ∈ v := by
    refine ⟨bu, ab.mono ?_⟩
    rw [inter_comm]
    exact inter_subset_inter_right _ ax
  let b' : v := ⟨b, bv⟩
  have b'_notmem_w : b' ∉ w := by
    intro b'w
    have b'k : B b' ⊆ k := @Finset.subset_set_biUnion_of_mem _ _ _ (fun y : v => B y) _ b'w
    have : (ball x (R x) \ k ∩ k).Nonempty := by
      apply ab.mono (inter_subset_inter _ b'k)
      refine ((hB _ hat).trans ?_).trans hd
      exact closedBall_subset_closedBall (ad.trans (min_le_left _ _))
    simpa only [diff_inter_self, Set.not_nonempty_empty]
  let b'' : { a // a ∉ w } := ⟨b', b'_notmem_w⟩
  have zb : c a ∈ closedBall (c b) (3 * r b) := by
    rcases ab with ⟨e, ⟨ea, eb⟩⟩
    have A : dist (c a) e ≤ r a := mem_closedBall'.1 (hB a hat ea)
    have B : dist e (c b) ≤ r b := mem_closedBall.1 (hB b (ut bu) eb)
    simp only [mem_closedBall]
    linarith only [dist_triangle (c a) e (c b), A, B, bdiam]
  suffices H : closedBall (c b'') (3 * r b'')
      ⊆ ⋃ a : { a // a ∉ w }, closedBall (c a) (3 * r a) from H zb
  exact subset_iUnion (fun a : { a // a ∉ w } => closedBall (c a) (3 * r a)) b''

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ⊤
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
x✝ : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : μ (closedBall x K) < ⊤
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : ∑' (a : ↑v), μ (B ↑a) < ⊤
w : Finset ↑v
hw : ∑' (a : { a // a ∉ w }), μ (B ↑↑a) < ε / ↑C
M : (s \ ⋃ a ∈ u, B a) ∩ ball x (R x) ⊆ ⋃ a, closedBall (c ↑↑a) (3 * r ↑↑a)
⊢ μ ((s \ ⋃ a ∈ u, B a) ∩ ball x (R x)) ≤ ε