import Mathlib.Tactic /-! # International Mathematical Olympiad 2001, Problem 3 Twenty-one girls and twenty-one boys took part in a mathematical competition. It turned out that each contestant solved at most six problems, and for each pair of a girl and a boy, there was at most one problem solved by both the girl and the boy. Show that there was a problem solved by at least three girls and at least three boys. -/ namespace Imo2001P3 theorem imo2001_p3 {Girl Boy Problem : Type} [Finite Girl] [Finite Boy] [Finite Problem] (girl_card : Nat.card Girl = 21) (boy_card : Nat.card Boy = 21) (girl_solved : Girl → Problem → Prop) (boy_solved : Boy → Problem → Prop) (hG : ∀ g : Girl, Nat.card {p | girl_solved g p} ≤ 6) (hB : ∀ b : Boy, Nat.card {p | boy_solved b p} ≤ 6) (hp : ∀ g : Girl, ∀ b : Boy, Nat.card {p | girl_solved g p ∧ boy_solved b p} ≤ 1) : ∃ p : Problem, 3 ≤ Nat.card {g | girl_solved g p} ∧ 3 ≤ Nat.card {g | boy_solved g p} := sorry

This problem does not yet have a complete solution.