revert N α
α : Type
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hs : Fintype.card α = n
N : ℕ
hN : N ≤ 2 ^ n
⊢ ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
n : ℕ
⊢ ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = n →
      ∀ N ≤ 2 ^ n,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N