-- Mathlib/MeasureTheory/Covering/Besicovitch.lean
theorem color_lt {i : Ordinal.{u}} (hi : i < p.lastStep) {N : ℕ}
    (hN : IsEmpty (SatelliteConfig α N p.τ)) : p.color i < N

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ k < i, k < p.lastStep → p.color k < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n => if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
n : ℕ
hn : n ≤ N
⊢ p.index (G n) = Classical.epsilon fun t => p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t

Tactic:
rw [index]

Result:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ k < i, k < p.lastStep → p.color k < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n => if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
n : ℕ
hn : n ≤ N
⊢ (Classical.epsilon fun b => p.c b ∉ ⋃ j, ball (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∧ ⨆ b, p.r ↑b ≤ p.τ * p.r b) =
    Classical.epsilon fun t => p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t

Proof state:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ k < i, k < p.lastStep → p.color k < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n => if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
Gab :
  ∀ (a b : Fin N.succ),
    G ↑a < G ↑b →
      p.r (p.index (G ↑a)) ≤ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑b))) ∧
        p.r (p.index (G ↑b)) ≤ p.τ * p.r (p.index (G ↑a))
a b : Fin N.succ
a_ne_b : a ≠ b
⊢ (fun k => p.r (p.index (G ↑k))) a ≤ dist ((fun k => p.c (p.index (G ↑k))) a) ((fun k => p.c (p.index (G ↑k))) b) ∧
      (fun k => p.r (p.index (G ↑k))) b ≤ p.τ * (fun k => p.r (p.index (G ↑k))) a ∨
    (fun k => p.r (p.index (G ↑k))) b ≤ dist ((fun k => p.c (p.index (G ↑k))) b) ((fun k => p.c (p.index (G ↑k))) a) ∧
      (fun k => p.r (p.index (G ↑k))) a ≤ p.τ * (fun k => p.r (p.index (G ↑k))) b

Tactic:
wlog G_le : G a ≤ G b generalizing a b

Result:
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ k < i, k < p.lastStep → p.color k < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n => if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
Gab :
  ∀ (a b : Fin N.succ),
    G ↑a < G ↑b →
      p.r (p.index (G ↑a)) ≤ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑b))) ∧
        p.r (p.index (G ↑b)) ≤ p.τ * p.r (p.index (G ↑a))
a b : Fin N.succ
a_ne_b : a ≠ b
this :
  ∀ ⦃a b : Fin N.succ⦄,
    a ≠ b →
      G ↑a ≤ G ↑b →
        (fun k => p.r (p.index (G ↑k))) a ≤
              dist ((fun k => p.c (p.index (G ↑k))) a) ((fun k => p.c (p.index (G ↑k))) b) ∧
            (fun k => p.r (p.index (G ↑k))) b ≤ p.τ * (fun k => p.r (p.index (G ↑k))) a ∨
          (fun k => p.r (p.index (G ↑k))) b ≤
              dist ((fun k => p.c (p.index (G ↑k))) b) ((fun k => p.c (p.index (G ↑k))) a) ∧
            (fun k => p.r (p.index (G ↑k))) a ≤ p.τ * (fun k => p.r (p.index (G ↑k))) b
G_le : ¬G ↑a ≤ G ↑b
⊢ (fun k => p.r (p.index (G ↑k))) a ≤ dist ((fun k => p.c (p.index (G ↑k))) a) ((fun k => p.c (p.index (G ↑k))) b) ∧
      (fun k => p.r (p.index (G ↑k))) b ≤ p.τ * (fun k => p.r (p.index (G ↑k))) a ∨
    (fun k => p.r (p.index (G ↑k))) b ≤ dist ((fun k => p.c (p.index (G ↑k))) b) ((fun k => p.c (p.index (G ↑k))) a) ∧
      (fun k => p.r (p.index (G ↑k))) a ≤ p.τ * (fun k => p.r (p.index (G ↑k))) b

α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ k < i, k < p.lastStep → p.color k < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n => if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
Gab :
  ∀ (a b : Fin N.succ),
    G ↑a < G ↑b →
      p.r (p.index (G ↑a)) ≤ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑b))) ∧
        p.r (p.index (G ↑b)) ≤ p.τ * p.r (p.index (G ↑a))
a b : Fin N.succ
a_ne_b : a ≠ b
G_le : G ↑a ≤ G ↑b
⊢ (fun k => p.r (p.index (G ↑k))) a ≤ dist ((fun k => p.c (p.index (G ↑k))) a) ((fun k => p.c (p.index (G ↑k))) b) ∧
      (fun k => p.r (p.index (G ↑k))) b ≤ p.τ * (fun k => p.r (p.index (G ↑k))) a ∨
    (fun k => p.r (p.index (G ↑k))) b ≤ dist ((fun k => p.c (p.index (G ↑k))) b) ((fun k => p.c (p.index (G ↑k))) a) ∧
      (fun k => p.r (p.index (G ↑k))) a ≤ p.τ * (fun k => p.r (p.index (G ↑k))) b