Fix 1963 A3 (again)

This was disprovable because `y` could fail to be differentiable at `1`.
E.g., one could define `y` such that:
`y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t` for `x ≥ 1`
and `y x = 0` for `x < 1`. This will satisfy the RHS of the iff in the
goal but not the left.

I see two obvious ways to resolve the issue:
 1. Demand that `y` is C^n on `[1, ∞)`
 2. Require that `y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t`
    holds on a neighbourhood of `[1, ∞)`

The informal statement is very vague so I have somewhat arbitrarily
opted for the first of these resolutions.

This was previously "fixed" in 7a92152 but unfortunately an error remained.

lean4/src/putnam_1963_a3.lean

@@ -13,7 +13,8 @@ theorem putnam_1963_a3
     (n : ℕ)
     (hn : 0 < n)
     (f y : ℝ → ℝ)
-    (hf : ContinuousOn f (Ici 1)) :
-    ContDiffOn ℝ n y (Ici 1) ∧ (∀ i < n, deriv^[i] y 1 = 0) ∧ (Ici 1).EqOn (P n y) f ↔
+    (hf : ContinuousOn f (Ici 1))
+    (hy : ContDiffOn ℝ n y (Ici 1)) :
+    (∀ i < n, deriv^[i] y 1 = 0) ∧ (Ici 1).EqOn (P n y) f ↔
     ∀ x ≥ 1, y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t :=
   sorry