fix build

leanprover-community · Feb 12, 2025 · 25db868 · 25db868
1 parent 58f12ca
commit 25db868
Showing 1 changed file with 3 additions and 5 deletions.
diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -5,7 +5,7 @@ Authors: Robin Carlier
 -/
 import Mathlib.Tactic.Zify
 import Mathlib.Data.List.Sort
-import Mathlib.Tactic.Linarith.Lemmas
+import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.NormNum.Ineq
 import Mathlib.Tactic.Ring.Basic
 /-! # Normal forms for morphisms in `SimplexCategoryGenRel`.
@@ -37,9 +37,7 @@ stones towards proving that the canonical functor
  - Show that every `P_δ` admits a unique normal form.
 -/
 
-namespace AlgebraicTopology.SimplexCategory.SimplexCategoryGenRel
-
-open CategoryTheory
+namespace AlgebraicTopology.SimplexCategoryGenRel
 
 section AdmissibleLists
 -- Impl. note: We are not bundling admissible lists as a subtype of `List ℕ` so that it remains
@@ -226,4 +224,4 @@ theorem simplicialInsert_isAdmissible (L : List ℕ) (hL : isAdmissible (m + 1)
 
 end AdmissibleLists
 
-end AlgebraicTopology.SimplexCategory.SimplexCategoryGenRel
+end AlgebraicTopology.SimplexCategoryGenRel