diff --git a/SphereEversion.lean b/SphereEversion.lean
index 657df270..97a4d253 100644
--- a/SphereEversion.lean
+++ b/SphereEversion.lean
@@ -41,7 +41,6 @@ import SphereEversion.ToMathlib.Analysis.NormedSpace.Misc
 import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm
 import SphereEversion.ToMathlib.Data.Nat.Basic
 import SphereEversion.ToMathlib.Data.Set.Lattice
-import SphereEversion.ToMathlib.Data.Set.Prod
 import SphereEversion.ToMathlib.Equivariant
 import SphereEversion.ToMathlib.ExistsOfConvex
 import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm
diff --git a/SphereEversion/ToMathlib/Data/Set/Prod.lean b/SphereEversion/ToMathlib/Data/Set/Prod.lean
deleted file mode 100644
index c195be7a..00000000
--- a/SphereEversion/ToMathlib/Data/Set/Prod.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-import Mathlib.Data.Set.Prod
-
-open Set
-
-namespace Set
-
-theorem univ_prod_nonempty_iff {α β : Type*} [Nonempty α] {s : Set β} :
-    ((univ : Set α) ×ˢ s).Nonempty ↔ s.Nonempty := by simp
-
-end Set