α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : IsEquipartition P
ht : t ∈ P.parts
⊢ Finset.card t ≤ (Finset.sum P.parts fun i => Finset.card i) / Finset.card P.parts + 1
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : IsEquipartition P
ht : t ∈ P.parts
⊢ Finset.card t ≤ Finset.card s / Finset.card P.parts + 1
rw [← P.sum_card_parts]
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : IsEquipartition P
ht : t ∈ P.parts
⊢ Finset.card t ≤ (Finset.sum P.parts fun i => Finset.card i) / Finset.card P.parts + 1
exact Finset.EquitableOn.le_add_one hP ht