∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p : Besicovitch.TauPackage β α)
  (i : Ordinal.{u}), p.iUnionUpTo i = ⋃ j, Metric.ball (p.c (p.index ↑j)) (p.r (p.index ↑j))