simp only [forall_true_left, forall_const, Fintype.card_eq_zero, and_self]
case h
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : 0 ≤ 1
⊢ (Finset α → Finset α → Color.blue = Color.blue → Color.blue = Color.blue) ∧
    Fintype.card { a // Color.blue = Color.red } = 0
no goals