Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2002P1

import Mathlib

/-!
# International Mathematical Olympiad 2002, Problem 1

Let n be a positive integer. Let T be the set of points (x, y) in the
plane where x and y are non-negative integers and x + y < n. Each
point of T is coloured red or blue, subject to the following
condition: if a point (x, y) is red, then so are all points (x', y')
of T with x' ≤ x and y' ≤ y. Let A be the number of ways of choosing
n blue points with distinct x-coordinates, and let B be the number of
ways of choosing n blue points with distinct y-coordinates. Prove
that A = B.
-/

namespace Imo2002P1

inductive Color : Type where
| red : Color
| blue : Color
deriving DecidableEq, Fintype

/-- The points (x, y) with nonnegative integer coordinates and x + y < n. -/
def T (n : ℕ) : Finset (ℕ × ℕ) :=
  (Finset.range n ×ˢ Finset.range n).filter fun p ↦ p.1 + p.2 < n

/-- The sets of n blue points in T whose coordinates are distinct in
the dimension selected by `coord`. -/
def ChoiceCount (n : ℕ) (color : ℕ × ℕ → Color) (coord : ℕ × ℕ → ℕ) : ℕ :=
  (((T n).powersetCard n).filter fun s ↦
    (∀ p ∈ s, color p = .blue) ∧
    ∀ p ∈ s, ∀ q ∈ s, coord p = coord q → p = q).card

theorem imo2002_p1 (n : ℕ) (_hn : 0 < n) (color : ℕ × ℕ → Color)
    (hcolor : ∀ x' y' x y, x' ≤ x → y' ≤ y → x + y < n →
      color (x, y) = .red → color (x', y') = .red) :
    ChoiceCount n color Prod.fst = ChoiceCount n color Prod.snd := sorry


end Imo2002P1

File author(s): David Renshaw

This problem has a complete formalized solution.