[GOAL]
α : 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
[PROOFSTEP]
simp_rw [IsEquipartition, Finset.equitableOn_iff, P.sum_card_parts]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : IsEquipartition P
ht : t ∈ P.parts
⊢ Finset.card s / Finset.card P.parts ≤ Finset.card t
[PROOFSTEP]
rw [← P.sum_card_parts]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : IsEquipartition P
ht : t ∈ P.parts
⊢ (Finset.sum P.parts fun i => Finset.card i) / Finset.card P.parts ≤ Finset.card t
[PROOFSTEP]
exact Finset.EquitableOn.le hP ht
[GOAL]
α : 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
[PROOFSTEP]
rw [← P.sum_card_parts]
[GOAL]
α : 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
[PROOFSTEP]
exact Finset.EquitableOn.le_add_one hP ht
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
⊢ ∀ (a : Finset α), a ∈ ↑⊥.parts → Finset.card a = 1 ∨ Finset.card a = 1 + 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hs : s ≠ ∅
⊢ IsEquipartition (indiscrete hs)
[PROOFSTEP]
rw [IsEquipartition, indiscrete_parts, coe_singleton]
[GOAL]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hs : s ≠ ∅
⊢ Set.EquitableOn {s} Finset.card
[PROOFSTEP]
exact Set.equitableOn_singleton s _
