-- 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.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
k : Set α := ⋃ a ∈ w, B ↑a
k_closed : IsClosed k
d : ℝ
dpos : 0 < d
a : ι
hat : a ∈ t
hz : c a ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
z_notmem_k : c a ∉ k
this : ball x (R x) \ k ∈ 𝓝 (c a)
hd : closedBall (c a) d ⊆ ball x (R x) \ k
ad : r a ≤ d ⊓ R (c a)
ax : B a ⊆ ball x (R x)
b : ι
bu : b ∈ u
ab : (B a ∩ B b).Nonempty
bdiam : r a ≤ 2 * r b
bv : b ∈ v
b' : ↑v := ⟨b, bv⟩
⊢ c a ∈ ⋃ a, closedBall (c ↑↑a) (3 * r ↑↑a)

Tactic:
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]

Result:
case intro.intro.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
k : Set α := ⋃ a ∈ w, B ↑a
k_closed : IsClosed k
d : ℝ
dpos : 0 < d
a : ι
hat : a ∈ t
hz : c a ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
z_notmem_k : c a ∉ k
this : ball x (R x) \ k ∈ 𝓝 (c a)
hd : closedBall (c a) d ⊆ ball x (R x) \ k
ad : r a ≤ d ⊓ R (c a)
ax : B a ⊆ ball x (R x)
b : ι
bu : b ∈ u
ab : (B a ∩ B b).Nonempty
bdiam : r a ≤ 2 * r b
bv : b ∈ v
b' : ↑v := ⟨b, bv⟩
b'_notmem_w : b' ∉ w
⊢ c a ∈ ⋃ a, closedBall (c ↑↑a) (3 * r ↑↑a)

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
M : (s \ ⋃ a ∈ u, B a) ∩ ball x (R x) ⊆ ⋃ a, closedBall (c ↑↑a) (3 * r ↑↑a)
this : Countable ↑v
⊢ μ ((s \ ⋃ a ∈ u, B a) ∩ ball x (R x)) ≤ ε

Tactic:
calc
  μ ((s \ ⋃ a ∈ u, B a) ∩ ball x (R x)) ≤ μ (⋃ a : { a // a ∉ w }, closedBall (c a) (3 * r a)) :=
    measure_mono M
  _ ≤ ∑' a : { a // a ∉ w }, μ (closedBall (c a) (3 * r a)) := measure_iUnion_le _
  _ ≤ ∑' a : { a // a ∉ w }, C * μ (B a) := (ENNReal.tsum_le_tsum fun a => μB a (ut (vu a.1.2)))
  _ = C * ∑' a : { a // a ∉ w }, μ (B a) := ENNReal.tsum_mul_left
  _ ≤ C * (ε / C) := by gcongr
  _ ≤ ε := ENNReal.mul_div_le

Result:
no goals

Proof state:
α : 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 < ε
⊢ ∑' (a : ↑v), μ (B ↑a) < ⊤

Tactic:
calc
  (∑' a : v, μ (B a)) = μ (⋃ a ∈ v, B a) := by
    rw [measure_biUnion (u_count.mono vu) _ fun a ha => (h't _ (vu.trans ut ha)).measurableSet]
    exact u_disj.subset vu
  _ ≤ μ (closedBall x K) := (measure_mono (iUnion₂_subset fun a ha => hK a (vu ha) ha.2))
  _ < ∞ := μK

Result:
no goals