diff --git a/SphereEversion.lean b/SphereEversion.lean
index 97a4d253..7409034d 100644
--- a/SphereEversion.lean
+++ b/SphereEversion.lean
@@ -50,7 +50,6 @@ import SphereEversion.ToMathlib.Geometry.Manifold.MiscManifold
 import SphereEversion.ToMathlib.Geometry.Manifold.SmoothManifoldWithCorners
 import SphereEversion.ToMathlib.Geometry.Manifold.VectorBundle.Misc
 import SphereEversion.ToMathlib.LinearAlgebra.Basic
-import SphereEversion.ToMathlib.LinearAlgebra.Basis
 import SphereEversion.ToMathlib.LinearAlgebra.FiniteDimensional
 import SphereEversion.ToMathlib.MeasureTheory.BorelSpace
 import SphereEversion.ToMathlib.MeasureTheory.ParametricIntervalIntegral
@@ -63,3 +62,4 @@ import SphereEversion.ToMathlib.Topology.Misc
 import SphereEversion.ToMathlib.Topology.Paracompact
 import SphereEversion.ToMathlib.Topology.Path
 import SphereEversion.ToMathlib.Topology.Separation
+import SphereEversion.ToMathlib.Unused.Fin
diff --git a/SphereEversion/ToMathlib/LinearAlgebra/Basis.lean b/SphereEversion/ToMathlib/LinearAlgebra/Basis.lean
deleted file mode 100644
index 68a4aeac..00000000
--- a/SphereEversion/ToMathlib/LinearAlgebra/Basis.lean
+++ /dev/null
@@ -1,32 +0,0 @@
-import Mathlib.LinearAlgebra.Basis.Flag
-import Mathlib.LinearAlgebra.Dual
-
-noncomputable section
-
-open Set Submodule
-
-section
-
-variable {R : Type*} [Semiring R] {M : Type*} [AddCommMonoid M] [Module R M]
-
--- not directly used
-theorem Fin.coe_succ_le_iff_le {n : ℕ} {j k : Fin n} : (j : Fin <| n + 1) ≤ k ↔ j ≤ k := by
-  simp only [Fin.coe_eq_castSucc]; rfl
-
--- not directly used
-theorem Fin.coe_lt_succ {n : ℕ} (k : Fin n) : (k : Fin <| n + 1) < k.succ := by
-  rw [Fin.coe_eq_castSucc]
-  exact Nat.lt_succ_self _
-
--- not used any more: now identical to Basis.flag_succ
-theorem Basis.flag_span_succ {n : ℕ} (b : Basis (Fin n) R M) (k : Fin n) :
-    b.flag k.succ = span R {b k} ⊔ b.flag k.castSucc := by
-  symm
-  rw [Basis.flag, ← span_union, ← image_singleton, ← image_union, flag]
-  refine congr_arg (span R <| b '' ·) <| Set.ext fun j ↦ ?_
-  have : j = k ∨ j < k ↔ ↑j < k.succ := by
-    rw [← le_iff_eq_or_lt, Fin.coe_eq_castSucc, Fin.lt_iff_val_lt_val]
-    exact Nat.lt_succ_iff.symm
-  simp [this]
-
-end
diff --git a/SphereEversion/ToMathlib/Unused/Fin.lean b/SphereEversion/ToMathlib/Unused/Fin.lean
new file mode 100644
index 00000000..28f1c219
--- /dev/null
+++ b/SphereEversion/ToMathlib/Unused/Fin.lean
@@ -0,0 +1,10 @@
+import Mathlib.Data.Fin.Basic
+
+-- not directly used
+theorem Fin.coe_succ_le_iff_le {n : ℕ} {j k : Fin n} : (j : Fin <| n + 1) ≤ k ↔ j ≤ k := by
+  simp only [Fin.coe_eq_castSucc]; rfl
+
+-- not directly used
+theorem Fin.coe_lt_succ {n : ℕ} (k : Fin n) : (k : Fin <| n + 1) < k.succ := by
+  rw [Fin.coe_eq_castSucc]
+  exact Nat.lt_succ_self _