Add Eric's suggestion.

trishullab · Nov 4, 2024 · 6f255bd · 6f255bd
1 parent 97f9746
commit 6f255bd
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lean4/src/putnam_2003_a3.lean b/lean4/src/putnam_2003_a3.lean
@@ -10,5 +10,5 @@ Find the minimum value of $|\sin x+\cos x+\tan x+\cot x+\sec x+\csc x|$ for real
 theorem putnam_2003_a3
     (f : ℝ → ℝ)
     (hf : ∀ x : ℝ, f x = |Real.sin x + Real.cos x + Real.tan x + 1 / Real.tan x + 1 / Real.cos x + 1 / Real.sin x|) :
-    IsLeast (f '' univ) putnam_2003_a3_solution :=
+    IsLeast (Set.range f) putnam_2003_a3_solution :=
   sorry