From a3d5752314062eca82167b74d78572878b58429e Mon Sep 17 00:00:00 2001
From: Oliver Nash <ddojsioc@google.com>
Date: Tue, 24 Sep 2024 16:00:35 +0000
Subject: [PATCH] Fix 2017 A1 (again)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The hypotheses were contradictory without the missing positivity guard
as the following succeeds without the change included here:
```
  exfalso
  have : IsQualifying S := hS.1
  rw [IsQualifying_def] at this
  obtain ⟨h₁, h₂, h₃, h₄⟩ := this
  have : -7 ∈ S := h₃ (-7) (h₄ 2 h₂)
  replace this : 0 < -7 := h₁ _ this
  linarith
```

This was previously "fixed" in c4512cac2689dfa645c831b67748e659c34990a2
but unfortunately an error remained.
---
 lean4/src/putnam_2017_a1.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean4/src/putnam_2017_a1.lean b/lean4/src/putnam_2017_a1.lean
index c149c381..fd6085a9 100644
--- a/lean4/src/putnam_2017_a1.lean
+++ b/lean4/src/putnam_2017_a1.lean
@@ -8,7 +8,7 @@ theorem putnam_2017_a1
     (IsQualifying_def : ∀ S, IsQualifying S ↔
       (∀ n ∈ S, 0 < n) ∧
       2 ∈ S ∧
-      (∀ n, n ^ 2 ∈ S → n ∈ S) ∧
+      (∀ n > 0, n ^ 2 ∈ S → n ∈ S) ∧
       (∀ n ∈ S, (n + 5) ^ 2 ∈ S))
     (S : Set ℤ)
     (hS : IsLeast IsQualifying S) :