Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1984P4

module

public import Mathlib.Algebra.BigOperators.Ring.Finset
public import Mathlib.Algebra.Group.Action.Defs
public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Order.ConditionallyCompleteLattice.Basic
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.NormNum.Ineq
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1984, Problem 4

A maths exam has two papers, each with at least one question and 28 questions
in total. Each pupil attempted 7 questions. Each pair of questions was
attempted by just two pupils. Show that one pupil attempted either nil or at
least 4 questions in the first paper.
-/

namespace Usa1984P4

theorem usa1984_p4 {Pupil : Type} [Fintype Pupil] (attempt : Pupil → Finset (Fin 28))
    (hattempt : ∀ p, (attempt p).card = 7)
    (hpair : ∀ q1 q2 : Fin 28, q1 ≠ q2 →
      (Finset.univ.filter fun p ↦ q1 ∈ attempt p ∧ q2 ∈ attempt p).card = 2)
    (paper1 : Finset (Fin 28)) (hpaper1 : paper1.Nonempty)
    (hpaper2 : (Finset.univ \ paper1).Nonempty) :
    ∃ p, (attempt p ∩ paper1).card = 0 ∨ 4 ≤ (attempt p ∩ paper1).card := sorry

end Usa1984P4

File author(s): Kimi K3

This problem has a complete formalized solution.