From 25db868a52f92dbcd6b3f91405b12ba2f8f73599 Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Wed, 12 Feb 2025 12:24:17 +0100
Subject: [PATCH] fix build

---
 .../SimplexCategory/GeneratorsRelations/NormalForms.lean  | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index 4034d8b139910..5cdd84062696b 100644
--- 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