∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T]
  (hJ : J.Nonempty),
  (PairReduction.logSizeBallSeq J hJ a c 0).radius = PairReduction.logSizeRadius (Exists.choose hJ) J a c