[Usa1998Q3] remove checks

dwrensha · Aug 22, 2023 · a6022de · a6022de
1 parent 9db6922
commit a6022de
Showing 1 changed file with 0 additions and 3 deletions.
diff --git 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