∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U V : Finset α} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 →
      ε ≤ 1 →
        ∀ (hU : U ∈ P.parts),
          V ∈ P.parts →
            U ≠ V → ¬G.IsUniform ε U V → 4 / 5 * ε ≤ ↑(SzemerediRegularity.star hP G ε hU V).card / 4 ^ P.parts.card