Drop a duplicate lemma, move the remaining file to Unused

leanprover-community · Aug 1, 2024 · fb59967 · fb59967
1 parent 607a265
commit fb59967
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 33 deletions.
diff --git 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
diff --git a/SphereEversion/ToMathlib/Unused/Fin.lean 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 _