∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U : Finset α} {hU : U ∈ P.parts} {s : Finset α},
  s ∈ (SzemerediRegularity.chunk hP G ε hU).parts →
    s.card ≤ Fintype.card α / SzemerediRegularity.stepBound P.parts.card + 1