From 107eb69f75658b051570e15010bda799d631923a Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Fri, 10 Jan 2025 18:32:58 +0100
Subject: [PATCH] fix putnam_2022_a6

---
 lean4/src/putnam_2022_a6.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean4/src/putnam_2022_a6.lean b/lean4/src/putnam_2022_a6.lean
index 1d87f58..9a1db10 100644
--- a/lean4/src/putnam_2022_a6.lean
+++ b/lean4/src/putnam_2022_a6.lean
@@ -13,6 +13,6 @@ theorem putnam_2022_a6
     IsGreatest
       {m : ℕ | ∃ x : ℕ → ℝ,
         StrictMono x ∧ -1 < x 1 ∧ x (2 * n) < 1 ∧
-        ∀ k ∈ Icc 1 m, ∑ i in Finset.Icc 1 n, ((x (2 * i - 1) : ℝ) ^ (2 * k - 1) - (x (2 * i)) ^ (2 * k - 1)) = 1}
+        ∀ k ∈ Icc 1 m, ∑ i in Icc 1 n, ((x (2 * i) : ℝ) ^ (2 * k - 1) - (x (2 * i - 1)) ^ (2 * k - 1)) = 1}
     (putnam_2022_a6_solution n) :=
   sorry