Fix 1994 A1

The statement should be that the sum diverges, rather than that it has
no finite limit (even though these are easily equivalent given the
latent positivity hypotheses).

lean4/src/putnam_1994_a1.lean

@@ -7,7 +7,7 @@ open Filter Topology
 Suppose that a sequence $a_1,a_2,a_3,\dots$ satisfies $0<a_n \leq a_{2n}+a_{2n+1}$ for all $n \geq 1$. Prove that the series $\sum_{n=1}^\infty a_n$ diverges.
 -/
 theorem putnam_1994_a1
-(a : ℕ → ℝ)
-(ha : ∀ n ≥ 1, 0 < a n ∧ a n ≤ a (2 * n) + a (2 * n + 1))
-: ¬(∃ s : ℝ, Tendsto (fun N : ℕ => ∑ n : Set.Icc 1 N, a n) atTop (𝓝 s)) :=
-sorry
+    (a : ℕ → ℝ)
+    (ha : ∀ n ≥ 1, 0 < a n ∧ a n ≤ a (2 * n) + a (2 * n + 1)) :
+    Tendsto (fun N : ℕ => ∑ n : Set.Icc 1 N, a n) atTop atTop :=
+  sorry