interval_cases 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
case zero.«0»
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : 0 ≤ 1
⊢ ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = 0

case zero.«1»
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : 1 ≤ 1
⊢ ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = 1