no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
⊢ IsEquipartition P ↔
    ∀ (a : Finset α),
      a ∈ P.parts →
        Finset.card a = Finset.card s / Finset.card P.parts ∨ Finset.card a = Finset.card s / Finset.card P.parts + 1
simp_rw [IsEquipartition, Finset.equitableOn_iff, P.sum_card_parts]