Vilin97 · Oct 20, 2026 · Oct 20, 2026
diff --git a/LeanPool/ClassificationOfSurfaces.lean b/LeanPool/ClassificationOfSurfaces.lean
@@ -135,9 +135,6 @@ public import LeanPool.ClassificationOfSurfaces.Topology.InvarianceOfDomain
 public import LeanPool.ClassificationOfSurfaces.TriangleCell
 public import LeanPool.ClassificationOfSurfaces.Triangulation
 public import LeanPool.ClassificationOfSurfaces.WeightedCircle
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Classification of Compact Surfaces

diff --git a/LeanPool/ClassificationOfSurfaces/API.lean b/LeanPool/ClassificationOfSurfaces/API.lean
@@ -3,7 +3,7 @@ Copyright (c) 2026 ClassificationOfSurfaces contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ryan McCorvie, Jack McCarthy
 -/
-module
+module -- shake: keep-all
 
 public import LeanPool.ClassificationOfSurfaces.CellComplexQuotient
 public import LeanPool.ClassificationOfSurfaces.CanonicalCoordinates
@@ -58,10 +58,6 @@ public import LeanPool.ClassificationOfSurfaces.SphereQuotientHomeomorph
 public import LeanPool.ClassificationOfSurfaces.StrongVertexStar
 public import LeanPool.ClassificationOfSurfaces.TriangleCell
 
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Public API map

diff --git a/LeanPool/ClassificationOfSurfaces/Basic.lean b/LeanPool/ClassificationOfSurfaces/Basic.lean
@@ -8,10 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.EvalStatement
 public import LeanPool.ClassificationOfSurfaces.Examples
 
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Classification of compact surfaces

diff --git a/LeanPool/ClassificationOfSurfaces/CanonicalCoordinates.lean b/LeanPool/ClassificationOfSurfaces/CanonicalCoordinates.lean
@@ -7,10 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.RepresentativeCarrier
 public import LeanPool.ClassificationOfSurfaces.CanonicalWords
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Carrier coordinates for canonical normal-form words

diff --git a/LeanPool/ClassificationOfSurfaces/CanonicalGeneratorMaps.lean b/LeanPool/ClassificationOfSurfaces/CanonicalGeneratorMaps.lean
@@ -9,10 +9,6 @@ public import LeanPool.ClassificationOfSurfaces.CanonicalWords
 public import LeanPool.ClassificationOfSurfaces.RepresentativeCarrier
 import LeanPool.ClassificationOfSurfaces.CanonicalCoordinates
 import LeanPool.ClassificationOfSurfaces.CanonicalPairings
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Generator maps for the canonical Eval representatives

diff --git a/LeanPool/ClassificationOfSurfaces/CanonicalPairings.lean b/LeanPool/ClassificationOfSurfaces/CanonicalPairings.lean
@@ -6,10 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.CanonicalWords
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Pairings in canonical normal-form words

diff --git a/LeanPool/ClassificationOfSurfaces/CanonicalWords.lean b/LeanPool/ClassificationOfSurfaces/CanonicalWords.lean
@@ -7,10 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.CellComplexQuotient
 public import LeanPool.ClassificationOfSurfaces.Representatives
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Canonical normal-form boundary words

diff --git a/LeanPool/ClassificationOfSurfaces/CellComplex.lean b/LeanPool/ClassificationOfSurfaces/CellComplex.lean
@@ -6,10 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.Triangulation
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Finite surface cell complexes

diff --git a/LeanPool/ClassificationOfSurfaces/CellComplexQuotient.lean b/LeanPool/ClassificationOfSurfaces/CellComplexQuotient.lean
@@ -7,10 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.CellComplex
 public import LeanPool.ClassificationOfSurfaces.PolygonalQuotient
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Polygonal realization of surface cell-complex data

