-- 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 hs
α : 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
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index jy)) (p.r (p.index jy))).Nonempty),
      {p.color ↑j}
color_j : p.color jy = sInf (univ \ A)
k : Ordinal.{u}
hk : k < jy
a✝ : (closedBall (p.c (p.index k)) (p.r (p.index k)) ∩ closedBall (p.c (p.index jy)) (p.r (p.index jy))).Nonempty
⊢ ¬N = p.color k

Tactic:
exact (p.color_lt (hk.trans jy_lt) hN).ne'

Result:
no goals

Proof state:
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)

Tactic:
exact (this jy jy_lt jyi hy jx jx_lt jxi hx x_ne_y.symm (le_of_not_le jxy)).symm

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : IsEmpty β
⊢ q.c '' ∅ ⊆ ⋃ i, ⋃ j ∈ (fun x => ∅) i, ball (q.c j) (q.r j)

Tactic:
simp

Result:
no goals

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
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
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index jy)) (p.r (p.index jy))).Nonempty),
      {p.color ↑j}
color_j : p.color jy = sInf (univ \ A)
⊢ Function.onFun Disjoint (fun j => closedBall (q.c j) (q.r j)) (p.index jx) (p.index jy)

Tactic:
have h : p.color jy ∈ univ \ A := by
  rw [color_j]
  apply csInf_mem
  refine ⟨N, ?_⟩
  simp only [A, not_exists, true_and, exists_prop, mem_iUnion, mem_singleton_iff, not_and,
    mem_univ, mem_diff, Subtype.exists, Subtype.coe_mk]
  intro k hk _
  exact (p.color_lt (hk.trans jy_lt) hN).ne'

Result:
α : 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
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index jy)) (p.r (p.index jy))).Nonempty),
      {p.color ↑j}
color_j : p.color jy = sInf (univ \ A)
h : p.color jy ∈ univ \ A
⊢ 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
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
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index jy)) (p.r (p.index jy))).Nonempty),
      {p.color ↑j}
color_j : p.color jy = sInf (univ \ A)
⊢ sInf (univ \ A) ∈ univ \ A

Tactic:
apply csInf_mem

Result:
case hs
α : 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
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index jy)) (p.r (p.index jy))).Nonempty),
      {p.color ↑j}
color_j : p.color jy = sInf (univ \ A)
⊢ (univ \ A).Nonempty

Proof state:
case inl
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : IsEmpty β
⊢ range q.c ⊆ ⋃ i, ⋃ j ∈ (fun x => ∅) i, ball (q.c j) (q.r j)

Tactic:
rw [← image_univ, eq_empty_of_isEmpty (univ : Set β)]

Result:
case inl
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : IsEmpty β
⊢ q.c '' ∅ ⊆ ⋃ i, ⋃ j ∈ (fun x => ∅) i, ball (q.c j) (q.r j)