∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [inst : Fintype ι]
  {π : BoxIntegral.TaggedPrepartition I},
  π.IsSubordinate r → J ∈ π.boxes → Metric.diam (BoxIntegral.Box.Icc J) ≤ 2 * ↑(r (π.tag J))