[Imo2010P3] easy direction

dwrensha · Nov 23, 2023 · a9dc1f8 · a9dc1f8
1 parent aedd816
commit a9dc1f8
Showing 1 changed file with 7 additions and 2 deletions.
diff --git a/Compfiles/Imo2010P3.lean b/Compfiles/Imo2010P3.lean
@@ -26,8 +26,13 @@ abbrev PosInt : Type := { x : ℤ // 0 < x }
 
 notation "ℤ>0" => PosInt
 
-determine solution_set : Set (ℤ>0 → ℤ>0) := sorry
+determine solution_set : Set (ℤ>0 → ℤ>0) := { f | f = id ∨ ∃ c, ∀ x, f x = x + c }
+
 
 problem imo2010_p3 (g : ℤ>0 → ℤ>0) :
     g ∈ solution_set ↔ ∀ m n, IsSquare ((g m + n) * (g n + m)) := by
-  sorry
+  constructor
+  · rintro (rfl | ⟨c, hc⟩) m n
+    · use m + n; rw [id, id]; ac_rfl
+    · use m + n + c; rw [hc m, hc n]; ac_rfl
+  · sorry