∀ {α : Type u_1} {inst : MetricSpace α} {N : ℕ} {τ : ℝ} {c : Fin N.succ → α} {r : Fin N.succ → ℝ}
  {rpos : ∀ (i : Fin N.succ), 0 < r i}
  {h : Pairwise fun i j => r i ≤ dist (c i) (c j) ∧ r j ≤ τ * r i ∨ r j ≤ dist (c j) (c i) ∧ r i ≤ τ * r j}
  {hlast : ∀ i < Fin.last N, r i ≤ dist (c i) (c (Fin.last N)) ∧ r (Fin.last N) ≤ τ * r i}
  {inter : ∀ i < Fin.last N, dist (c i) (c (Fin.last N)) ≤ r i + r (Fin.last N)} {c_1 : Fin N.succ → α}
  {r_1 : Fin N.succ → ℝ} {rpos_1 : ∀ (i : Fin N.succ), 0 < r_1 i}
  {h_1 :
    Pairwise fun i j =>
      r_1 i ≤ dist (c_1 i) (c_1 j) ∧ r_1 j ≤ τ * r_1 i ∨ r_1 j ≤ dist (c_1 j) (c_1 i) ∧ r_1 i ≤ τ * r_1 j}
  {hlast_1 : ∀ i < Fin.last N, r_1 i ≤ dist (c_1 i) (c_1 (Fin.last N)) ∧ r_1 (Fin.last N) ≤ τ * r_1 i}
  {inter_1 : ∀ i < Fin.last N, dist (c_1 i) (c_1 (Fin.last N)) ≤ r_1 i + r_1 (Fin.last N)},
  { c := c, r := r, rpos := rpos, h := h, hlast := hlast, inter := inter } =
      { c := c_1, r := r_1, rpos := rpos_1, h := h_1, hlast := hlast_1, inter := inter_1 } →
    c = c_1 ∧ r = r_1