Fix 2021 A1

This was disprovable because of an off-by-one error. Specifically, the
length of the list was the number of locations (including the initial
location) rather than the number of hops.

I have opted to rewrite the question in addition to fixing the error.

lean4/src/putnam_2021_a1.lean

@@ -10,9 +10,9 @@ Each hop has length $5$, and after each hop the grasshopper is at a point whose
 What is the smallest number of hops needed for the grasshopper to reach the point $(2021, 2021)$?
 -/
 theorem putnam_2021_a1
-(P : List (ℤ × ℤ) → Prop)
-(hP : P = fun l : List (ℤ × ℤ) => l.length ≥ 1 ∧ l[0]! = (0, 0) ∧ l[l.length-1]! = (2021, 2021) ∧
-∀ n ∈ Finset.range (l.length-1), Real.sqrt ((l[n]!.1 - l[n + 1]!.1)^2 + (l[n]!.2 - l[n + 1]!.2)^2) = 5)
-: (∃ l : List (ℤ × ℤ), P l ∧ l.length = putnam_2021_a1_solution) ∧
-∀ l : List (ℤ × ℤ), P l → l.length ≥ putnam_2021_a1_solution :=
-sorry
+    (P : List (ℤ × ℤ) → Prop)
+    (P_def : ∀ l, P l ↔ l.Chain' fun p q ↦ (p.1 - q.1) ^ 2 + (p.2 - q.2) ^ 2 = 25) :
+    IsLeast
+      {k | ∃ l, P ((0, 0) :: l) ∧ l.getLast! = (2021, 2021) ∧ l.length = k}
+      putnam_2021_a1_solution :=
+  sorry