[Usa1985P1] golf

dwrensha · Dec 17, 2024 · 72acc90 · 72acc90
1 parent 086b7fe
commit 72acc90
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Compfiles/Usa1985P1.lean b/Compfiles/Usa1985P1.lean
@@ -90,9 +90,9 @@ problem usa1985_p1 :
 
   use x, k^3, k^6 * j
   refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
-  · intro ii _
+  · intro ii hii
     dsimp [x]
-    have h1 : 0 < (ii : ℤ) + 1 := by clear h3; positivity
+    have h1 : 0 < (ii : ℤ) + 1 := h0 ii hii
     have h2 : 0 < (∑ ii ∈ Finset.range 1985, ((ii:ℤ) + 1) ^ 2) ^ 4 := by
       exact pow_pos h3 4
     exact Int.mul_pos h1 h2