module
public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Fin.VecNotation
public section
/-!
# USA Mathematical Olympiad 1976, Problem 1
The squares of a 4 x 7 chess board are colored red or blue. Show that however
the coloring is done, we can find a rectangle with four distinct corner
squares all the same color. Find a counter-example to show that this is not
true for a 4 x 6 board.
-/
namespace Usa1976P1
/-- A coloring (true = red, false = blue) of an `m × n` board has a
monochromatic rectangle if there are two distinct rows and two distinct
columns whose four intersection squares all have the same color. -/
def HasMonoRectangle {m n : ℕ} (c : Fin m → Fin n → Bool) : Prop :=
∃ r1 r2 : Fin m, ∃ j1 j2 : Fin n, ∃ b : Bool,
r1 ≠ r2 ∧ j1 ≠ j2 ∧
c r1 j1 = b ∧ c r2 j1 = b ∧ c r1 j2 = b ∧ c r2 j2 = b
/-- A 4 x 6 coloring with no monochromatic rectangle. Written row by row,
with `true` = red:
```
R B R B R B
R B B R B R
B R R B B R
B R B R R B
```
Every column has two red and two blue squares, and no two columns have their
red squares in the same two rows or their blue squares in the same two rows,
so there can be no monochromatic rectangle. -/
/- determine -/ abbrev counterexample : Fin 4 → Fin 6 → Bool := sorry
theorem usa1976_p1_first (c : Fin 4 → Fin 7 → Bool) : HasMonoRectangle c := sorry
theorem usa1976_p1_second : ¬ HasMonoRectangle counterexample := sorry
end Usa1976P1
This problem has a complete formalized solution.