Update lean4/src/putnam_1994_b3.lean

Co-authored-by: Eric Wieser <[email protected]>

lean4/src/putnam_1994_b3.lean

@@ -9,7 +9,7 @@ abbrev putnam_1994_b3_solution : Set ℝ := sorry
 Find the set of all real numbers $k$ with the following property: For any positive, differentiable function $f$ that satisfies $f'(x)>f(x)$ for all $x$, there is some number $N$ such that $f(x)>e^{kx}$ for all $x>N$.
 -/
 theorem putnam_1994_b3
-    (S : Set (ℝ → ℝ))
-    (S_def : ∀ f, f ∈ S ↔ (∀ x, 0 < f x ∧ f x < deriv f x) ∧ Differentiable ℝ f) :
-    {k | ∀ f ∈ S, ∃ N, ∀ x > N, Real.exp (k * x) < f x} = putnam_1994_b3_solution := by
+    :
+    {k | ∀ f (hf : (∀ x, 0 < f x ∧ f x < deriv f x) ∧ Differentiable ℝ f),
+      ∃ N, ∀ x > N, Real.exp (k * x) < f x} = putnam_1994_b3_solution := by
   sorry