-- Mathlib/MeasureTheory/Covering/Besicovitch.lean
theorem exist_disjoint_covering_families {N : ℕ} {τ : ℝ} (hτ : 1 < τ)
    (hN : IsEmpty (SatelliteConfig α N τ)) (q : BallPackage β α) :
    ∃ s : Fin N → Set β,
      (∀ i : Fin N, (s i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)) ∧
        range q.c ⊆ ⋃ i : Fin N, ⋃ j ∈ s i, ball (q.c j) (q.r j)

Proof state:
case inr.refine_2.intro
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i => ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
b : β
a : Ordinal.{u}
ha : a < p.lastStep ∧ dist (p.c b) (p.c (p.index a)) < p.r (p.index a)
⊢ q.c b ∈ ⋃ i, ⋃ j ∈ s i, ball (q.c j) (q.r j)

Tactic:
simp only [s, exists_prop, mem_iUnion, mem_ball, mem_singleton_iff, biUnion_and',
  exists_eq_left, iUnion_exists, exists_and_left]

Result:
case inr.refine_2.intro
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i => ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
b : β
a : Ordinal.{u}
ha : a < p.lastStep ∧ dist (p.c b) (p.c (p.index a)) < p.r (p.index a)
⊢ ∃ i i_1, p.color i_1 = ↑i ∧ i_1 < p.lastStep ∧ dist (q.c b) (q.c (p.index i_1)) < q.r (p.index i_1)

Proof state:
case inr.refine_1.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i => ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
i : Fin N
jx : Ordinal.{u}
jx_lt : jx < p.lastStep
jxi : p.color jx = ↑i
hx : p.index jx ∈ s i
jy : Ordinal.{u}
jy_lt : jy < p.lastStep
jyi : p.color jy = ↑i
hy : p.index jy ∈ s i
x_ne_y : p.index jx ≠ p.index jy
⊢ Function.onFun Disjoint (fun j => closedBall (q.c j) (q.r j)) (p.index jx) (p.index jy)

Tactic:
wlog jxy : jx ≤ jy generalizing jx jy

Result:
case inr.refine_1.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i => ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
i : Fin N
jx : Ordinal.{u}
jx_lt : jx < p.lastStep
jxi : p.color jx = ↑i
hx : p.index jx ∈ s i
jy : Ordinal.{u}
jy_lt : jy < p.lastStep
jyi : p.color jy = ↑i
hy : p.index jy ∈ s i
x_ne_y : p.index jx ≠ p.index jy
this :
  ∀ jx < p.lastStep,
    p.color jx = ↑i →
      p.index jx ∈ s i →
        ∀ jy < p.lastStep,
          p.color jy = ↑i →
            p.index jy ∈ s i →
              p.index jx ≠ p.index jy →
                jx ≤ jy → Function.onFun Disjoint (fun j => closedBall (q.c j) (q.r j)) (p.index jx) (p.index jy)
jxy : ¬jx ≤ jy
⊢ Function.onFun Disjoint (fun j => closedBall (q.c j) (q.r j)) (p.index jx) (p.index jy)

α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i => ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
i : Fin N
jx : Ordinal.{u}
jx_lt : jx < p.lastStep
jxi : p.color jx = ↑i
hx : p.index jx ∈ s i
jy : Ordinal.{u}
jy_lt : jy < p.lastStep
jyi : p.color jy = ↑i
hy : p.index jy ∈ s i
x_ne_y : p.index jx ≠ p.index jy
jxy : jx ≤ jy
⊢ Function.onFun Disjoint (fun j => closedBall (q.c j) (q.r j)) (p.index jx) (p.index jy)

Proof state:
case inr.refine_1.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i => ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
i : Fin N
y : β
hy : y ∈ s i
jx : Ordinal.{u}
jx_lt : jx < p.lastStep
jxi : p.color jx = ↑i
hx : p.index jx ∈ s i
x_ne_y : p.index jx ≠ y
⊢ Function.onFun Disjoint (fun j => closedBall (q.c j) (q.r j)) (p.index jx) y

Tactic:
obtain ⟨jy, jy_lt, jyi, rfl⟩ :
  ∃ jy : Ordinal, jy < p.lastStep ∧ p.color jy = i ∧ y = p.index jy := by
  simpa only [s, exists_prop, mem_iUnion, mem_singleton_iff] using hy

Result:
case inr.refine_1.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i => ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
i : Fin N
jx : Ordinal.{u}
jx_lt : jx < p.lastStep
jxi : p.color jx = ↑i
hx : p.index jx ∈ s i
jy : Ordinal.{u}
jy_lt : jy < p.lastStep
jyi : p.color jy = ↑i
hy : p.index jy ∈ s i
x_ne_y : p.index jx ≠ p.index jy
⊢ Function.onFun Disjoint (fun j => closedBall (q.c j) (q.r j)) (p.index jx) (p.index jy)

Proof state:
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i => ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
i : Fin N
x : β
hx : x ∈ s i
y : β
hy : y ∈ s i
x_ne_y : x ≠ y
⊢ ∃ jx < p.lastStep, p.color jx = ↑i ∧ x = p.index jx

Tactic:
simpa only [s, exists_prop, mem_iUnion, mem_singleton_iff] using hx

Result:
no goals

Proof state:
case inr.refine_2.intro
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i => ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
b : β
a : Ordinal.{u}
ha : a < p.lastStep ∧ dist (p.c b) (p.c (p.index a)) < p.r (p.index a)
⊢ ∃ i i_1, p.color i_1 = ↑i ∧ i_1 < p.lastStep ∧ dist (q.c b) (q.c (p.index i_1)) < q.r (p.index i_1)

Tactic:
exact ⟨⟨p.color a, p.color_lt ha.1 hN⟩, a, rfl, ha⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
⊢ ∃ s,
    (∀ (i : Fin N), (s i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)) ∧
      range q.c ⊆ ⋃ i, ⋃ j ∈ s i, ball (q.c j) (q.r j)

Tactic:
cases isEmpty_or_nonempty β

Result:
case inl
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : IsEmpty β
⊢ ∃ s,
    (∀ (i : Fin N), (s i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)) ∧
      range q.c ⊆ ⋃ i, ⋃ j ∈ s i, ball (q.c j) (q.r j)

case inr
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
⊢ ∃ s,
    (∀ (i : Fin N), (s i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)) ∧
      range q.c ⊆ ⋃ i, ⋃ j ∈ s i, ball (q.c j) (q.r j)