lake shake fix

leanprover-community · Feb 11, 2025 · 20a2ea0 · 20a2ea0
1 parent 38840b8
commit 20a2ea0
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -3,7 +3,11 @@ Copyright (c) 2025 Robin Carlier. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robin Carlier
 -/
-import Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
+import Mathlib.Tactic.Zify
+import Mathlib.Data.List.Sort
+import Mathlib.Tactic.Linarith.Lemmas
+import Mathlib.Tactic.NormNum.Ineq
+import Mathlib.Tactic.Ring.Basic
 /-! # Normal forms for morphisms in `SimplexCategoryGenRel`.
 
 In this file, we establish that `P_δ` and `P_σ` morphisms in `SimplexCategoryGenRel`