import Mathlib.Algebra.Group.Pointwise.Finset.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Data.Real.Basic
import Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-!
# International Mathematical Olympiad 2025, Problem 1
A line in the plane is called sunny if it is not parallel to any of the x-axis, the y-axis,
and the line x + y = 0.
Let n ⩾ 3 be a given integer. Determine all nonnegative integers k such that there exist n distinct
lines in the plane satisfying both of the following:
• for all positive integers a and b with a + b ⩽ n + 1, the point (a, b) is on at least one of the
lines; and
• exactly k of the n lines are sunny.
-/
namespace Imo2025P1
open scoped Affine Finset
open Module
/-- The `x`-axis, as an affine subspace. -/
def xAxis : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)) where
carrier := {p | p 1 = 0}
smul_vsub_vadd_mem c p₁ p₂ p₃ hp₁ hp₂ hp₃ := by simp_all
/-- The `y`-axis, as an affine subspace. -/
def yAxis : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)) where
carrier := {p | p 0 = 0}
smul_vsub_vadd_mem c p₁ p₂ p₃ hp₁ hp₂ hp₃ := by simp_all
/- The line `x+y=0`, as an affine subspace. -/
def linexy0 : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)) where
carrier := {p | p 0 + p 1 = 0}
smul_vsub_vadd_mem c p₁ p₂ p₃ hp₁ hp₂ hp₃ := by
simp only [Fin.isValue, vsub_eq_sub, vadd_eq_add, Set.mem_setOf_eq, PiLp.add_apply,
PiLp.smul_apply, PiLp.sub_apply, smul_eq_mul]
suffices c * (p₁ 0 + p₁ 1 - (p₂ 0 + p₂ 1)) + (p₃ 0 + p₃ 1) = 0 by
rw [← this]
ring
simp_all
/-- The condition on lines in the problem. -/
def Sunny (s : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2))) : Prop :=
¬ s ∥ xAxis ∧ ¬ s ∥ yAxis ∧ ¬ s ∥ linexy0
/-- The decidable predicate `Sunny`. -/
noncomputable def sunnyPred : DecidablePred Sunny := Classical.decPred _
/- determine -/ abbrev answer : Set.Ici 3 → Set ℕ := sorry
/-- The final theorem: answer is {0, 1, 3}. -/
theorem imo2025_p1 (n : Set.Ici 3) :
{k | ∃ lines : Finset (AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2))),
have := sunnyPred;
#lines = n ∧ (∀ l ∈ lines, finrank ℝ l.direction = 1) ∧
(∀ a b : ℕ, 0 < a → 0 < b → a + b ≤ (n : ℕ) + 1 → ∃ l ∈ lines, !₂[(a : ℝ), b] ∈ l) ∧
#{l ∈ lines | Sunny l} = k} = answer n := sorry
end Imo2025P1
This problem has a complete formalized solution.
The solution was imported from mathlib4.