From 7a73fdc0e528234aee07a9b823c53a3e70c97e5c Mon Sep 17 00:00:00 2001
From: Ondanaoto <n.onda.go20@gmail.com>
Date: Tue, 2 Apr 2024 22:00:01 +0900
Subject: [PATCH] odd

---
 Compfiles/Imo2012P4.lean | 44 ++++++++++++++++++++++++++++++++++++++--
 1 file changed, 42 insertions(+), 2 deletions(-)

diff --git a/Compfiles/Imo2012P4.lean b/Compfiles/Imo2012P4.lean
index 84d49a8a..693b6af2 100644
--- a/Compfiles/Imo2012P4.lean
+++ b/Compfiles/Imo2012P4.lean
@@ -20,7 +20,17 @@ the following equality holds:
 
 namespace Imo2012P4
 
-determine solution_set : Set (ℤ → ℤ) := sorry
+-- def odd_const (c : ℤ) : ℤ → ℤ := λ x =>
+--   match x with
+--   | 0 => 0
+--   | 1 => c
+--   |
+
+def odd_const : Set (ℤ → ℤ) := fun f =>
+  ∃ c : ℤ, ∀ x : ℤ,
+    (Odd x → f x = c) ∧ (Even x → f x = 0)
+
+determine solution_set : Set (ℤ → ℤ) := odd_const
 
 problem imo2012_p4 (f : ℤ → ℤ) :
     f ∈ solution_set ↔
@@ -121,6 +131,36 @@ problem imo2012_p4 (f : ℤ → ℤ) :
         rw [show 2 * a = a * 2 from by ring]
         linarith
 
-      sorry
+      have h_odd_const (x : ℤ) : Odd x → f x = f 1 := by
+        intro odd
+        wlog pos : x ≥ 0 with H
+        simp at pos
+        have := even (- x); simp at this
+        set y := -x with yh
+        rw [this]; clear this
+        have ynng : y ≥ 0 := by linarith
+        have y_odd : Odd y := by
+          have ⟨ k, hk ⟩ := odd
+          use -k-1
+          linarith
+
+        exact H f constraint (by assumption)
+         (by assumption) (by assumption)
+         (by assumption) (by assumption)
+         (by assumption) (by assumption) y y_odd ynng
+
+        -- when `x ≥ 0`
+        
+
+      have f_in_odd_const : f ∈ odd_const := by
+        use f 1
+        intro x
+        constructor
+        · intro odd
+          exact h_odd_const x odd
+        sorry
+
     sorry
   sorry
+
+end Imo2012P4