Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2017P5

module

public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.Finset.Fin
public import Mathlib.Data.Nat.SuccPred
public import Mathlib.Data.ZMod.Defs
public import Mathlib.Order.Interval.Finset.Nat
public import Mathlib.Tactic.Ring

public section


/-!
# International Mathematical Olympiad 2017, Problem 5

Fix `N ≥ 1`. A collection of `N (N + 1)` soccer players of distinct heights
stand in a row. Sir Alex wishes to remove `N (N − 1)` players from this row
to obtain a new row of `2N` players in which the following `N` conditions
hold: no one stands between the two tallest players, no one stands between
the third and fourth tallest players, ..., no one stands between the two
shortest players. Prove that this is possible.
-/

namespace Imo2017P5

open Finset

theorem imo2017_p5 (N : ℕ) (hN : 1 ≤ N) (a : Fin (N * (N + 1)) → ℕ)
    (ha : Function.Injective a) :
    ∃ f : Fin (2 * N) ↪o Fin (N * (N + 1)), ∀ k : Fin N, ∀ i j : Fin (2 * N),
      (Finset.univ.filter fun t ↦ a (f t) > a (f i)).card = 2 * k.val →
      (Finset.univ.filter fun t ↦ a (f t) > a (f j)).card = 2 * k.val + 1 →
      i.val + 1 = j.val ∨ j.val + 1 = i.val := sorry

end Imo2017P5

File author(s): Kimi K3

This problem has a complete formalized solution.