import Mathlib.Data.Fintype.Card import Mathlib.Data.Finset.Basic import Mathlib.Data.Finset.Card import Mathlib.Data.Finite.Basic import Mathlib.Tactic /-! # USA Mathematical Olympiad 2002, Problem 1 Let S be a set with 2002 elements, and let N be an integer with 0 ≤ N ≤ 2^2002. Prove that it is possible to color every subset of S either blue or red so that the following conditions hold: a) the union of any two red subsets is red; b) the union of any two blue subsets is blue; c) there are exactly N red subsets. -/ namespace Usa2002P1 inductive Color : Type where | red : Color | blue : Color deriving DecidableEq, Fintype theorem usa2002_p1 {α : Type} [DecidableEq α] [Fintype α] (hs : Fintype.card α = 2002) (N : ℕ) (hN : N ≤ 2 ^ 2002) : ∃ f : Finset α → Color, ((∀ s1 s2 : Finset α, f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ (Fintype.card { a : Finset α // f a = Color.red } = N)) := sorry

This problem has a complete solution written by David Renshaw.