diff --git a/LeanPool/ClassificationOfSurfaces/DiskSquare.lean b/LeanPool/ClassificationOfSurfaces/DiskSquare.lean
@@ -9,10 +9,6 @@ public import LeanPool.ClassificationOfSurfaces.WeightedCircle
 public import LeanPool.ClassificationOfSurfaces.PolygonCellRadial
 import Mathlib.Analysis.Convex.GaugeRescale
 import Mathlib.Analysis.InnerProductSpace.Basic
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # A square model for polygon cells
@@ -1581,22 +1577,23 @@ theorem finalOldArcLocal_re_eq_one_iff_endpoint
     have hpi : 2 * Real.pi ≠ 0 := by positivity
     have heq :
         s.1 = (l : ℝ) + (t : ℝ) + (k : ℝ) * (l + 1) := by
-      field_simp [hnpos.ne'] at hk
-      nlinarith [Real.pi_pos]
+      field_simp [hnpos.ne', hpi] at hk
+      ring_nf at hk ⊢
+      exact hk
     have hkUpper : (k : ℝ) ≤ 0 := by
-      nlinarith [s.2.2, t.property.1, hnpos]
+      nlinarith only [heq, s.2.2, t.property.1, hnpos]
     have hkLower : (-1 : ℝ) ≤ k := by
-      nlinarith [s.2.1, t.property.2, hnpos]
+      nlinarith only [heq, s.2.1, t.property.2, hnpos]
     have hkUpperInt : k ≤ 0 := by exact_mod_cast hkUpper
     have hkLowerInt : (-1 : ℤ) ≤ k := by exact_mod_cast hkLower
     have hkCases : k = -1 ∨ k = 0 := by omega
     rcases hkCases with rfl | rfl
     · left
       norm_num at heq
-      nlinarith [s.2.1, t.property.2]
+      linarith only [heq, s.2.1, t.property.2]
     · right
       norm_num at heq
-      exact_mod_cast (by nlinarith [s.2.2, t.property.1] :
+      exact_mod_cast (by linarith only [heq, s.2.2, t.property.1] :
         s.1 = (l : ℝ))
   · intro hs
     rcases hs with hs | hs
@@ -1741,22 +1738,23 @@ theorem firstOldArcLocal_re_eq_one_iff_endpoint
     have hpi : 2 * Real.pi ≠ 0 := by positivity
     have heq :
         1 + s.1 = (t : ℝ) + (k : ℝ) * (r + 1) := by
-      field_simp [hnpos.ne'] at hk
-      nlinarith [Real.pi_pos]
+      field_simp [hnpos.ne', hpi] at hk
+      ring_nf at hk ⊢
+      exact hk
     have hkUpper : (k : ℝ) ≤ 1 := by
-      nlinarith [s.2.2, t.property.1, hnpos]
+      nlinarith only [heq, s.2.2, t.property.1, hnpos]
     have hkLower : (0 : ℝ) ≤ k := by
-      nlinarith [s.2.1, t.property.2, hnpos]
+      nlinarith only [heq, s.2.1, t.property.2, hnpos]
     have hkUpperInt : k ≤ 1 := by exact_mod_cast hkUpper
     have hkLowerInt : (0 : ℤ) ≤ k := by exact_mod_cast hkLower
     have hkCases : k = 0 ∨ k = 1 := by omega
     rcases hkCases with rfl | rfl
     · left
       norm_num at heq
-      nlinarith [s.2.1, t.property.2]
+      linarith only [heq, s.2.1, t.property.2]
     · right
       norm_num at heq
-      exact_mod_cast (by nlinarith [s.2.2, t.property.1] :
+      exact_mod_cast (by linarith only [heq, s.2.2, t.property.1] :
         s.1 = (r : ℝ))
   · intro hs
     rcases hs with hs | hs

diff --git a/LeanPool/ClassificationOfSurfaces/EvalStatement.lean b/LeanPool/ClassificationOfSurfaces/EvalStatement.lean
@@ -10,9 +10,6 @@ public import LeanPool.ClassificationOfSurfaces.Representatives
 public import Mathlib.Geometry.Manifold.Instances.Real
 import LeanPool.ClassificationOfSurfaces.GeometricTriangulationRealization
 import LeanPool.ClassificationOfSurfaces.NormalForm
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Lean Eval target theorem

diff --git a/LeanPool/ClassificationOfSurfaces/Examples.lean b/LeanPool/ClassificationOfSurfaces/Examples.lean
@@ -7,10 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.CellComplexQuotient
 public import LeanPool.ClassificationOfSurfaces.Representatives
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Standard combinatorial examples

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicCancellation.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicCancellation.lean
@@ -6,10 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicDerivedRewrites
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Cancellation chains for finite cyclic presentations

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicCanonical.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicCanonical.lean
@@ -7,10 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.CanonicalWords
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicPresentation
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Canonical finite cyclic presentations

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicCanonicalRealization.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicCanonicalRealization.lean
@@ -8,10 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.CanonicalGeneratorMaps
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicCanonical
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicSignedRealization
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Realization of canonical finite-cyclic presentations

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicCrosscap.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicCrosscap.lean
@@ -8,10 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicDyck
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicUnorientedRealization
 import LeanPool.ClassificationOfSurfaces.FiniteCyclicP2Realization
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # The Gallier--Xu cross-cap rewrite

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicDerivedRewrites.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicDerivedRewrites.lean
@@ -6,10 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicNormalization
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Derived Gallier--Xu word rewrites

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicDyck.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicDyck.lean
@@ -7,10 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicMoves
 import LeanPool.ClassificationOfSurfaces.FiniteCyclicMoveRealization
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # The Gallier--Xu Dyck rewrite

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicFaceMerge.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicFaceMerge.lean
@@ -6,10 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicCancellation
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Exact two-face merging for finite cyclic presentations

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicMoveRealization.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicMoveRealization.lean
@@ -8,10 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicMoves
 import LeanPool.ClassificationOfSurfaces.FiniteCyclicP1Realization
 import LeanPool.ClassificationOfSurfaces.FiniteCyclicP2Realization
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Realization invariance for finite cyclic move closures

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicMoves.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicMoves.lean
@@ -8,10 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicP2
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicRealization
 import LeanPool.ClassificationOfSurfaces.FiniteCyclicSignedRealization
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Finite cyclic move closures

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicNormalization.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicNormalization.lean
@@ -8,10 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicCrosscap
 import LeanPool.ClassificationOfSurfaces.FiniteCyclicMoveRealization
 import LeanPool.ClassificationOfSurfaces.FiniteCyclicP2DegenerateRealization
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Stable closure for Gallier--Xu normalization chains

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicNormalizationResult.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicNormalizationResult.lean
@@ -7,10 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicCanonical
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicCancellation
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Canonical output of finite-cyclic normalization

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicP1.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicP1.lean
@@ -6,10 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicPresentation
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Gallier--Xu P1 edge subdivision

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicP1Realization.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicP1Realization.lean
@@ -9,10 +9,6 @@ public import LeanPool.ClassificationOfSurfaces.FiniteCyclicMoves
 public import LeanPool.ClassificationOfSurfaces.WeightedCircle
 public import LeanPool.ClassificationOfSurfaces.PolygonCellRadial
 import LeanPool.ClassificationOfSurfaces.FiniteCyclicSignedRealization
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Polygonal realization of Gallier--Xu P1

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicP2.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicP2.lean
@@ -6,10 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicP1
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Gallier--Xu P2 face subdivision

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicP2DegenerateRealization.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicP2DegenerateRealization.lean
@@ -7,10 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicP2Realization
 public import LeanPool.ClassificationOfSurfaces.P2DegenerateDisk
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Polygonal realization of one-sided-degenerate Gallier--Xu P2

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicP2Realization.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicP2Realization.lean
@@ -8,10 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.DiskSquare
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicMoves
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicSignedRealization
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Polygonal realization of Gallier--Xu P2

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicPresentation.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicPresentation.lean
@@ -6,10 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.SignedPresentation
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Finite cyclic surface presentations

diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicRealization.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicRealization.lean
@@ -7,10 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicPresentation
 public import LeanPool.ClassificationOfSurfaces.PolygonalQuotient
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Polygonal realization of finite cyclic presentations