-- Mathlib/MeasureTheory/Covering/Besicovitch.lean
theorem exist_finset_disjoint_balls_large_measure (μ : Measure α) [IsFiniteMeasure μ] {N : ℕ}
    {τ : ℝ} (hτ : 1 < τ) (hN : IsEmpty (SatelliteConfig α N τ)) (s : Set α) (r : α → ℝ)
    (rpos : ∀ x ∈ s, 0 < r x) (rle : ∀ x ∈ s, r x ≤ 1) :
    ∃ t : Finset α, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ N / (N + 1) * μ s ∧
      (t : Set α).PairwiseDisjoint fun x => closedBall x (r x)

Proof state:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : 0 < μ s
h✝ : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : μ o = μ s
a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
u : Fin N → Set ↑s
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j => closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun i => ⋃ x ∈ u i, closedBall (↑x) (r ↑x)
A : s = ⋃ i, s ∩ v i
S : ∑ _i : Fin N, μ s / ↑N ≤ ∑ i : Fin N, μ (s ∩ v i)
i : Fin N
hi : μ s / (↑N + 1) < μ (s ∩ v i)
B : μ (o ∩ v i) = ∑' (x : ↑(u i)), μ (o ∩ closedBall (↑↑x) (r ↑↑x))
w : Finset ↑(u i)
hw : μ s / (↑N + 1) < ∑ x ∈ w, μ (o ∩ closedBall (↑↑x) (r ↑↑x))
y : ↑(u i)
a✝ : y ∈ ↑w
⊢ y ∈ (fun x => ↑↑x) ⁻¹' s

Tactic:
simp only [Subtype.coe_prop, mem_preimage]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : μ s ≤ 0
this : μ s = 0
⊢ ∃ t,
    ↑t ⊆ s ∧
      μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)

Tactic:
refine ⟨∅, by simp only [Finset.coe_empty, empty_subset], ?_, ?_⟩

Result:
case inl.refine_1
α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : μ s ≤ 0
this : μ s = 0
⊢ μ (s \ ⋃ x ∈ ∅, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s

case inl.refine_2
α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : μ s ≤ 0
this : μ s = 0
⊢ (↑∅).PairwiseDisjoint fun x => closedBall x (r x)

Proof state:
α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : 0 < μ s
h✝ : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : μ o = μ s
a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
u : Fin N → Set ↑s
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j => closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun i => ⋃ x ∈ u i, closedBall (↑x) (r ↑x)
A : s = ⋃ i, s ∩ v i
S : ∑ _i : Fin N, μ s / ↑N ≤ ∑ i : Fin N, μ (s ∩ v i)
i : Fin N
hi : μ s / (↑N + 1) < μ (s ∩ v i)
B : μ (o ∩ v i) = ∑' (x : ↑(u i)), μ (o ∩ closedBall (↑↑x) (r ↑↑x))
w : Finset ↑(u i)
hw : μ s / (↑N + 1) < ∑ x ∈ w, μ (o ∩ closedBall (↑↑x) (r ↑↑x))
⊢ ∑ x ∈ w, μ (o ∩ closedBall (↑↑x) (r ↑↑x)) = μ ((⋃ x ∈ w, closedBall (↑↑x) (r ↑↑x)) ∩ o)

Tactic:
rw [← Finset.set_biUnion_coe, inter_comm _ o, inter_iUnion₂, Finset.set_biUnion_coe,
  measure_biUnion_finset]

Result:
case hd
α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : 0 < μ s
h✝ : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : μ o = μ s
a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
u : Fin N → Set ↑s
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j => closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun i => ⋃ x ∈ u i, closedBall (↑x) (r ↑x)
A : s = ⋃ i, s ∩ v i
S : ∑ _i : Fin N, μ s / ↑N ≤ ∑ i : Fin N, μ (s ∩ v i)
i : Fin N
hi : μ s / (↑N + 1) < μ (s ∩ v i)
B : μ (o ∩ v i) = ∑' (x : ↑(u i)), μ (o ∩ closedBall (↑↑x) (r ↑↑x))
w : Finset ↑(u i)
hw : μ s / (↑N + 1) < ∑ x ∈ w, μ (o ∩ closedBall (↑↑x) (r ↑↑x))
⊢ (↑w).PairwiseDisjoint fun x => o ∩ closedBall (↑↑x) (r ↑↑x)

case hm
α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : 0 < μ s
h✝ : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : μ o = μ s
a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
u : Fin N → Set ↑s
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j => closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun i => ⋃ x ∈ u i, closedBall (↑x) (r ↑x)
A : s = ⋃ i, s ∩ v i
S : ∑ _i : Fin N, μ s / ↑N ≤ ∑ i : Fin N, μ (s ∩ v i)
i : Fin N
hi : μ s / (↑N + 1) < μ (s ∩ v i)
B : μ (o ∩ v i) = ∑' (x : ↑(u i)), μ (o ∩ closedBall (↑↑x) (r ↑↑x))
w : Finset ↑(u i)
hw : μ s / (↑N + 1) < ∑ x ∈ w, μ (o ∩ closedBall (↑↑x) (r ↑↑x))
⊢ ∀ b ∈ w, MeasurableSet (o ∩ closedBall (↑↑b) (r ↑↑b))

Proof state:
α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : 0 < μ s
h✝ : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : μ o = μ s
a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
u : Fin N → Set ↑s
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j => closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun i => ⋃ x ∈ u i, closedBall (↑x) (r ↑x)
A : s = ⋃ i, s ∩ v i
S : ∑ _i : Fin N, μ s / ↑N ≤ ∑ i : Fin N, μ (s ∩ v i)
i : Fin N
hi : μ s / (↑N + 1) < μ (s ∩ v i)
B : μ (o ∩ v i) = ∑' (x : ↑(u i)), μ (o ∩ closedBall (↑↑x) (r ↑↑x))
w : Finset ↑(u i)
hw : μ s / (↑N + 1) < ∑ x ∈ w, μ (o ∩ closedBall (↑↑x) (r ↑↑x))
k : α
hk : k ∈ ↑(Finset.image (fun x => ↑↑x) w)
l : α
hl : l ∈ ↑(Finset.image (fun x => ↑↑x) w)
hkl : k ≠ l
⊢ ∃ k' ∈ w, ↑↑k' = k

Tactic:
simpa only [mem_image, Finset.mem_coe, Finset.coe_image] using hk

Result:
no goals