rw [Nat.pow_zero] at hN
case zero
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : N ≤ 2 ^ 0
⊢ ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
case zero
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : N ≤ 1
⊢ ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N