From a6022deb8d4b65a1204f29a19ec0f3b93479e739 Mon Sep 17 00:00:00 2001
From: David Renshaw <dwrenshaw@gmail.com>
Date: Tue, 22 Aug 2023 15:20:31 -0400
Subject: [PATCH] [Usa1998Q3] remove checks

---
 MathPuzzles/Usa1998Q3.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/MathPuzzles/Usa1998Q3.lean b/MathPuzzles/Usa1998Q3.lean
index 9957d705..84866655 100644
--- a/MathPuzzles/Usa1998Q3.lean
+++ b/MathPuzzles/Usa1998Q3.lean
@@ -128,6 +128,3 @@ theorem usa1998_q3
   -- ∏ᵢ(1 + yᵢ)/n ≥ ∏ᵢ∏_{j ≠ i} (1 - yⱼ)^{1/n}
   -- ... a bunch more steps...
   sorry
-
-#check Finset.card_erase_of_mem
-#check Real.geom_mean_le_arith_mean_weighted