α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hn : 0 < n
hs : n ≤ card s
⊢ ∃ P, IsEquipartition P ∧ card P.parts = n
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hn : n ≠ 0
hs : n ≤ card s
⊢ ∃ P, IsEquipartition P ∧ card P.parts = n
rw [← pos_iff_ne_zero] at hn
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hn : 0 < n
hs : n ≤ card s
this : (n - card s % n) * (card s / n) + card s % n * (card s / n + 1) = card s
⊢ ∃ P, IsEquipartition P ∧ card P.parts = n
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hn : 0 < n
hs : n ≤ card s
⊢ ∃ P, IsEquipartition P ∧ card P.parts = n
have : (n - s.card % n) * (s.card / n) + s.card % n * (s.card / n + 1) = s.card := by
  rw [tsub_mul, mul_add, ← add_assoc,
    tsub_add_cancel_of_le (Nat.mul_le_mul_right _ (mod_lt _ hn).le), mul_one, add_comm,
    mod_add_div]
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hn : 0 < n
hs : n ≤ card s
this : (n - card s % n) * (card s / n) + card s % n * (card s / n + 1) = card s
⊢ card (equitabilise this).parts = n
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hn : 0 < n
hs : n ≤ card s
this : (n - card s % n) * (card s / n) + card s % n * (card s / n + 1) = card s
⊢ ∃ P, IsEquipartition P ∧ card P.parts = n
refine'
  ⟨(indiscrete (card_pos.1 <| hn.trans_le hs).ne_empty).equitabilise this,
    equitabilise_isEquipartition, _⟩
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hn : 0 < n
hs : n ≤ card s
this : (n - card s % n) * (card s / n) + card s % n * (card s / n + 1) = card s
⊢ card (equitabilise this).parts = n
rw [card_parts_equitabilise _ _ (Nat.div_pos hs hn).ne', tsub_add_cancel_of_le (mod_lt _ hn).le]
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
m n a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = card s
hn : 0 < n
hs : n ≤ card s
⊢ (n - card s % n) * (card s / n) + card s % n * (card s / n + 1) = card s
rw [tsub_mul, mul_add, ← add_assoc,
  tsub_add_cancel_of_le (Nat.mul_le_mul_right _ (mod_lt _ hn).le), mul_one, add_comm,
  mod_add_div]