diff --git a/LeanPool/ClassificationOfSurfaces.lean b/LeanPool/ClassificationOfSurfaces.lean
index 1fba4961b6..e2520fc5ac 100644
--- 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
index 11b79a6cf4..c155cb019f 100644
--- 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
index 4ff847aa00..71be8b5dc9 100644
--- 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
index ff2543f53c..771e8a58b7 100644
--- 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
index a3492c8e8f..f20d689606 100644
--- 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
index 4f54f3d9d9..1b93f6f0ff 100644
--- 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
index b1ecbedc56..e22f64bff8 100644
--- 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
index 6d771403e8..51e9c2c10d 100644
--- 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
index eea331b711..d1a7b02e3e 100644
--- 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
index 5a961b3f7f..2f2a9fcf44 100644
--- 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
index 03ad200e77..dda7964f11 100644
--- 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
index def0e8e799..38003155e0 100644
--- 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
index d15253a57c..145f7e1fee 100644
--- 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
index d79f298ee3..e94c2658e5 100644
--- 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
index b8c12996b5..4dc3bea4c6 100644
--- 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
index 3073df1372..b1564c43ce 100644
--- 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
index 61c0ff15f7..53400ace22 100644
--- 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
index 2857d6d925..8402adad43 100644
--- 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
index 1a83cfe869..0f9ac859be 100644
--- 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
index 2e1e04208b..84b2e99f29 100644
--- 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
index 83d3a6f081..8e6c91b1ce 100644
--- 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
index cd93b8c734..4a27827c9f 100644
--- 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
index 1404606ea6..2603acce99 100644
--- 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
index b2d85bf4e5..b1facfdab0 100644
--- 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
index 01d96297d7..592be1b169 100644
--- 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
index a167655149..ee4637da99 100644
--- 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
index 26d4725a44..daeac842dc 100644
--- 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
index 5d25b54bb3..d6e7c07bd5 100644
--- 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
index 6bef5d6c54..5b022558f0 100644
--- 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
index 97fc8eace9..d42169d5c9 100644
--- 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
diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicReduction.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicReduction.lean
index ea5e2976b7..a4d0a99bde 100644
--- a/LeanPool/ClassificationOfSurfaces/FiniteCyclicReduction.lean
+++ b/LeanPool/ClassificationOfSurfaces/FiniteCyclicReduction.lean
@@ -6,10 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicFaceMerge
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Combinatorial selections for finite-cyclic reduction
diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicSignedRealization.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicSignedRealization.lean
index 7af4f98ef5..c3c01de15c 100644
--- a/LeanPool/ClassificationOfSurfaces/FiniteCyclicSignedRealization.lean
+++ b/LeanPool/ClassificationOfSurfaces/FiniteCyclicSignedRealization.lean
@@ -6,11 +6,7 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicRealization
-import Mathlib.Analysis.SpecialFunctions.Bernstein
 import Mathlib.Analysis.SpecialFunctions.Complex.Circle
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Polygonal realization under signed presentation isomorphism
diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicSphereRealization.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicSphereRealization.lean
index 2536470197..0cfbcb219c 100644
--- a/LeanPool/ClassificationOfSurfaces/FiniteCyclicSphereRealization.lean
+++ b/LeanPool/ClassificationOfSurfaces/FiniteCyclicSphereRealization.lean
@@ -8,10 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicCanonical
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicRealization
 public import LeanPool.ClassificationOfSurfaces.SphereQuotientHomeomorph
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # The canonical finite-cyclic sphere realization
diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicTerminalNormalization.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicTerminalNormalization.lean
index e68dfb6dd3..c3c7ce4c5f 100644
--- a/LeanPool/ClassificationOfSurfaces/FiniteCyclicTerminalNormalization.lean
+++ b/LeanPool/ClassificationOfSurfaces/FiniteCyclicTerminalNormalization.lean
@@ -6,10 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicWordReduction
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Terminal finite-cyclic word normalization
diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicTriangulation.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicTriangulation.lean
index cba2e70568..3bb9a5143b 100644
--- a/LeanPool/ClassificationOfSurfaces/FiniteCyclicTriangulation.lean
+++ b/LeanPool/ClassificationOfSurfaces/FiniteCyclicTriangulation.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
 
 /-!
 # Finite cyclic presentations of triangulations
diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicUnorientedRealization.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicUnorientedRealization.lean
index aea7d058b9..ac896dd6f9 100644
--- a/LeanPool/ClassificationOfSurfaces/FiniteCyclicUnorientedRealization.lean
+++ b/LeanPool/ClassificationOfSurfaces/FiniteCyclicUnorientedRealization.lean
@@ -6,11 +6,7 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicSignedRealization
-import Mathlib.Analysis.SpecialFunctions.Bernstein
 import Mathlib.Analysis.SpecialFunctions.Complex.Circle
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Polygonal realization under independently reoriented faces
diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicWordReduction.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicWordReduction.lean
index dacd8000ac..081771a12d 100644
--- a/LeanPool/ClassificationOfSurfaces/FiniteCyclicWordReduction.lean
+++ b/LeanPool/ClassificationOfSurfaces/FiniteCyclicWordReduction.lean
@@ -6,10 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicWordReductionCore
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Marked finite cyclic word reduction
@@ -1956,7 +1952,7 @@ theorem targetTokens_isSeparated {n : ℕ}
         List.map_cons, List.map_append,
         List.mem_cons, List.mem_append,
         edgeOfDart_dart]
-      tauto
+      exact hresidual.elim (fun h ↦ Or.inl (Or.inr h)) (fun h ↦ Or.inr (Or.inr h))
     have heDisplayedProtected :
         edge ∈
           ReductionToken.protectedEdges
@@ -1969,7 +1965,7 @@ theorem targetTokens_isSeparated {n : ℕ}
         CompletedBlock.edges,
         List.nil_append, List.singleton_append,
         List.mem_cons, List.mem_append]
-      tauto
+      exact hprotected.elim (fun h ↦ Or.inl (Or.inr h)) (fun h ↦ Or.inr h)
     exact (List.disjoint_left.mp separatedDisplayed)
       heDisplayedResidual heDisplayedProtected
   rcases hresidual with rfl | hresidual
diff --git a/LeanPool/ClassificationOfSurfaces/FiniteCyclicWordReductionCore.lean b/LeanPool/ClassificationOfSurfaces/FiniteCyclicWordReductionCore.lean
index 1ff5c8c62e..516448c40f 100644
--- a/LeanPool/ClassificationOfSurfaces/FiniteCyclicWordReductionCore.lean
+++ b/LeanPool/ClassificationOfSurfaces/FiniteCyclicWordReductionCore.lean
@@ -7,10 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicReduction
 public import LeanPool.ClassificationOfSurfaces.FiniteCyclicNormalizationResult
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Recursive reduction of finite cyclic one-face words
diff --git a/LeanPool/ClassificationOfSurfaces/GeometricTriangulationRealization.lean b/LeanPool/ClassificationOfSurfaces/GeometricTriangulationRealization.lean
index 0422c0f5f6..926b996390 100644
--- a/LeanPool/ClassificationOfSurfaces/GeometricTriangulationRealization.lean
+++ b/LeanPool/ClassificationOfSurfaces/GeometricTriangulationRealization.lean
@@ -11,9 +11,6 @@ public import LeanPool.ClassificationOfSurfaces.TriangleCell
 public import LeanPool.ClassificationOfSurfaces.Moise.IntrinsicCellwiseExtension
 import LeanPool.ClassificationOfSurfaces.Moise.IntrinsicMidpointSubdivision
 import LeanPool.ClassificationOfSurfaces.StrongVertexStar
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Faithful polygonal realization of a geometric triangulation
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/AdaptiveControlledApproximation.lean b/LeanPool/ClassificationOfSurfaces/Moise/AdaptiveControlledApproximation.lean
index 36ce98f7fd..a2f65bf2be 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/AdaptiveControlledApproximation.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/AdaptiveControlledApproximation.lean
@@ -9,9 +9,6 @@ public import LeanPool.ClassificationOfSurfaces.Moise.AdaptiveOpenCover
 public import LeanPool.ClassificationOfSurfaces.Moise.LocallyFiniteControlledApproximation
 import LeanPool.ClassificationOfSurfaces.Moise.FacewiseComparison
 import LeanPool.ClassificationOfSurfaces.Moise.HalfPlanePolygon
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Adaptive meshes for strongly-positive metric controls
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/AdaptiveFanAffine.lean b/LeanPool/ClassificationOfSurfaces/Moise/AdaptiveFanAffine.lean
index e153742f7f..8d031da7a7 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/AdaptiveFanAffine.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/AdaptiveFanAffine.lean
@@ -210,7 +210,9 @@ theorem adaptiveGlobalFanMapStandardAffine_apply
   have hpoint := K.adaptiveGlobalFanFaceMap_standardAffine_point hU f
     (K.adaptiveGlobalFanAffinePiece hU f) haQ
       (K.adaptiveGlobalFanLinearPiece hU f) hb x
-  exact hpoint
+  simpa only [adaptiveGlobalFanFaceMapValue, adaptiveGlobalFanFaceMap,
+    adaptiveFanFaceMap, adaptiveGlobalFanMapStandardAffine, AffineMap.comp_apply,
+    LinearMap.coe_toAffineMap] using hpoint
 
 /- One adaptive global fan face is affine, in original intrinsic barycentric coordinates, as a
 function of its standard planar face coordinates. -/
@@ -236,52 +238,21 @@ theorem adaptiveFanFaceMap_val_eq_vertex_sum
   classical
   let Q := K.safeSubdivision f.1.1
   obtain ⟨a, ha⟩ := Q.affineOnFace f.1.2.1.1 f.1.2.1.2
-  let point :
-      {p // p ∈ K.adaptiveFanFaceVertices U hU f} →
-        (Q.refined.Vertex → ℝ) :=
-    fun p ↦ (K.adaptiveFanVertexSource U hU f p).1
-  let weight : {p // p ∈ K.adaptiveFanFaceVertices U hU f} → ℝ :=
-    fun p ↦ x p
-  have hweight : ∑ p, weight p = 1 := x.2.2
-  let zfun : Q.refined.Vertex → ℝ :=
-    (Finset.univ : Finset
-      {p // p ∈ K.adaptiveFanFaceVertices U hU f}
-    ).affineCombination ℝ point weight
-  have hzfun :
-      zfun = (K.adaptiveFanSourcePoint U hU f x).1 := by
-    rw [K.adaptiveFanSourcePoint_val]
-    rw [show zfun =
-        ∑ p, weight p • point p by
-      exact Finset.affineCombination_eq_linear_combination
-        Finset.univ point weight hweight]
-    funext v
-    simp only [weight, point, Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
-  have hsourceCarrier :
-      K.adaptiveFanSourcePoint U hU f x ∈
-        Q.refined.faceCarrier f.1.2.1.1 :=
+  have hsourceCarrier : K.adaptiveFanSourcePoint U hU f x ∈
+      Q.refined.faceCarrier f.1.2.1.1 :=
     K.adaptiveFanSourcePoint_mem_carrier U hU f x
   have hvertex (p : {p // p ∈ K.adaptiveFanFaceVertices U hU f}) :
-      a (point p) = p.1.1 := by
-    have hpCarrier :=
-      K.adaptiveFanVertexSource_mem_carrier U hU f p
+      a (K.adaptiveFanVertexSource U hU f p).1 = p.1.1 := by
+    have hpCarrier := K.adaptiveFanVertexSource_mem_carrier U hU f p
     have hpAffine := ha (K.adaptiveFanVertexSource U hU f p) hpCarrier
     rw [← hpAffine]
-    exact congrArg Subtype.val
-      (Q.homeo.apply_symm_apply p.1)
-  change
-    (Q.homeo (K.adaptiveFanSourcePoint U hU f x)).1 =
-      fun v ↦ ∑ p, x p * p.1.1 v
-  rw [ha _ hsourceCarrier]
-  change a (K.adaptiveFanSourcePoint U hU f x).1 = _
-  rw [← hzfun,
-    (Finset.univ : Finset
-      {p // p ∈ K.adaptiveFanFaceVertices U hU f}
-    ).map_affineCombination point weight hweight a,
-    Finset.affineCombination_eq_linear_combination
-      Finset.univ (a ∘ point) weight hweight]
+    exact congrArg Subtype.val (Q.homeo.apply_symm_apply p.1)
+  change (Q.homeo (K.adaptiveFanSourcePoint U hU f x)).1 =
+    fun v ↦ ∑ p, x p * p.1.1 v
+  rw [ha _ hsourceCarrier, K.adaptiveFanSourcePoint_val U hU f x,
+    affineMap_apply_weighted_sum a
+      (fun p ↦ (K.adaptiveFanVertexSource U hU f p).1) x]
   funext v
-  simp only [Function.comp_apply, Finset.sum_apply, Pi.smul_apply,
-    smul_eq_mul, weight]
   apply Finset.sum_congr rfl
   intro p _
   rw [hvertex p]
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/AdaptiveFanComplex.lean b/LeanPool/ClassificationOfSurfaces/Moise/AdaptiveFanComplex.lean
index 5a5164a696..4451b917c4 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/AdaptiveFanComplex.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/AdaptiveFanComplex.lean
@@ -383,6 +383,14 @@ noncomputable def adaptiveFanSourcePoint (hU : IsOpen U)
     intro p _
     rw [(K.adaptiveFanVertexSource_mem_carrier U hU f p) v hv, mul_zero]
 
+/-- The coordinate function underlying an adaptive fan source point. -/
+theorem adaptiveFanSourcePoint_val (hU : IsOpen U)
+    (f : K.AdaptiveFanFace U hU)
+    (x : stdSimplex ℝ {p // p ∈ K.adaptiveFanFaceVertices U hU f}) :
+    (K.adaptiveFanSourcePoint U hU f x).1 =
+      (fun v ↦ ∑ p, x p * (K.adaptiveFanVertexSource U hU f p).1 v) := by
+  simp only [adaptiveFanSourcePoint]
+
 theorem adaptiveFanSourcePoint_mem_carrier (hU : IsOpen U)
     (f : K.AdaptiveFanFace U hU)
     (x : stdSimplex ℝ {p // p ∈ K.adaptiveFanFaceVertices U hU f}) :
@@ -391,7 +399,7 @@ theorem adaptiveFanSourcePoint_mem_carrier (hU : IsOpen U)
   by
     classical
     intro v hv
-    change (∑ p, x p * (K.adaptiveFanVertexSource U hU f p).1 v) = 0
+    rw [K.adaptiveFanSourcePoint_val U hU f x]
     apply Finset.sum_eq_zero
     intro p _
     rw [(K.adaptiveFanVertexSource_mem_carrier U hU f p) v hv, mul_zero]
@@ -417,7 +425,7 @@ theorem adaptiveFanSourcePoint_simplexLineMap (hU : IsOpen U)
           (K.adaptiveFanSourcePoint U hU f y).1 r.1 := by
   classical
   funext v
-  simp only [adaptiveFanSourcePoint, adaptiveFanSimplexLineMap,
+  simp only [adaptiveFanSourcePoint_val, adaptiveFanSimplexLineMap,
     AffineMap.lineMap_apply_module, Pi.add_apply, Pi.smul_apply, smul_eq_mul]
   change (∑ p, (((1 - r.1) • x.1 + r.1 • y.1) p) *
       (K.adaptiveFanVertexSource U hU f p).1 v) =
@@ -444,10 +452,8 @@ theorem adaptiveFanSourcePoint_vertex (hU : IsOpen U)
   classical
   apply Subtype.ext
   funext v
-  change (∑ q, (stdSimplex.vertex p :
-        stdSimplex ℝ {p // p ∈ K.adaptiveFanFaceVertices U hU f}) q *
-      (K.adaptiveFanVertexSource U hU f q).1 v) =
-        (K.adaptiveFanVertexSource U hU f p).1 v
+  rw [K.adaptiveFanSourcePoint_val]
+  dsimp only
   rw [Finset.sum_eq_single p]
   · simp
   · intro q _ hqp
@@ -523,6 +529,7 @@ theorem adaptiveFanSourcePoint_opposite (hU : IsOpen U)
       x.1 (K.adaptiveFanCenterVertex U hU f) / 3 := by
   classical
   let c := K.adaptiveFanCenterVertex U hU f
+  rw [K.adaptiveFanSourcePoint_val]
   change (∑ p, x p * (K.adaptiveFanVertexSource U hU f p).1
       ((K.safeSubdivision f.1.1).refined.faceVertex f.1.2.1 (f.2.1 + 2))) = x c / 3
   rw [Finset.sum_eq_single c]
@@ -579,6 +586,7 @@ theorem adaptiveFanSourcePoint_faceVertex_lower_bound (hU : IsOpen U)
   have hqNonneg : 0 ≤ x q * (K.adaptiveFanVertexSource U hU f q).1
       ((K.safeSubdivision f.1.1).refined.faceVertex f.1.2.1 i) :=
     mul_nonneg (x.2.1 q) ((K.adaptiveFanVertexSource U hU f q).2.1.1 _)
+  rw [K.adaptiveFanSourcePoint_val]
   change x c / 3 ≤ ∑ r, x r * (K.adaptiveFanVertexSource U hU f r).1
     ((K.safeSubdivision f.1.1).refined.faceVertex f.1.2.1 i)
   rw [K.adaptiveFanVertex_univ U hU f,
@@ -611,10 +619,12 @@ theorem adaptiveFanSourcePoint_eq_lineMap_normalizedBase (hU : IsOpen U)
   have hpNot : p ∉ ({q} : Finset _) := by
     simp [p, q, K.adaptiveFanFirstVertex_ne_second U hU f]
   funext v
-  change (∑ r, x r * (K.adaptiveFanVertexSource U hU f r).1 v) = _
+  rw [K.adaptiveFanSourcePoint_val]
+  dsimp only
   rw [K.adaptiveFanVertex_univ U hU f,
     Finset.sum_insert hcNot, Finset.sum_insert hpNot, Finset.sum_singleton,
     AffineMap.lineMap_apply_module]
+  rw [K.adaptiveFanSourcePoint_val]
   change x.1 c * _ + (x.1 p * _ + x.1 q * _) =
     (1 - d) * (K.adaptiveFanVertexSource U hU f c).1 v +
       d * (∑ r,
@@ -830,39 +840,6 @@ theorem affineIndependent_adaptiveFanVertexSource_val (hU : IsOpen U)
     exact hthree.range
   · exact K.adaptiveFanVertexSource_val_injective U hU f
 
-/-- The affine combination map is injective when its source points are affinely independent. -/
-theorem affineCombination_injective_of_affineIndependent
-    {ι E : Type*} [Fintype ι] [AddCommGroup E] [Module ℝ E]
-    (source : ι → E) (hsource : AffineIndependent ℝ source) :
-    Function.Injective (fun x : stdSimplex ℝ ι ↦
-      Finset.univ.affineCombination ℝ source x) := by
-  intro x y hxy
-  have hweights := (hsource.affineCombination_eq_iff_eq x.2.2 y.2.2).mp hxy
-  exact Subtype.ext (funext fun i ↦ hweights i (Finset.mem_univ i))
-
-theorem simplex_eq_of_weighted_sum_eq_of_affineIndependent
-    {ι α : Type*} [Fintype ι]
-    (source : ι → α → ℝ) (hsource : AffineIndependent ℝ source)
-    {x y : stdSimplex ℝ ι}
-    (hxy : (fun v ↦ ∑ p, x p * source p v) =
-      (fun v ↦ ∑ p, y p * source p v)) :
-    x = y := by
-  apply affineCombination_injective_of_affineIndependent source hsource
-  change Finset.univ.affineCombination ℝ source x =
-    Finset.univ.affineCombination ℝ source y
-  rw [Finset.univ.affineCombination_eq_linear_combination source x x.2.2,
-    Finset.univ.affineCombination_eq_linear_combination source y y.2.2]
-  funext v
-  simpa only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul] using congrFun hxy v
-
-/-- The coordinate function underlying an adaptive fan source point. -/
-theorem adaptiveFanSourcePoint_val (hU : IsOpen U)
-    (f : K.AdaptiveFanFace U hU)
-    (x : stdSimplex ℝ {p // p ∈ K.adaptiveFanFaceVertices U hU f}) :
-    (K.adaptiveFanSourcePoint U hU f x).1 =
-      (fun v ↦ ∑ p, x p * (K.adaptiveFanVertexSource U hU f p).1 v) := by
-  rfl
-
 /-- The standard simplex parametrizing one adaptive fan face. -/
 abbrev adaptiveFanSimplex (hU : IsOpen U) (f : K.AdaptiveFanFace U hU) :=
   stdSimplex ℝ {p // p ∈ K.adaptiveFanFaceVertices U hU f}
@@ -878,14 +855,11 @@ theorem adaptiveFanSourcePoint_val_injective (hU : IsOpen U)
     (f : K.AdaptiveFanFace U hU) :
     Function.Injective (K.adaptiveFanSourcePointVal U hU f) := by
   intro x y hxy
-  let source : {p // p ∈ K.adaptiveFanFaceVertices U hU f} →
-      (K.safeSubdivision f.1.1).refined.Vertex → ℝ :=
-    fun p ↦ (K.adaptiveFanVertexSource U hU f p).1
-  apply simplex_eq_of_weighted_sum_eq_of_affineIndependent source
+  apply simplex_eq_of_weighted_sum_eq_of_affineIndependent
+    (fun p ↦ (K.adaptiveFanVertexSource U hU f p).1)
     (K.affineIndependent_adaptiveFanVertexSource_val U hU f)
-  change (fun v ↦ ∑ p, x p * (K.adaptiveFanVertexSource U hU f p).1 v) =
-    (fun v ↦ ∑ p, y p * (K.adaptiveFanVertexSource U hU f p).1 v) at hxy
-  simpa only [source, Finset.sum_apply, Pi.smul_apply, smul_eq_mul] using hxy
+  exact (K.adaptiveFanSourcePoint_val U hU f x).symm.trans
+    (hxy.trans (K.adaptiveFanSourcePoint_val U hU f y))
 
 /-- One parametrized fan triangle in the open subspace. -/
 noncomputable def adaptiveFanFaceMap (hU : IsOpen U)
@@ -1082,6 +1056,7 @@ theorem adaptiveFanSourcePoint_baseSimplexPath_val (hU : IsOpen U)
   have hpNot : p ∉ ({q} : Finset _) := by
     simp [p, q, K.adaptiveFanFirstVertex_ne_second U hU f]
   funext v
+  rw [K.adaptiveFanSourcePoint_val]
   change (∑ z, K.adaptiveFanBaseSimplexPath U hU f r z *
       (K.adaptiveFanVertexSource U hU f z).1 v) = _
   rw [K.adaptiveFanVertex_univ U hU f,
@@ -1442,7 +1417,7 @@ theorem levelFaceEdgeParameter_adaptiveFanFaceMap_of_center_eq_zero
         K.adaptiveFanSourcePoint U hU f x := by
     exact (K.safeSubdivision f.1.1).homeo.symm_apply_apply _
   unfold levelFaceEdgeParameter
-  rw [hsymm]
+  rw [hsymm, K.adaptiveFanSourcePoint_val]
   change (∑ r, x r * (K.adaptiveFanVertexSource U hU f r).1
       ((K.safeSubdivision f.1.1).refined.faceVertex f.1.2.1 (f.2.1 + 1))) = _
   rw [K.adaptiveFanVertex_univ U hU f,
@@ -1853,6 +1828,7 @@ theorem adaptiveFanFaceMap_mem_relInterior_of_center_pos (hU : IsOpen U)
     intro p
     exact mul_nonneg (x.2.1 p)
       ((K.adaptiveFanVertexSource U hU f p).2.1.1 _)
+  rw [K.adaptiveFanSourcePoint_val]
   change 0 < ∑ p, x p * (K.adaptiveFanVertexSource U hU f p).1
     ((K.safeSubdivision f.1.1).refined.faceVertex f.1.2.1 i)
   exact lt_of_lt_of_le hterm
@@ -3032,6 +3008,7 @@ theorem adaptiveFanFaceMap_eq_of_extendedCoordinates_eq_of_same_tile
   apply congrArg (K.safeSubdivision t.1).homeo
   apply Subtype.ext
   funext v
+  rw [K.adaptiveFanSourcePoint_val, K.adaptiveFanSourcePoint_val]
   change (∑ p, x p * (K.adaptiveFanVertexSource U hU ⟨t, i, a⟩ p).1 v) =
     ∑ p, y p * (K.adaptiveFanVertexSource U hU ⟨t, j, b⟩ p).1 v
   simpa only [adaptiveFanVertexSource] using
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/BoundaryInvariant.lean b/LeanPool/ClassificationOfSurfaces/Moise/BoundaryInvariant.lean
index f755a58919..6f1f182a87 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/BoundaryInvariant.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/BoundaryInvariant.lean
@@ -8,9 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.Surface
 public import LeanPool.ClassificationOfSurfaces.Moise.PlaneComplex
 import LeanPool.ClassificationOfSurfaces.Moise.Brouwer
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Boundary invariance for C0 surface charts
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/Brouwer.lean b/LeanPool/ClassificationOfSurfaces/Moise/Brouwer.lean
index 793be143b9..8ce9a81e05 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/Brouwer.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/Brouwer.lean
@@ -8,10 +8,7 @@ module
 public import LeanPool.ClassificationOfSurfaces.Topology.InvarianceOfDomain
 public import LeanPool.ClassificationOfSurfaces.Moise.PlaneComplex
 import LeanPool.ClassificationOfSurfaces.Moise.NoRetraction
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
 import Mathlib.Geometry.Euclidean.Sphere.Basic
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Brouwer's fixed-point theorem for the plane disk
@@ -110,7 +107,7 @@ private lemma fixedPointRayScale_eq_one_of_mem_sphere (p x : Plane) (hpx : p ≠
   let c := ⟪p, p⟫_ℝ
   let t := fixedPointRayScale p x
   have hroot : a * t ^ 2 + 2 * b * t + c = 1 := by
-    simpa [a, b, c, t] using fixedPointRayScale_quadratic p x hpx hp
+    simpa only [a, b, c, t] using fixedPointRayScale_quadratic p x hpx hp
   have hxinner : ⟪x, x⟫_ℝ = 1 := by
     rw [real_inner_self_eq_norm_sq, hx]
     norm_num
@@ -119,7 +116,7 @@ private lemma fixedPointRayScale_eq_one_of_mem_sphere (p x : Plane) (hpx : p ≠
     simp only [inner_add_left, inner_add_right] at hxinner
     rw [real_inner_comm p (x - p)] at hxinner
     dsimp only [a, b, c]
-    nlinarith [hxinner]
+    linarith only [hxinner, real_inner_comm p (x - p)]
   let s : EuclideanGeometry.Sphere Plane := ⟨0, 1⟩
   have hxmem : x ∈ s := by
     change dist x (0 : Plane) = 1
@@ -139,14 +136,15 @@ private lemma fixedPointRayScale_eq_one_of_mem_sphere (p x : Plane) (hpx : p ≠
           rw [inner_add_right, real_inner_comm p (x - p)]
     rwa [hinner] at hgeom
   have ht : a * t = -b + Real.sqrt (b ^ 2 + a * (1 - c)) := by
-    simpa [a, b, c, t] using fixedPointRayScale_mul_inner p x hpx
+    simpa only [a, b, c, t] using fixedPointRayScale_mul_inner p x hpx
   have hfactor : 0 < a * (t + 1) + 2 * b := by
-    nlinarith [Real.sqrt_nonneg (b ^ 2 + a * (1 - c))]
+    rw [mul_add, mul_one]
+    linarith only [ht, hab, Real.sqrt_nonneg (b ^ 2 + a * (1 - c))]
   have hprod : (t - 1) * (a * (t + 1) + 2 * b) = 0 := by
-    nlinarith [hroot, hrootOne]
+    nlinarith only [hroot, hrootOne]
   have htOne : t = 1 := by
     rcases mul_eq_zero.mp hprod with h | h
-    · linarith
+    · linarith only [h]
     · exact False.elim (hfactor.ne' h)
   exact htOne
 
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/ChartExtraction.lean b/LeanPool/ClassificationOfSurfaces/Moise/ChartExtraction.lean
index 72cb5c358e..a29c16ad79 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/ChartExtraction.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/ChartExtraction.lean
@@ -9,9 +9,6 @@ public import LeanPool.ClassificationOfSurfaces.Moise.PlaneComplex
 public import Mathlib.Geometry.Manifold.Instances.Real
 import LeanPool.ClassificationOfSurfaces.Moise.BoundaryInvariant
 import LeanPool.ClassificationOfSurfaces.Moise.Brouwer
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Extraction of Moise charts from the mathlib atlas
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/ChartInduction.lean b/LeanPool/ClassificationOfSurfaces/Moise/ChartInduction.lean
index 5b80fe71a7..cf0ced2381 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/ChartInduction.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/ChartInduction.lean
@@ -8,9 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.Moise.ChartInductionCore
 import LeanPool.ClassificationOfSurfaces.Moise.FineSubdivision
 import LeanPool.ClassificationOfSurfaces.Moise.IntrinsicMarkedFan
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # The Radó crossing weld and chart induction
@@ -1792,7 +1789,9 @@ private theorem MixedLocalFanCertificate.hasLocalCommonCoordinates_iff
       (pushGeometricRealization C.oldCompactToCommon
           C.mixedOldComplex.compactIntrinsic.faces x).1 =
         (pushGeometricRealization M.targetToCommon M.localComplex.faces z).1 := by
-  rfl
+  simp only [MixedLocalFanCertificate.hasLocalCommonCoordinates,
+    pushGeometricRealization_val, stdSimplex.map]
+  exact Iff.rfl
 
 /-- A local realization lifts canonically to the compact mixed complex, with the same coordinates
 after amalgamating the local vertices. -/
@@ -2110,8 +2109,6 @@ private theorem MixedLocalFanCertificate.positive_usedOld_isLocal_of_common
     (hv : 0 < xb.1 (C.compactVertexEquiv.symm v)) :
     ∃ u : M.localComplex.UsedVertex, M.localUsedOldEmbedding u = v := by
   classical
-  let : Fintype M.UsedOldVertex :=
-    C.mixedOldComplex.compactIntrinsic.vertexFintype
   apply exists_local_of_positive_of_amalgamated_coordinates
     M.localUsedOldEmbedding M.localUsedVertexEmbedding
     (fun w ↦ xb.1 (C.compactVertexEquiv.symm w))
@@ -4645,11 +4642,6 @@ private theorem chartInduction_relabel_agree
   let R := ChartInductionGeometry.subdivision P
   let source := ChartInductionGeometry.source P G.anchorLines
   intro x y hxy
-  change
-    (G.oldEmbed C ∘ (relabelGeometricRealizationHomeomorph C.oldCompactToCommon
-      (G.mixedOldComplex C).compactIntrinsic.faces).symm) x =
-    (G.targetEmbed ∘ (relabelGeometricRealizationHomeomorph M.targetToCommon
-      G.targetMesh.triangles).symm) y
   exact MixedLocalFanCertificate.common_relabel_agree_small
     M C G.targetMesh.triangles (G.oldEmbed C) G.targetEmbed
     (fun tf xb yb hxb hcoords ↦
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/ChartInductionCore.lean b/LeanPool/ClassificationOfSurfaces/Moise/ChartInductionCore.lean
index 255dd7aeb7..3c2124d452 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/ChartInductionCore.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/ChartInductionCore.lean
@@ -11,9 +11,6 @@ public import LeanPool.ClassificationOfSurfaces.Moise.RelativeSynchronizedArrang
 import LeanPool.ClassificationOfSurfaces.Moise.AdaptiveFanAffine
 import LeanPool.ClassificationOfSurfaces.Moise.Brouwer
 import LeanPool.ClassificationOfSurfaces.Moise.EmbeddedComplexValence
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 import Mathlib.Topology.Metrizable.Urysohn
 
 /-!
@@ -70,6 +67,23 @@ private theorem TriangleMesh.baryEval_eq_iff_of_triangles_subset (R : TriangleMe
       (show R.coordinateEmbed xR = R.coordinateEmbed yR from hxy))
   · exact congrArg R.toPlaneComplex.baryEval
 
+/-- Compare two restrictions before specializing their ambient mesh and predicates. -/
+private theorem TriangleMesh.restrictTriangles_coordinateEmbed_eq_iff (R : TriangleMesh)
+    (p q : Finset R.Vertex → Prop) [DecidablePred p] [DecidablePred q]
+    (x : GeometricRealization (R.restrictTriangles p).Vertex
+      (R.restrictTriangles p).triangles)
+    (y : GeometricRealization (R.restrictTriangles q).Vertex
+      (R.restrictTriangles q).triangles) :
+    (R.restrictTriangles p).coordinateEmbed x =
+        (R.restrictTriangles q).coordinateEmbed y ↔
+      (x : (R.restrictTriangles p).Vertex → ℝ) =
+        (y : (R.restrictTriangles q).Vertex → ℝ) := by
+  refine TriangleMesh.baryEval_eq_iff_of_triangles_subset R ?_ ?_ x y
+  · intro t ht
+    exact ((R.mem_restrictTriangles_triangles p).mp ht).1
+  · intro t ht
+    exact ((R.mem_restrictTriangles_triangles q).mp ht).1
+
 /-- A finite two-dimensional complex embedded in `S`, not necessarily covering it.  The
 realization is computed from the combinatorial data (as in `GeometricTriangulation`), so the
 support of a partial triangulation is a genuine finite polyhedron sitting inside `S`. -/
@@ -2563,15 +2577,13 @@ theorem patchMeshes_coordinateEmbed_eq_iff (k : ChartKind)
         (Q.patchNewMesh k).coordinateEmbed y ↔
       (x : (Q.patchOldMesh k).Vertex → ℝ) =
         (y : (Q.patchNewMesh k).Vertex → ℝ) := by
-  refine TriangleMesh.baryEval_eq_iff_of_triangles_subset
+  classical
+  exact TriangleMesh.restrictTriangles_coordinateEmbed_eq_iff
     (PolygonalFamily.synchronizedArrangement (Q.patchFacePolygon k) (patchTriangleMesh k))
-    ?_ ?_ x y
-  · intro t ht
-    exact ((PolygonalFamily.selectedSynchronizedMesh_triangle_mem
-      (Q.patchFacePolygon k) (patchTriangleMesh k) (fun _ ↦ True)).mp ht).1
-  · intro t ht
-    exact ((PolygonalFamily.targetSynchronizedMesh_triangle_mem
-      (Q.patchFacePolygon k) (patchTriangleMesh k)).mp ht).1
+    (PolygonalFamily.IsSelectedSynchronizedTriangle
+      (Q.patchFacePolygon k) (patchTriangleMesh k) (fun _ ↦ True))
+    (PolygonalFamily.IsTargetSynchronizedTriangle
+      (Q.patchFacePolygon k) (patchTriangleMesh k)) x y
 
 /-- If the retained source coordinates land in a closed model region, the whole replacement
 support does too. -/
@@ -2843,14 +2855,12 @@ theorem synchronizedPatchMeshes_coordinateEmbed_eq_iff (k : ChartKind)
         (synchronizedPatchNewMesh k J).coordinateEmbed y ↔
       (x : (synchronizedPatchOldMesh k J).Vertex → ℝ) =
         (y : (synchronizedPatchNewMesh k J).Vertex → ℝ) := by
-  refine TriangleMesh.baryEval_eq_iff_of_triangles_subset
-    (PolygonalFamily.synchronizedArrangement J k.patchComplex.toTriangleMesh) ?_ ?_ x y
-  · intro t ht
-    exact ((PolygonalFamily.selectedSynchronizedMesh_triangle_mem J
-      k.patchComplex.toTriangleMesh (fun _ ↦ True)).mp ht).1
-  · intro t ht
-    exact ((PolygonalFamily.targetSynchronizedMesh_triangle_mem J
-      k.patchComplex.toTriangleMesh).mp ht).1
+  classical
+  exact TriangleMesh.restrictTriangles_coordinateEmbed_eq_iff
+    (PolygonalFamily.synchronizedArrangement J k.patchComplex.toTriangleMesh)
+    (PolygonalFamily.IsSelectedSynchronizedTriangle J k.patchComplex.toTriangleMesh
+      (fun _ ↦ True))
+    (PolygonalFamily.IsTargetSynchronizedTriangle J k.patchComplex.toTriangleMesh) x y
 
 /-- Transport the finite polygonal member of a synchronized patch weld to the surface. -/
 noncomputable def synchronizedPatchOldSurfaceEmbed
@@ -3030,13 +3040,11 @@ theorem meshes_coordinateEmbed_eq_iff (J : ι → PolygonalCircle) (N : Triangle
     (oldMesh J N).coordinateEmbed x = (newMesh J N).coordinateEmbed y ↔
       (x : (oldMesh J N).Vertex → ℝ) =
         (y : (newMesh J N).Vertex → ℝ) := by
-  refine TriangleMesh.baryEval_eq_iff_of_triangles_subset
-    (PolygonalFamily.synchronizedArrangement J N) ?_ ?_ x y
-  · intro t ht
-    exact ((PolygonalFamily.selectedSynchronizedMesh_triangle_mem J N
-      (fun _ ↦ True)).mp ht).1
-  · intro t ht
-    exact ((PolygonalFamily.targetSynchronizedMesh_triangle_mem J N).mp ht).1
+  classical
+  exact TriangleMesh.restrictTriangles_coordinateEmbed_eq_iff
+    (PolygonalFamily.synchronizedArrangement J N)
+    (PolygonalFamily.IsSelectedSynchronizedTriangle J N (fun _ ↦ True))
+    (PolygonalFamily.IsTargetSynchronizedTriangle J N) x y
 
 /-- Transport the selected polygonal member of an arbitrary synchronized weld to the surface. -/
 noncomputable def oldSurfaceEmbed
@@ -3353,13 +3361,11 @@ theorem meshes_coordinateEmbed_eq_iff
         (newMesh J N lines).coordinateEmbed y ↔
       (x : (oldMesh J N lines).Vertex → ℝ) =
         (y : (newMesh J N lines).Vertex → ℝ) := by
-  refine TriangleMesh.baryEval_eq_iff_of_triangles_subset
-    (PolygonalFamily.relativeSynchronizedArrangement J N lines) ?_ ?_ x y
-  · intro t ht
-    exact ((PolygonalFamily.selectedRelativeSynchronizedMesh_triangle_mem
-      J N lines (fun _ ↦ True)).mp ht).1
-  · intro t ht
-    exact ((PolygonalFamily.targetRelativeSynchronizedMesh_triangle_mem J N lines).mp ht).1
+  classical
+  exact TriangleMesh.restrictTriangles_coordinateEmbed_eq_iff
+    (PolygonalFamily.relativeSynchronizedArrangement J N lines)
+    (PolygonalFamily.IsSelectedRelativeSynchronizedTriangle J N lines (fun _ ↦ True))
+    (PolygonalFamily.IsTargetRelativeSynchronizedTriangle J N lines) x y
 
 /-- The `oldSurfaceEmbed` declaration. -/
 noncomputable def oldSurfaceEmbed
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/ChartPatch.lean b/LeanPool/ClassificationOfSurfaces/Moise/ChartPatch.lean
index d04c220fac..5c3033283c 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/ChartPatch.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/ChartPatch.lean
@@ -7,9 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.Moise.ChartExtraction
 public import LeanPool.ClassificationOfSurfaces.Moise.ElementaryMove
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # A fixed polygonal patch inside the Rado chart models
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/Countermodels.lean b/LeanPool/ClassificationOfSurfaces/Moise/Countermodels.lean
index cdb1ce98cc..29f6461d05 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/Countermodels.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/Countermodels.lean
@@ -6,10 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.CellComplex
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Countermodels and semantic anchors
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/DualConnectivity.lean b/LeanPool/ClassificationOfSurfaces/Moise/DualConnectivity.lean
index b05ade0df4..0c76960249 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/DualConnectivity.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/DualConnectivity.lean
@@ -9,9 +9,6 @@ public import LeanPool.ClassificationOfSurfaces.Moise.ChartInductionCore
 import LeanPool.ClassificationOfSurfaces.Moise.EmbeddedComplexValence
 import LeanPool.ClassificationOfSurfaces.Moise.IntrinsicMarkedFan
 import LeanPool.ClassificationOfSurfaces.Moise.PuncturedSurface
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Dual connectivity of completed surface triangulations
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/ElementaryMove.lean b/LeanPool/ClassificationOfSurfaces/Moise/ElementaryMove.lean
index a4157e7ce8..6672cdb55a 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/ElementaryMove.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/ElementaryMove.lean
@@ -88,7 +88,7 @@ theorem diamondFan_affineIndependent {a : ℝ} (ha0 : -2 < a) (ha2 : a < 2)
         simp only [diamondFanPosition_apply_zero, diamondFanPosition_apply_four,
           diamondFanPosition_apply_two, planePoint_apply_zero, planePoint_apply_one,
           PiLp.sub_apply]
-        linarith
+        linarith only [ha2]
       convert h using 1; funext i; fin_cases i <;> rfl
     · ext v
       fin_cases v <;> simp
@@ -99,7 +99,7 @@ theorem diamondFan_affineIndependent {a : ℝ} (ha0 : -2 < a) (ha2 : a < 2)
         simp only [diamondFanPosition_apply_one, diamondFanPosition_apply_two,
           diamondFanPosition_apply_four, planePoint_apply_zero, planePoint_apply_one,
           PiLp.sub_apply]
-        linarith
+        linarith only [ha2]
       convert h using 1; funext i; fin_cases i <;> rfl
     · ext v
       fin_cases v <;> simp
@@ -293,7 +293,7 @@ theorem diamondFan_left_union {a : ℝ} (ha0 : -2 < a) (ha1 : a < 2) :
     convexHull ℝ (diamondFanPosition a '' (({0, 4, 2} : Finset (Fin 5)) : Set _)) ∪
         convexHull ℝ (diamondFanPosition a '' (({0, 3, 4} : Finset (Fin 5)) : Set _)) =
       diamondLeftRegion := by
-  have hc0 : 0 < (2 - a) / 4 := by linarith
+  have hc0 : 0 < (2 - a) / 4 := by linarith only [ha1]
   have hc1 : (2 - a) / 4 < 1 := by linarith
   have hsplit := triangle_edge_split_union
     ![planePoint 0 2, planePoint 0 (-2), planePoint (-1) 0]
@@ -321,7 +321,7 @@ theorem diamondFan_right_union {a : ℝ} (ha0 : -2 < a) (ha1 : a < 2) :
     convexHull ℝ (diamondFanPosition a '' (({1, 2, 4} : Finset (Fin 5)) : Set _)) ∪
         convexHull ℝ (diamondFanPosition a '' (({1, 4, 3} : Finset (Fin 5)) : Set _)) =
       diamondRightRegion := by
-  have hc0 : 0 < (2 - a) / 4 := by linarith
+  have hc0 : 0 < (2 - a) / 4 := by linarith only [ha1]
   have hc1 : (2 - a) / 4 < 1 := by linarith
   have hsplit := triangle_edge_split_union
     ![planePoint 0 2, planePoint 0 (-2), planePoint 1 0]
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/EmbeddedComplexValence.lean b/LeanPool/ClassificationOfSurfaces/Moise/EmbeddedComplexValence.lean
index 53f9b47452..03ea781e75 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/EmbeddedComplexValence.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/EmbeddedComplexValence.lean
@@ -8,9 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.Moise.GeometricTriangulation
 public import Mathlib.Geometry.Manifold.Instances.Real
 import LeanPool.ClassificationOfSurfaces.Moise.Brouwer
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Edge valence of a triangle complex embedded in a surface
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/FacewiseComparison.lean b/LeanPool/ClassificationOfSurfaces/Moise/FacewiseComparison.lean
index 98132c7045..d00c1e027a 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/FacewiseComparison.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/FacewiseComparison.lean
@@ -8,9 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.Moise.LocallyFinitePLApproximation
 import LeanPool.ClassificationOfSurfaces.Moise.LocallyFiniteSidePreservation
 import Mathlib.Analysis.Normed.Affine.AddTorsor
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # The per-face comparison map for locally finite side preservation
@@ -1124,7 +1121,7 @@ theorem dist_completePath_comparison_lt (G : K.PlaneGraphRealization)
       exact (AffineMap.lineMap _ _).apply_lineMap _ _ _
     rw [hcp, hprofile, hsrcpt]
     have h2r : (2 : ℝ) * r ∈ Set.Icc (0 : ℝ) 1 :=
-      ⟨by linarith [hr.1], by linarith⟩
+      ⟨by linarith only [hr.1], by linarith only [hr2]⟩
     calc dist (AffineMap.lineMap (G.vertexImage (K.edgeFirst e))
             A.leftEndpoint (2 * r))
           (faceOriginalMap G f (AffineMap.lineMap (K.faceEdgeSourcePoint f i 0)
@@ -1152,23 +1149,23 @@ theorem dist_completePath_comparison_lt (G : K.PlaneGraphRealization)
       _ < rsep / 2 := by
           have : G.vertexIsolationRadius (K.edgeFirst e) ≤ rsep / 8 :=
             hiso₁.trans heta8
-          linarith
+          linarith only [this, hrsep_pos]
   · by_cases hr34 : r ≤ 3 / 4
     · -- middle range
       exact dist_completePath_comparison_lt_of_middle G f i htube hr hr2 hr34
     · -- right spoke
       push Not at hr2 hr34
       have hw : (0 : ℝ) ≤ 2 * (2 * r - 1) - 1 ∧ 2 * (2 * r - 1) - 1 ≤ 1 := by
-        constructor <;> nlinarith [hr.2]
+        constructor <;> linarith only [hr.2, hr34]
       have hcp : A.completePath ⟨r, hr⟩ =
           AffineMap.lineMap A.rightEndpoint (G.vertexImage (K.edgeSecond e))
             (2 * (2 * r - 1) - 1) := by
         rw [CentralPolygonalArc.completePath, Path.trans_apply]
-        rw [dite_eq_right (by linarith : ¬ ((⟨r, hr⟩ : unitInterval) : ℝ) ≤ 1 / 2)]
+        rw [dite_eq_right (by linarith only [hr2] : ¬ ((⟨r, hr⟩ : unitInterval) : ℝ) ≤ 1 / 2)]
         rw [Path.trans_apply]
         rw [dite_eq_right (by
           change ¬ (2 * ((⟨r, hr⟩ : unitInterval) : ℝ) - 1) ≤ 1 / 2
-          linarith)]
+          linarith only [hr34])]
         rw [Path.segment_apply]
       have hprofile : sideParamProfile G f i r =
           AffineMap.lineMap (sideTrimRight G f i) 1 (4 * r - 3) := by
@@ -1188,7 +1185,7 @@ theorem dist_completePath_comparison_lt (G : K.PlaneGraphRealization)
         exact (AffineMap.lineMap _ _).apply_lineMap _ _ _
       rw [hcp, hprofile, hsrcpt]
       have h1w : (1 : ℝ) - (2 * (2 * r - 1) - 1) ∈ Set.Icc (0 : ℝ) 1 :=
-        ⟨by linarith [hw.2], by linarith [hw.1]⟩
+        ⟨by linarith only [hw.2], by linarith only [hw.1]⟩
       calc dist (AffineMap.lineMap A.rightEndpoint
               (G.vertexImage (K.edgeSecond e)) (2 * (2 * r - 1) - 1))
             (faceOriginalMap G f (AffineMap.lineMap (K.faceEdgeSourcePoint f i 1)
@@ -1204,11 +1201,11 @@ theorem dist_completePath_comparison_lt (G : K.PlaneGraphRealization)
         _ ≤ G.vertexIsolationRadius (K.edgeSecond e) + rsep / 4 := by
             apply add_le_add
             · rw [dist_lineMap_right, Real.norm_eq_abs,
-                abs_of_nonneg (by linarith [hw.2] : (0:ℝ) ≤ 1 - (2 * (2 * r - 1) - 1))]
+                abs_of_nonneg (by linarith only [hw.2] : (0:ℝ) ≤ 1 - (2 * (2 * r - 1) - 1))]
               calc (1 - (2 * (2 * r - 1) - 1)) *
                   dist A.rightEndpoint (G.vertexImage (K.edgeSecond e)) ≤
                   1 * dist A.rightEndpoint (G.vertexImage (K.edgeSecond e)) :=
-                    mul_le_mul_of_nonneg_right (by linarith [hw.1]) dist_nonneg
+                    mul_le_mul_of_nonneg_right (by linarith only [hw.1]) dist_nonneg
                 _ = G.vertexIsolationRadius (K.edgeSecond e) := by
                     rw [one_mul]
                     exact A.rightEndpoint_on_sphere
@@ -1220,7 +1217,7 @@ theorem dist_completePath_comparison_lt (G : K.PlaneGraphRealization)
         _ < rsep / 2 := by
             have : G.vertexIsolationRadius (K.edgeSecond e) ≤ rsep / 8 :=
               hiso₂.trans heta8
-            linarith
+            linarith only [this, hrsep_pos]
 
 /-- The graph replacement on one face boundary stays within half the face separation radius of
 the facewise comparison map. -/
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/GraphPolygonalization.lean b/LeanPool/ClassificationOfSurfaces/Moise/GraphPolygonalization.lean
index d912978192..9ab51b76d4 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/GraphPolygonalization.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/GraphPolygonalization.lean
@@ -432,14 +432,14 @@ theorem radial_segments_inter {center p q : Plane} {radius : ℝ}
         rw [dist_lineMap_left, Real.norm_eq_abs, abs_of_nonneg hu.1,
           dist_comm center q, hq]
       rw [heq] at hdistU
-      nlinarith
+      exact mul_right_cancel₀ hradius.ne' (hdistT.symm.trans hdistU)
     by_cases ht0 : t = 0
     · simp [ht0]
     · exfalso
       apply hpq
       rw [AffineMap.lineMap_apply_module', AffineMap.lineMap_apply_module', htu] at heq
       have hsmul : t • (q - center) = t • (p - center) := by
-        simpa [htu] using add_right_cancel heq
+        simpa only [htu] using add_right_cancel heq
       have hpqc : p - center = q - center := by
         exact (smul_right_injective Plane ht0 hsmul).symm
       calc
@@ -458,7 +458,9 @@ theorem eq_endpoint_of_mem_radial_segment {center p x : Plane} {radius : ℝ}
   have hdist : dist (AffineMap.lineMap center p t) center = t * radius := by
     rw [dist_lineMap_left, Real.norm_eq_abs, abs_of_nonneg ht.1,
       dist_comm center p, hp]
-  have ht1 : t = 1 := by nlinarith
+  have ht1 : t = 1 := by
+    exact mul_right_cancel₀ hradius.ne'
+      (hdist.symm.trans (hxsphere.trans (one_mul radius).symm))
   simp [ht1]
 
 theorem disjoint_radial_segments_away_center {center p q : Plane} {radius : ℝ}
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/GraphRefinement.lean b/LeanPool/ClassificationOfSurfaces/Moise/GraphRefinement.lean
index 26b2181dd5..9b86596ebb 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/GraphRefinement.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/GraphRefinement.lean
@@ -6,7 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.Moise.GraphSubdivision
-import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 
 /-!
 # Finite marked refinements of plane graphs
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/HalfPlanePolygon.lean b/LeanPool/ClassificationOfSurfaces/Moise/HalfPlanePolygon.lean
index a75ad59439..e9cabc8fca 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/HalfPlanePolygon.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/HalfPlanePolygon.lean
@@ -9,10 +9,6 @@ public import LeanPool.ClassificationOfSurfaces.Moise.ChartExtraction
 public import LeanPool.ClassificationOfSurfaces.Moise.PolygonalJordan
 import LeanPool.ClassificationOfSurfaces.Moise.LineSubdivision
 import Mathlib.Analysis.Normed.Affine.AddTorsor
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Polygonal disks in a half-plane
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicCellwiseExtension.lean b/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicCellwiseExtension.lean
index d1483fc4c0..c8b7908b94 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicCellwiseExtension.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicCellwiseExtension.lean
@@ -9,7 +9,6 @@ public import LeanPool.ClassificationOfSurfaces.Moise.IntrinsicFaceFilling
 import LeanPool.ClassificationOfSurfaces.Moise.IntrinsicMidpointSubdivision
 import LeanPool.ClassificationOfSurfaces.Moise.PLApproximation
 import LeanPool.ClassificationOfSurfaces.Moise.PolygonalFamilyPolyhedron
-import Mathlib.CategoryTheory.Category.Init
 
 /-!
 # Cellwise assembly of intrinsic PL face fillings
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicCloseCellwiseExtension.lean b/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicCloseCellwiseExtension.lean
index f914336568..cf9dc7dd1b 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicCloseCellwiseExtension.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicCloseCellwiseExtension.lean
@@ -10,7 +10,6 @@ public import LeanPool.ClassificationOfSurfaces.Moise.IntrinsicCellwiseExtension
 import LeanPool.ClassificationOfSurfaces.Moise.IntrinsicFineSubdivision
 import LeanPool.ClassificationOfSurfaces.Moise.PLApproximation
 import LeanPool.ClassificationOfSurfaces.Moise.PolygonalFamilyPolyhedron
-import Mathlib.CategoryTheory.Category.Init
 
 /-!
 # Cellwise extension of a close intrinsic graph approximation
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicCloseGraphApproximation.lean b/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicCloseGraphApproximation.lean
index 9fd995e12d..9fc8a7e8c8 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicCloseGraphApproximation.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicCloseGraphApproximation.lean
@@ -6,7 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.Moise.IntrinsicGraphModel
-import Mathlib.CategoryTheory.Category.Init
 
 /-!
 # Arbitrarily close intrinsic graph approximation
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicComplex.lean b/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicComplex.lean
index 010cad2412..79f3e5c0fe 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicComplex.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicComplex.lean
@@ -45,6 +45,54 @@ namespace IntrinsicTwoComplex
 
 variable (K : IntrinsicTwoComplex)
 
+section
+
+open scoped BigOperators
+
+/-- A simplex affine combination is the coordinatewise weighted sum. -/
+theorem simplex_affineCombination_eq_weighted_sum {ι α : Type*} [Fintype ι]
+    (point : ι → α → ℝ) (x : stdSimplex ℝ ι) :
+    Finset.univ.affineCombination ℝ point x = fun v ↦ ∑ p, x p * point p v := by
+  rw [Finset.univ.affineCombination_eq_linear_combination point x x.2.2]
+  funext v
+  simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
+
+/-- Affine evaluation commutes with a simplex weighted sum. -/
+theorem affineMap_apply_weighted_sum {ι α β : Type*} [Fintype ι]
+    (a : (α → ℝ) →ᵃ[ℝ] (β → ℝ)) (point : ι → α → ℝ)
+    (x : stdSimplex ℝ ι) :
+    a (fun v ↦ ∑ p, x p * point p v) = fun v ↦ ∑ p, x p * a (point p) v := by
+  rw [← simplex_affineCombination_eq_weighted_sum point x,
+    Finset.univ.map_affineCombination point x x.2.2 a,
+    simplex_affineCombination_eq_weighted_sum (a ∘ point) x]
+  rfl
+
+/-- The affine combination map is injective when its source points are affinely independent. -/
+theorem affineCombination_injective_of_affineIndependent
+    {ι E : Type*} [Fintype ι] [AddCommGroup E] [Module ℝ E]
+    (source : ι → E) (hsource : AffineIndependent ℝ source) :
+    Function.Injective (fun x : stdSimplex ℝ ι ↦
+      Finset.univ.affineCombination ℝ source x) := by
+  intro x y hxy
+  have hweights := (hsource.affineCombination_eq_iff_eq x.2.2 y.2.2).mp hxy
+  exact Subtype.ext (funext fun i ↦ hweights i (Finset.mem_univ i))
+
+theorem simplex_eq_of_weighted_sum_eq_of_affineIndependent
+    {ι α : Type*} [Fintype ι]
+    (source : ι → α → ℝ) (hsource : AffineIndependent ℝ source)
+    {x y : stdSimplex ℝ ι}
+    (hxy : (fun v ↦ ∑ p, x p * source p v) =
+      (fun v ↦ ∑ p, y p * source p v)) :
+    x = y := by
+  apply affineCombination_injective_of_affineIndependent source hsource
+  change Finset.univ.affineCombination ℝ source x =
+    Finset.univ.affineCombination ℝ source y
+  rw [simplex_affineCombination_eq_weighted_sum source x,
+    simplex_affineCombination_eq_weighted_sum source y]
+  exact hxy
+
+end
+
 /-- The canonical barycentric realization of an intrinsic complex. -/
 abbrev realization : Type :=
   GeometricRealization K.Vertex K.faces
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicFaceFilling.lean b/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicFaceFilling.lean
index e079f53d19..38852d512b 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicFaceFilling.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicFaceFilling.lean
@@ -8,7 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.Moise.IntrinsicFaceExtension
 public import LeanPool.ClassificationOfSurfaces.Moise.FinitePLHomeomorph
 import LeanPool.ClassificationOfSurfaces.Moise.PLApproximation
-import Mathlib.CategoryTheory.Category.Init
 
 /-!
 # PL fillings of intrinsic polygonal face boundaries
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicGraphModel.lean b/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicGraphModel.lean
index 284a69e8bc..2a7bcc163f 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicGraphModel.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicGraphModel.lean
@@ -6,7 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.Moise.IntrinsicFaceBoundary
-import Mathlib.CategoryTheory.Category.Init
 
 /-!
 # A conforming plane model of an intrinsic replacement graph
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicMarkedFan.lean b/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicMarkedFan.lean
index 571b287696..7848aaa3bf 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicMarkedFan.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/IntrinsicMarkedFan.lean
@@ -1116,11 +1116,18 @@ noncomputable def fanFaceMap (f : M.FanFace) :
     intro p _
     rw [M.fanVertex_mem_faceCarrier f p.2 v hv, mul_zero]
 
+/-- Coordinates of a marked fan map without unfolding its realization certificates. -/
+theorem fanFaceMap_val (f : M.FanFace)
+    (x : stdSimplex ℝ {p // p ∈ M.fanFaceVertices f}) :
+    (M.fanFaceMap f x).1 = (fun v ↦ ∑ p, x p * p.1.1 v) := by
+  simp only [fanFaceMap]
+
 theorem fanFaceMap_mem_faceCarrier (f : M.FanFace)
     (x : stdSimplex ℝ {p // p ∈ M.fanFaceVertices f}) :
     M.fanFaceMap f x ∈ K.faceCarrier f.1.1 := by
   classical
   intro v hv
+  rw [M.fanFaceMap_val]
   change (∑ p, x p * p.1.1 v) = 0
   apply Finset.sum_eq_zero
   intro p _
@@ -1132,6 +1139,7 @@ theorem fanFaceMap_vertex (f : M.FanFace)
   classical
   apply Subtype.ext
   funext v
+  rw [M.fanFaceMap_val]
   change (∑ q, (stdSimplex.vertex p :
       stdSimplex ℝ {p // p ∈ M.fanFaceVertices f}) q * q.1.1 v) = p.1.1 v
   rw [Finset.sum_eq_single p]
@@ -1220,27 +1228,12 @@ theorem affineIndependent_fanVertex_val (f : M.FanFace) :
 
 theorem fanFaceMap_injective (f : M.FanFace) :
     Function.Injective (M.fanFaceMap f) := by
-  classical
   intro x y hxy
-  have hval : (M.fanFaceMap f x).1 = (M.fanFaceMap f y).1 :=
-    congrArg Subtype.val hxy
-  change (fun v ↦ ∑ p, x p * p.1.1 v) =
-    (fun v ↦ ∑ p, y p * p.1.1 v) at hval
-  let source :=
-    fun p : {p // p ∈ M.fanFaceVertices f} ↦ p.1.1
-  have hcomb : Finset.univ.affineCombination ℝ source x =
-      Finset.univ.affineCombination ℝ source y := by
-    rw [Finset.univ.affineCombination_eq_linear_combination source x x.2.2,
-      Finset.univ.affineCombination_eq_linear_combination source y y.2.2]
-    funext v
-    simpa only [source, Finset.sum_apply, Pi.smul_apply, smul_eq_mul] using
-      congrFun hval v
-  have hweights :=
-    ((M.affineIndependent_fanVertex_val f).affineCombination_eq_iff_eq
-      x.2.2 y.2.2).mp hcomb
-  apply Subtype.ext
-  funext p
-  exact hweights p (Finset.mem_univ p)
+  apply simplex_eq_of_weighted_sum_eq_of_affineIndependent
+    (fun p : {p // p ∈ M.fanFaceVertices f} ↦ p.1.1)
+    (M.affineIndependent_fanVertex_val f)
+  exact (M.fanFaceMap_val f x).symm.trans
+    ((congrArg Subtype.val hxy).trans (M.fanFaceMap_val f y))
 
 theorem continuous_fanFaceMap (f : M.FanFace) :
     Continuous (M.fanFaceMap f) := by
@@ -1343,7 +1336,7 @@ theorem fanFaceMap_simplexLineMap (f : M.FanFace)
         (M.fanFaceMap f y).1 r.1 := by
   classical
   funext v
-  simp only [fanFaceMap, fanSimplexLineMap,
+  simp only [fanFaceMap_val, fanSimplexLineMap,
     AffineMap.lineMap_apply_module, Pi.add_apply, Pi.smul_apply, smul_eq_mul]
   change (∑ p, (((1 - r.1) • x.1 + r.1 • y.1) p) * p.1.1 v) =
     (1 - r.1) * ∑ p, x p * p.1.1 v +
@@ -1396,6 +1389,7 @@ theorem fanFaceMap_mem_baseEdge_of_center_eq_zero
       (M.edgeIntervalSecond_mem_edgeMarks
         (K.faceEdge f.1 f.2.1) f.2.2)).2
   intro v hv
+  rw [M.fanFaceMap_val]
   change (∑ z, x z * z.1.1 v) = 0
   rw [M.fanVertex_univ f, Finset.sum_insert hcNot,
     Finset.sum_insert hpNot, Finset.sum_singleton]
@@ -1441,6 +1435,7 @@ theorem edgeParameterValue_fanFaceMap_of_center_eq_zero
     M.fanFaceMap_mem_baseEdge_of_center_eq_zero f x hxCenter
   rw [M.edgeParameterValue_eq e hmapEdge,
     K.edgeParameter_eq_secondCoordinate]
+  rw [M.fanFaceMap_val]
   change (∑ z, x z * z.1.1 (K.edgeSecond e)) =
     x p * M.edgeParameterValue e p.1 +
       x q * M.edgeParameterValue e q.1
@@ -1742,10 +1737,12 @@ theorem fanFaceMap_eq_lineMap_normalizedBase (f : M.FanFace)
   have hpNot : p ∉ ({q} : Finset _) := by
     simp [p, q, M.fanFirstVertex_ne_second f]
   funext v
+  rw [M.fanFaceMap_val]
   change (∑ r, x r * r.1.1 v) = _
   rw [M.fanVertex_univ f, Finset.sum_insert hcNot,
     Finset.sum_insert hpNot, Finset.sum_singleton,
     AffineMap.lineMap_apply_module]
+  rw [M.fanFaceMap_val]
   change x c * c.1.1 v + (x p * p.1.1 v + x q * q.1.1 v) =
     (1 - d) * (K.faceCenter f.1).1 v +
       d * (∑ r, M.fanNormalizedBasePoint f x hxCenter r * r.1.1 v)
@@ -1772,6 +1769,7 @@ theorem fanFaceMap_opposite (f : M.FanFace)
   classical
   let c := M.fanCenterVertex f
   let opposite := K.faceVertex f.1 (f.2.1 + 2)
+  rw [M.fanFaceMap_val]
   change (∑ p, x p * p.1.1 opposite) = x c / 3
   rw [Finset.sum_eq_single c]
   · have hc : c.1.1 opposite = 1 / 3 := by
@@ -1840,6 +1838,7 @@ theorem fanFaceMap_faceVertex_lower_bound (f : M.FanFace)
     Finset.single_le_sum
       (fun p _ ↦ mul_nonneg (x.2.1 p) (p.1.2.1.1 _))
       (Finset.mem_univ c)
+  rw [M.fanFaceMap_val]
   change x c / 3 ≤
     ∑ p, x p * p.1.1 (K.faceVertex f.1 i)
   rw [hcValue] at hterm
@@ -2946,6 +2945,8 @@ theorem globalFanFaceMap_val_eq_fanBarycentricAffine
         (extendFaceCoordinates (M.globalFanFaceVertices f) x) := by
   classical
   funext k
+  change (M.fanFaceMap f (M.fanRelabelSimplex f x)).1 k = _
+  rw [M.fanFaceMap_val]
   change (∑ p : {p // p ∈ M.fanFaceVertices f},
       M.fanRelabelSimplex f x p * p.1.1 k) =
     M.fanBarycentricAffine
@@ -2998,6 +2999,7 @@ theorem fanFaceMap_eq_of_extendedCoordinates_eq
     M.fanFaceMap f x = M.fanFaceMap g y := by
   apply Subtype.ext
   funext v
+  rw [M.fanFaceMap_val, M.fanFaceMap_val]
   change (∑ p, x p * p.1.1 v) = ∑ p, y p * p.1.1 v
   exact sum_extendFaceCoordinates_eq_of_eq x y hxy (fun p ↦ p.1 v)
 
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/LineSubdivision.lean b/LeanPool/ClassificationOfSurfaces/Moise/LineSubdivision.lean
index ca9309822b..2c8d3c5e21 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/LineSubdivision.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/LineSubdivision.lean
@@ -2415,75 +2415,75 @@ theorem localRefinementTriangles_monochromatic (t : M.Triangle) :
   split_ifs with h01 h02 h12 h02' h12' h12''
   · rcases signs_of_two_crossings h01 h02 with h | h
     · apply M.strictPattern_monochromatic_positive
-      · simpa using h.1.le
-      · simpa using h.2.1.le
-      · simpa using h.2.2.le
-      · simpa using M.localCutVertex_apply_eq_zero f t 0 1 h01
-      · simpa using M.localCutVertex_apply_eq_zero f t 0 2 h02
+      · exact h.1.le
+      · exact h.2.1.le
+      · exact h.2.2.le
+      · exact M.localCutVertex_apply_eq_zero f t 0 1 h01
+      · exact M.localCutVertex_apply_eq_zero f t 0 2 h02
     · apply M.strictPattern_monochromatic_negative
-      · simpa using h.1.le
-      · simpa using h.2.1.le
-      · simpa using h.2.2.le
-      · simpa using M.localCutVertex_apply_eq_zero f t 0 1 h01
-      · simpa using M.localCutVertex_apply_eq_zero f t 0 2 h02
+      · exact h.1.le
+      · exact h.2.1.le
+      · exact h.2.2.le
+      · exact M.localCutVertex_apply_eq_zero f t 0 1 h01
+      · exact M.localCutVertex_apply_eq_zero f t 0 2 h02
   · have h10 : f (M.position (M.orderedVertex t 1)) *
         f (M.position (M.orderedVertex t 0)) < 0 := by simpa [mul_comm] using h01
     rcases signs_of_two_crossings h10 h12 with h | h
     · apply M.strictPattern_monochromatic_positive
-      · simpa using h.1.le
-      · simpa using h.2.1.le
-      · simpa using h.2.2.le
-      · simpa using M.localCutVertex_apply_eq_zero f t 0 1 h01
-      · simpa using M.localCutVertex_apply_eq_zero f t 1 2 h12
+      · exact h.1.le
+      · exact h.2.1.le
+      · exact h.2.2.le
+      · exact M.localCutVertex_apply_eq_zero f t 0 1 h01
+      · exact M.localCutVertex_apply_eq_zero f t 1 2 h12
     · apply M.strictPattern_monochromatic_negative
-      · simpa using h.1.le
-      · simpa using h.2.1.le
-      · simpa using h.2.2.le
-      · simpa using M.localCutVertex_apply_eq_zero f t 0 1 h01
-      · simpa using M.localCutVertex_apply_eq_zero f t 1 2 h12
+      · exact h.1.le
+      · exact h.2.1.le
+      · exact h.2.2.le
+      · exact M.localCutVertex_apply_eq_zero f t 0 1 h01
+      · exact M.localCutVertex_apply_eq_zero f t 1 2 h12
   · have hz := third_eq_zero_of_one_crossing h01 h02 h12
     rcases mul_neg_iff.mp h01 with h | h
     · apply M.edgePattern_monochromatic_positive
-      · simpa using h.1.le
-      · simpa using h.2.le
-      · simpa using hz
-      · simpa using M.localCutVertex_apply_eq_zero f t 0 1 h01
+      · exact h.1.le
+      · exact h.2.le
+      · exact hz
+      · exact M.localCutVertex_apply_eq_zero f t 0 1 h01
     · apply M.edgePattern_monochromatic_negative
-      · simpa using h.1.le
-      · simpa using h.2.le
-      · simpa using hz
-      · simpa using M.localCutVertex_apply_eq_zero f t 0 1 h01
+      · exact h.1.le
+      · exact h.2.le
+      · exact hz
+      · exact M.localCutVertex_apply_eq_zero f t 0 1 h01
   · have h20 : f (M.position (M.orderedVertex t 2)) *
         f (M.position (M.orderedVertex t 0)) < 0 := by simpa [mul_comm] using h02'
     have h21 : f (M.position (M.orderedVertex t 2)) *
         f (M.position (M.orderedVertex t 1)) < 0 := by simpa [mul_comm] using h12'
     rcases signs_of_two_crossings h20 h21 with h | h
     · apply M.strictPattern_monochromatic_positive
-      · simpa using h.1.le
-      · simpa using h.2.1.le
-      · simpa using h.2.2.le
-      · simpa using M.localCutVertex_apply_eq_zero f t 0 2 h02'
-      · simpa using M.localCutVertex_apply_eq_zero f t 1 2 h12'
+      · exact h.1.le
+      · exact h.2.1.le
+      · exact h.2.2.le
+      · exact M.localCutVertex_apply_eq_zero f t 0 2 h02'
+      · exact M.localCutVertex_apply_eq_zero f t 1 2 h12'
     · apply M.strictPattern_monochromatic_negative
-      · simpa using h.1.le
-      · simpa using h.2.1.le
-      · simpa using h.2.2.le
-      · simpa using M.localCutVertex_apply_eq_zero f t 0 2 h02'
-      · simpa using M.localCutVertex_apply_eq_zero f t 1 2 h12'
+      · exact h.1.le
+      · exact h.2.1.le
+      · exact h.2.2.le
+      · exact M.localCutVertex_apply_eq_zero f t 0 2 h02'
+      · exact M.localCutVertex_apply_eq_zero f t 1 2 h12'
   · have h21 : ¬ f (M.position (M.orderedVertex t 2)) *
         f (M.position (M.orderedVertex t 1)) < 0 := by simpa [mul_comm] using h12'
     have hz := third_eq_zero_of_one_crossing h02' h01 h21
     rcases mul_neg_iff.mp h02' with h | h
     · apply M.edgePattern_monochromatic_positive
-      · simpa using h.1.le
-      · simpa using h.2.le
-      · simpa using hz
-      · simpa using M.localCutVertex_apply_eq_zero f t 0 2 h02'
+      · exact h.1.le
+      · exact h.2.le
+      · exact hz
+      · exact M.localCutVertex_apply_eq_zero f t 0 2 h02'
     · apply M.edgePattern_monochromatic_negative
-      · simpa using h.1.le
-      · simpa using h.2.le
-      · simpa using hz
-      · simpa using M.localCutVertex_apply_eq_zero f t 0 2 h02'
+      · exact h.1.le
+      · exact h.2.le
+      · exact hz
+      · exact M.localCutVertex_apply_eq_zero f t 0 2 h02'
   · have h21 : f (M.position (M.orderedVertex t 2)) *
         f (M.position (M.orderedVertex t 1)) < 0 := by simpa [mul_comm] using h12''
     have h10 : ¬ f (M.position (M.orderedVertex t 1)) *
@@ -2493,15 +2493,15 @@ theorem localRefinementTriangles_monochromatic (t : M.Triangle) :
     have hz := third_eq_zero_of_one_crossing h12'' h10 h20
     rcases mul_neg_iff.mp h12'' with h | h
     · apply M.edgePattern_monochromatic_positive
-      · simpa using h.1.le
-      · simpa using h.2.le
-      · simpa using hz
-      · simpa using M.localCutVertex_apply_eq_zero f t 1 2 h12''
+      · exact h.1.le
+      · exact h.2.le
+      · exact hz
+      · exact M.localCutVertex_apply_eq_zero f t 1 2 h12''
     · apply M.edgePattern_monochromatic_negative
-      · simpa using h.1.le
-      · simpa using h.2.le
-      · simpa using hz
-      · simpa using M.localCutVertex_apply_eq_zero f t 1 2 h12''
+      · exact h.1.le
+      · exact h.2.le
+      · exact hz
+      · exact M.localCutVertex_apply_eq_zero f t 1 2 h12''
   · have hsign := same_closed_side_of_pairwise_products
         (not_lt.mp h01) (not_lt.mp h02') (not_lt.mp h12'')
     intro s hs
@@ -2512,16 +2512,16 @@ theorem localRefinementTriangles_monochromatic (t : M.Triangle) :
       intro x hx
       simp only [Finset.mem_insert, Finset.mem_singleton] at hx
       rcases hx with rfl | rfl | rfl
-      · simpa using h.1
-      · simpa using h.2.1
-      · simpa using h.2.2
+      · exact h.1
+      · exact h.2.1
+      · exact h.2.2
     · right
       intro x hx
       simp only [Finset.mem_insert, Finset.mem_singleton] at hx
       rcases hx with rfl | rfl | rfl
-      · simpa using h.1
-      · simpa using h.2.1
-      · simpa using h.2.2
+      · exact h.1
+      · exact h.2.1
+      · exact h.2.2
 
 /-- View a mesh whose vertex type is identified with the refined vertex pool as a family of
 triangles on that fixed pool. -/
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteCellwiseExtension.lean b/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteCellwiseExtension.lean
index 84ed5723b8..299cc79a98 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteCellwiseExtension.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteCellwiseExtension.lean
@@ -6,7 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.Moise.LocallyFiniteFaceFilling
-import Mathlib.CategoryTheory.Category.Init
 
 /-!
 # Cellwise assembly for locally finite PL face fillings
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteControlledApproximation.lean b/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteControlledApproximation.lean
index 8929c8abf1..79383310a5 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteControlledApproximation.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteControlledApproximation.lean
@@ -9,9 +9,6 @@ public import LeanPool.ClassificationOfSurfaces.Moise.ChartExtraction
 public import LeanPool.ClassificationOfSurfaces.Moise.LocallyFinitePLApproximation
 import LeanPool.ClassificationOfSurfaces.Moise.HalfPlanePolygon
 import LeanPool.ClassificationOfSurfaces.Moise.LocallyFiniteSidePreservation
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Controlled locally finite PL replacement
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteFaceExtension.lean b/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteFaceExtension.lean
index 31b1d0b994..d31d87811f 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteFaceExtension.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteFaceExtension.lean
@@ -8,7 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.Moise.LocallyFiniteFaceModel
 public import LeanPool.ClassificationOfSurfaces.Moise.IntrinsicFaceExtension
 public import LeanPool.ClassificationOfSurfaces.Moise.LocallyFiniteFaceBoundary
-import Mathlib.CategoryTheory.Category.Init
 
 /-!
 # Coherent polygonal boundary maps for locally finite faces
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteFaceFilling.lean b/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteFaceFilling.lean
index 709ffc0f07..1d7c00af67 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteFaceFilling.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteFaceFilling.lean
@@ -8,7 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.Moise.LocallyFiniteFaceExtension
 public import LeanPool.ClassificationOfSurfaces.Moise.FinitePLHomeomorph
 import LeanPool.ClassificationOfSurfaces.Moise.PLApproximation
-import Mathlib.CategoryTheory.Category.Init
 
 /-!
 # PL fillings of locally finite polygonal face boundaries
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteFaceModel.lean b/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteFaceModel.lean
index e0c53fac43..c2d4c39d9b 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteFaceModel.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteFaceModel.lean
@@ -7,7 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.Moise.IntrinsicFaceModel
 public import LeanPool.ClassificationOfSurfaces.Moise.LocallyFiniteTriangulation
-import Mathlib.Combinatorics.SimpleGraph.Init
 
 /-!
 # Standard plane models for locally finite faces
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/LocallyFinitePLApproximation.lean b/LeanPool/ClassificationOfSurfaces/Moise/LocallyFinitePLApproximation.lean
index 956b4f5ae1..583cc677f0 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/LocallyFinitePLApproximation.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/LocallyFinitePLApproximation.lean
@@ -7,7 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.Moise.LocallyFiniteCellwiseExtension
 import LeanPool.ClassificationOfSurfaces.Moise.PLApproximation
-import Mathlib.CategoryTheory.Category.Init
 
 /-!
 # Quantitative locally finite PL approximation
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteSidePreservation.lean b/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteSidePreservation.lean
index 9ef6a6ca95..002755e494 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteSidePreservation.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteSidePreservation.lean
@@ -7,7 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.Moise.LocallyFinitePLApproximation
 import LeanPool.ClassificationOfSurfaces.Moise.PLApproximation
-import Mathlib.CategoryTheory.Category.Init
 
 /-!
 # Side preservation for locally finite face fillings
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/NoRetraction.lean b/LeanPool/ClassificationOfSurfaces/Moise/NoRetraction.lean
index 708ed62ebb..87cff616fb 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/NoRetraction.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/NoRetraction.lean
@@ -86,15 +86,10 @@ theorem no_retraction_closedUnitDisk :
       simpa [γ] using h
     rw [hΓ0, one_mul]
   have hΓ0 : Γ 0 = Λ 0 := by simp [Λ]
-  have hΓeq : Γ = Circle.isCoveringMap_exp.liftPath γ (Γ 0) (by
-      simpa using (congrFun hΓlift 0).symm) :=
-    (Circle.isCoveringMap_exp.eq_liftPath_iff' (by
-      simpa using (congrFun hΓlift 0).symm)).mpr ⟨hΓlift, rfl⟩
-  have hΛeq : Λ = Circle.isCoveringMap_exp.liftPath γ (Γ 0) (by
-      simpa using (congrFun hΓlift 0).symm) :=
-    (Circle.isCoveringMap_exp.eq_liftPath_iff' (by
-      simpa using (congrFun hΓlift 0).symm)).mpr ⟨hΛlift, hΓ0.symm⟩
-  have hend : Γ 1 = Λ 1 := by rw [hΓeq, hΛeq]
+  have hΓΛ : (Γ : I → ℝ) = Λ :=
+    Circle.isCoveringMap_exp.eq_of_comp_eq Γ.continuous Λ.continuous
+      (hΓlift.trans hΛlift.symm) 0 hΓ0
+  have hend : Γ 1 = Λ 1 := congrFun hΓΛ 1
   have hloop : Γ 1 = Γ 0 := by
     change F (circleToClosedUnitDisk (γ 1)) = F (circleToClosedUnitDisk (γ 0))
     congr 2
@@ -103,8 +98,7 @@ theorem no_retraction_closedUnitDisk :
   rw [hloop] at hend
   have hend' : Γ 0 = Γ 0 + 2 * Real.pi := by simp [Λ] at hend
   have hpi : (2 : ℝ) * Real.pi ≠ 0 := mul_ne_zero (by norm_num) Real.pi_ne_zero
-  apply hpi
-  linarith
+  exact hpi (add_eq_left.mp hend'.symm)
 
 /-- The Euclidean plane and the complex plane are linearly isometric, using the orthonormal
 basis `(1, I)` of `ℂ` over `ℝ`. -/
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/PLApproximation.lean b/LeanPool/ClassificationOfSurfaces/Moise/PLApproximation.lean
index 2271de60d6..42e2ffa7b0 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/PLApproximation.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/PLApproximation.lean
@@ -13,7 +13,6 @@ import LeanPool.ClassificationOfSurfaces.Moise.FineSubdivision
 import LeanPool.ClassificationOfSurfaces.Moise.NoRetraction
 import LeanPool.ClassificationOfSurfaces.Moise.PolygonalSchoenflies
 import Mathlib.Analysis.Complex.Tietze
-import Mathlib.CategoryTheory.Category.Init
 
 /-!
 # PL approximation of homeomorphisms
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/PlaneComplex.lean b/LeanPool/ClassificationOfSurfaces/Moise/PlaneComplex.lean
index ad13e238d9..48581a629d 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/PlaneComplex.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/PlaneComplex.lean
@@ -169,22 +169,17 @@ theorem endpoint_not_mem_openSegment_of_mem_segment {a b x y : Plane}
       _ = AffineMap.lineMap (k := ℝ) (AffineMap.lineMap (k := ℝ) a b s)
           (AffineMap.lineMap (k := ℝ) a b t) u := huEq.symm
       _ = AffineMap.lineMap (k := ℝ) a b c := by
-        ext i
-        simp [c, AffineMap.lineMap_apply_module]
-        ring
+        simpa only [c, AffineMap.lineMap_apply_ring] using
+          ((AffineMap.lineMap a b).apply_lineMap s t u).symm
   have hc : c = 0 := by
     exact (AffineMap.lineMap_injective ℝ hab hmaps).symm
   have hcoeff : 0 < 1 - u := sub_pos.mpr hu.2
   have htermS : 0 ≤ (1 - u) * s := mul_nonneg hcoeff.le hs.1
   have htermT : 0 ≤ u * t := mul_nonneg hu.1.le ht.1
-  have htermS0 : (1 - u) * s = 0 := by
-    dsimp [c] at hc
-    nlinarith
-  have htermT0 : u * t = 0 := by
-    dsimp [c] at hc
-    nlinarith
-  have hs0 : s = 0 := (mul_eq_zero.mp htermS0).resolve_left hcoeff.ne'
-  have ht0 : t = 0 := (mul_eq_zero.mp htermT0).resolve_left hu.1.ne'
+  have hterms : (1 - u) * s = 0 ∧ u * t = 0 :=
+    (add_eq_zero_iff_of_nonneg htermS htermT).mp hc
+  have hs0 : s = 0 := (mul_eq_zero.mp hterms.1).resolve_left hcoeff.ne'
+  have ht0 : t = 0 := (mul_eq_zero.mp hterms.2).resolve_left hu.1.ne'
   apply hxy
   rw [hs0, ht0]
 
@@ -206,9 +201,8 @@ theorem segment_subset_of_midpoint_mem_openSegment
       AffineMap.lineMap A B u =
         AffineMap.lineMap P Q ((1 - u) * a + u * b) := by
     rw [← ha, ← hb]
-    ext k
-    simp [AffineMap.lineMap_apply_module]
-    ring
+    simpa only [AffineMap.lineMap_apply_ring] using
+      ((AffineMap.lineMap P Q).apply_lineMap a b u).symm
   have hparam : (1 - u) * a + u * b = 1 / 2 := by
     apply AffineMap.lineMap_injective ℝ hPQ
     rw [← hcompose]
@@ -234,7 +228,7 @@ theorem segment_subset_of_midpoint_mem_openSegment
       have hright : u * b ≤ 0 := mul_nonpos_of_nonneg_of_nonpos hu.1.le hb0
       exfalso
       norm_num at hparam
-      linarith
+      linarith only [hleft, hright, hparam]
     · exact Or.inl ⟨ha0, hb1⟩
     · exact Or.inr ⟨hb0, ha1⟩
     · have hleft : 0 ≤ (1 - u) * (a - 1) :=
@@ -243,8 +237,10 @@ theorem segment_subset_of_midpoint_mem_openSegment
         mul_nonneg hu.1.le (sub_nonneg.mpr hb1)
       exfalso
       norm_num at hparam
-      nlinarith only [hleft, hright, hparam]
-  have endpoints_mem (h : a ≤ 0 ∧ 1 ≤ b) :
+      linarith only [hleft, hright, hparam]
+  have endpoints_mem (a b : ℝ) (A B : Plane)
+      (ha : AffineMap.lineMap P Q a = A) (hb : AffineMap.lineMap P Q b = B)
+      (h : a ≤ 0 ∧ 1 ≤ b) :
       P ∈ segment ℝ A B ∧ Q ∈ segment ℝ A B := by
     have hab : a ≤ b := (h.1.trans (by norm_num : (0 : ℝ) ≤ 1)).trans h.2
     have hpScalar : Wbtw ℝ a 0 b :=
@@ -255,21 +251,10 @@ theorem segment_subset_of_midpoint_mem_openSegment
     have hq := hqScalar.map (AffineMap.lineMap P Q)
     rw [ha, hb] at hp hq
     simpa using And.intro hp.mem_segment hq.mem_segment
-  have endpoints_mem_rev (h : b ≤ 0 ∧ 1 ≤ a) :
-      P ∈ segment ℝ B A ∧ Q ∈ segment ℝ B A := by
-    have hba : b ≤ a := (h.1.trans (by norm_num : (0 : ℝ) ≤ 1)).trans h.2
-    have hpScalar : Wbtw ℝ b 0 a :=
-      (wbtw_iff_of_le hba).mpr ⟨h.1, (by norm_num : (0 : ℝ) ≤ 1).trans h.2⟩
-    have hqScalar : Wbtw ℝ b 1 a :=
-      (wbtw_iff_of_le hba).mpr ⟨h.1.trans (by norm_num), h.2⟩
-    have hp := hpScalar.map (AffineMap.lineMap P Q)
-    have hq := hqScalar.map (AffineMap.lineMap P Q)
-    rw [ha, hb] at hp hq
-    simpa using And.intro hp.mem_segment hq.mem_segment
   rcases hbracket with hab | hba
-  · obtain ⟨hp, hq⟩ := endpoints_mem hab
+  · obtain ⟨hp, hq⟩ := endpoints_mem a b A B ha hb hab
     exact (convex_segment A B).segment_subset hp hq
-  · obtain ⟨hp, hq⟩ := endpoints_mem_rev hba
+  · obtain ⟨hp, hq⟩ := endpoints_mem b a B A hb ha hba
     rw [segment_symm] at hp hq
     exact (convex_segment A B).segment_subset hp hq
 
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/PolygonalArc.lean b/LeanPool/ClassificationOfSurfaces/Moise/PolygonalArc.lean
index f60091694a..f7406f4aa1 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/PolygonalArc.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/PolygonalArc.lean
@@ -8,7 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.Moise.BrokenLine
 public import LeanPool.ClassificationOfSurfaces.Moise.PolygonalPolyhedron
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
-import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 
 /-!
 # Polygonal arcs from broken lines
@@ -928,34 +927,34 @@ theorem exists_face_on_segment (i : Fin B.n) {x : Plane}
               have hxlo : 0 < verticalLine a x := by
                 change 0 < x 0 - a 0
                 rw [hxcoord0]
-                nlinarith [ht.1, ht.2]
+                nlinarith only [ht.1, ht.2, hlt]
               have hxhi : verticalLine b x < 0 := by
                 change x 0 - b 0 < 0
                 rw [hxcoord0]
-                nlinarith [ht.1, ht.2]
+                nlinarith only [ht.1, ht.2, hlt]
               have hlo := M.nonneg_on_face_of_monochromatic_of_pos
                 (B.arrangementMesh_monochromatic_verticalLine i.castSucc) hs hxs hxlo v hv
               have hhi := M.nonpos_on_face_of_monochromatic_of_neg
                 (B.arrangementMesh_monochromatic_verticalLine i.succ) hs hxs hxhi v hv
               change 0 ≤ M.toPlaneComplex.position v 0 - a 0 at hlo
               change M.toPlaneComplex.position v 0 - b 0 ≤ 0 at hhi
-              constructor <;> linarith
+              constructor <;> linarith only [hlo, hhi]
             · rw [Set.uIcc_of_ge hgt.le, Set.mem_Icc]
               have hxhi : verticalLine a x < 0 := by
                 change x 0 - a 0 < 0
                 rw [hxcoord0]
-                nlinarith [ht.1, ht.2]
+                nlinarith only [ht.1, ht.2, hgt]
               have hxlo : 0 < verticalLine b x := by
                 change 0 < x 0 - b 0
                 rw [hxcoord0]
-                nlinarith [ht.1, ht.2]
+                nlinarith only [ht.1, ht.2, hgt]
               have hhi := M.nonpos_on_face_of_monochromatic_of_neg
                 (B.arrangementMesh_monochromatic_verticalLine i.castSucc) hs hxs hxhi v hv
               have hlo := M.nonneg_on_face_of_monochromatic_of_pos
                 (B.arrangementMesh_monochromatic_verticalLine i.succ) hs hxs hxlo v hv
               change M.toPlaneComplex.position v 0 - a 0 ≤ 0 at hhi
               change 0 ≤ M.toPlaneComplex.position v 0 - b 0 at hlo
-              constructor <;> linarith
+              constructor <;> linarith only [hlo, hhi]
         · by_cases h1 : a 1 = b 1
           · rw [h1, Set.uIcc_self]
             have h0 : a 0 ≠ b 0 := by
@@ -972,7 +971,7 @@ theorem exists_face_on_segment (i : Fin B.n) {x : Plane}
               rw [h1] at hvline
               ring_nf at hvline ⊢
               rw [h1]
-              linarith
+              linarith only [hvline]
             calc
               M.toPlaneComplex.position v 1 = a 1 := sub_eq_zero.mp
                 ((mul_eq_zero.mp hprod).resolve_left (sub_ne_zero.mpr h0.symm))
@@ -982,34 +981,34 @@ theorem exists_face_on_segment (i : Fin B.n) {x : Plane}
               have hxlo : 0 < horizontalLine a x := by
                 change 0 < x 1 - a 1
                 rw [hxcoord1]
-                nlinarith [ht.1, ht.2]
+                nlinarith only [ht.1, ht.2, hlt]
               have hxhi : horizontalLine b x < 0 := by
                 change x 1 - b 1 < 0
                 rw [hxcoord1]
-                nlinarith [ht.1, ht.2]
+                nlinarith only [ht.1, ht.2, hlt]
               have hlo := M.nonneg_on_face_of_monochromatic_of_pos
                 (B.arrangementMesh_monochromatic_horizontalLine i.castSucc) hs hxs hxlo v hv
               have hhi := M.nonpos_on_face_of_monochromatic_of_neg
                 (B.arrangementMesh_monochromatic_horizontalLine i.succ) hs hxs hxhi v hv
               change 0 ≤ M.toPlaneComplex.position v 1 - a 1 at hlo
               change M.toPlaneComplex.position v 1 - b 1 ≤ 0 at hhi
-              constructor <;> linarith
+              constructor <;> linarith only [hlo, hhi]
             · rw [Set.uIcc_of_ge hgt.le, Set.mem_Icc]
               have hxhi : horizontalLine a x < 0 := by
                 change x 1 - a 1 < 0
                 rw [hxcoord1]
-                nlinarith [ht.1, ht.2]
+                nlinarith only [ht.1, ht.2, hgt]
               have hxlo : 0 < horizontalLine b x := by
                 change 0 < x 1 - b 1
                 rw [hxcoord1]
-                nlinarith [ht.1, ht.2]
+                nlinarith only [ht.1, ht.2, hgt]
               have hhi := M.nonpos_on_face_of_monochromatic_of_neg
                 (B.arrangementMesh_monochromatic_horizontalLine i.castSucc) hs hxs hxhi v hv
               have hlo := M.nonneg_on_face_of_monochromatic_of_pos
                 (B.arrangementMesh_monochromatic_horizontalLine i.succ) hs hxs hxlo v hv
               change M.toPlaneComplex.position v 1 - a 1 ≤ 0 at hhi
               change 0 ≤ M.toPlaneComplex.position v 1 - b 1 at hlo
-              constructor <;> linarith
+              constructor <;> linarith only [hlo, hhi]
 
 /-- The common arrangement of a finite segment family resolves each requested member into faces
 contained in that member.  Keeping this theorem abstract in the family index prevents clients
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/PuncturedSurface.lean b/LeanPool/ClassificationOfSurfaces/Moise/PuncturedSurface.lean
index 57b1fde891..17d9ce5ff4 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/PuncturedSurface.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/PuncturedSurface.lean
@@ -9,9 +9,6 @@ public import LeanPool.ClassificationOfSurfaces.Moise.ChartExtraction
 public import LeanPool.ClassificationOfSurfaces.Moise.BoundaryInvariant
 import Mathlib.Analysis.Normed.Module.Ball.Homeomorph
 import Mathlib.Analysis.Normed.Module.Connected
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Punctured surface charts
diff --git a/LeanPool/ClassificationOfSurfaces/Moise/ThinKiteMove.lean b/LeanPool/ClassificationOfSurfaces/Moise/ThinKiteMove.lean
index 7096cf0efb..c48706d2d3 100644
--- a/LeanPool/ClassificationOfSurfaces/Moise/ThinKiteMove.lean
+++ b/LeanPool/ClassificationOfSurfaces/Moise/ThinKiteMove.lean
@@ -209,7 +209,7 @@ theorem thinKitePatch_subset_leftCone {δ : ℝ} (hδ : 0 ≤ δ) {p : Plane}
   have hs : thinKiteScale δ = (1 + 2 * δ) / 4 := rfl
   constructor
   · simp only [thinKiteMap, planePoint_apply_zero]
-    linarith
+    linarith only [hLL, hUL]
   · constructor
     · simp only [thinKiteMap, planePoint_apply_zero, planePoint_apply_one]
       rw [hs]
@@ -308,7 +308,7 @@ theorem exists_leftBase_openSegment_mem_kiteTriangle {q : Plane}
       · have htd : t * (dx + dy) < 1 := by
           dsimp [t]
           field_simp
-          nlinarith
+          linarith only []
         linarith
       · nlinarith [mul_nonneg ht.le (sub_nonneg.mpr hyx)]
       · exact mul_nonneg ht.le hy0
@@ -360,7 +360,7 @@ theorem exists_rightBase_openSegment_mem_kiteTriangle {q : Plane}
       · have htd : t * (dx + dy) < 1 := by
           dsimp [t]
           field_simp
-          nlinarith
+          linarith only []
         linarith
       · exact mul_nonneg ht.le hy0
     · simp [w]
@@ -410,6 +410,20 @@ theorem rightBase_direction_outside_kiteTriangle {q : Plane}
   have hpRight := havoid ⟨hpSegment.1, hpTriangle⟩
   exact hpSegment.2 (by simpa using hpRight)
 
+/-- The left base vertex is fixed by every thin-kite transport. -/
+private theorem thinKitePatch_leftBase_mem (δ : ℝ) :
+    planePoint (-1) 0 ∈ thinKitePatch δ := by
+  exact ⟨planePoint (-1) 0, Or.inl <|
+    subset_convexHull ℝ _ ⟨2, rfl⟩, by
+      simp [thinKiteMap, planePoint]⟩
+
+/-- The right base vertex is fixed by every thin-kite transport. -/
+private theorem thinKitePatch_rightBase_mem (δ : ℝ) :
+    planePoint 1 0 ∈ thinKitePatch δ := by
+  exact ⟨planePoint 1 0, Or.inr <|
+    subset_convexHull ℝ _ ⟨2, rfl⟩, by
+      simp [thinKiteMap, planePoint]⟩
+
 /-- A segment leaving the left base vertex outside the triangle misses every sufficiently thin
 kite except at that vertex. -/
 theorem exists_thinKitePatch_inter_leftSegment_eq_singleton {q : Plane}
@@ -423,7 +437,7 @@ theorem exists_thinKitePatch_inter_leftSegment_eq_singleton {q : Plane}
     apply Set.Subset.antisymm
     · rintro p ⟨hpPatch, hpSegment⟩
       by_cases hpLeft : p = planePoint (-1) 0
-      · simp [hpLeft]
+      · simp only [hpLeft, Set.mem_singleton_iff]
       rw [segment_eq_image_lineMap] at hpSegment
       obtain ⟨t, ht, rfl⟩ := hpSegment
       have htne : t ≠ 0 := by
@@ -434,30 +448,30 @@ theorem exists_thinKitePatch_inter_leftSegment_eq_singleton {q : Plane}
       have hcone := thinKitePatch_subset_leftCone hδ.le hpPatch
       have hcoord0 :
           (AffineMap.lineMap (planePoint (-1) 0) q t) 0 + 1 = t * (q 0 + 1) := by
-        simp [AffineMap.lineMap_apply_module, planePoint]
+        simp only [AffineMap.lineMap_apply_module, PiLp.add_apply,
+          PiLp.smul_apply, planePoint_apply_zero, smul_eq_mul]
         ring
       have hdx0 : q 0 + 1 = 0 := by
         rw [hcoord0] at hcone
-        nlinarith
+        nlinarith only [htpos, hx, hcone.1]
       have hcoord1 :
           (AffineMap.lineMap (planePoint (-1) 0) q t) 1 = t * q 1 := by
-        simp [AffineMap.lineMap_apply_module, planePoint]
+        simp only [AffineMap.lineMap_apply_module, PiLp.add_apply,
+          PiLp.smul_apply, planePoint_apply_one, smul_eq_mul, mul_zero, zero_add]
       rw [hcoord0, hdx0, mul_zero] at hcone
       rw [hcoord1] at hcone
-      have hdy0 : q 1 = 0 := by nlinarith
+      have hdy0 : q 1 = 0 := by nlinarith only [htpos, hcone]
       exfalso
       apply hq
       apply plane_ext
       · simp only [planePoint_apply_zero]
-        linarith
+        linarith only [hdx0]
       · simpa [planePoint] using hdy0
     · intro p hp
       rw [Set.mem_singleton_iff] at hp
       subst p
       refine ⟨?_, left_mem_segment ℝ _ _⟩
-      exact ⟨planePoint (-1) 0, Or.inl <|
-        subset_convexHull ℝ _ ⟨2, rfl⟩, by
-          simp [thinKiteMap, planePoint]⟩
+      exact thinKitePatch_leftBase_mem δ
   · let ε := -q 1 / (q 0 + 1)
     have hε : 0 < ε := by
       dsimp [ε]
@@ -466,7 +480,7 @@ theorem exists_thinKitePatch_inter_leftSegment_eq_singleton {q : Plane}
     apply Set.Subset.antisymm
     · rintro p ⟨hpPatch, hpSegment⟩
       by_cases hpLeft : p = planePoint (-1) 0
-      · simp [hpLeft]
+      · simp only [hpLeft, Set.mem_singleton_iff]
       rw [segment_eq_image_lineMap] at hpSegment
       obtain ⟨t, ht, rfl⟩ := hpSegment
       have htne : t ≠ 0 := by
@@ -477,24 +491,24 @@ theorem exists_thinKitePatch_inter_leftSegment_eq_singleton {q : Plane}
       have hcone := thinKitePatch_subset_leftCone hδ.le hpPatch
       have hcoord0 :
           (AffineMap.lineMap (planePoint (-1) 0) q t) 0 + 1 = t * (q 0 + 1) := by
-        simp [AffineMap.lineMap_apply_module, planePoint]
+        simp only [AffineMap.lineMap_apply_module, PiLp.add_apply,
+          PiLp.smul_apply, planePoint_apply_zero, smul_eq_mul]
         ring
       have hcoord1 :
           (AffineMap.lineMap (planePoint (-1) 0) q t) 1 = t * q 1 := by
-        simp [AffineMap.lineMap_apply_module, planePoint]
+        simp only [AffineMap.lineMap_apply_module, PiLp.add_apply,
+          PiLp.smul_apply, planePoint_apply_one, smul_eq_mul, mul_zero, zero_add]
       rw [hcoord0, hcoord1] at hcone
       have hmargin : δ * (q 0 + 1) < -q 1 := by
         dsimp [ε] at hδε
         exact (lt_div_iff₀ hx).mp hδε
       exfalso
-      nlinarith
+      nlinarith only [htpos, hmargin, hcone]
     · intro p hp
       rw [Set.mem_singleton_iff] at hp
       subst p
       refine ⟨?_, left_mem_segment ℝ _ _⟩
-      exact ⟨planePoint (-1) 0, Or.inl <|
-        subset_convexHull ℝ _ ⟨2, rfl⟩, by
-          simp [thinKiteMap, planePoint]⟩
+      exact thinKitePatch_leftBase_mem δ
   · let ε := q 1 / (q 0 + 1) - 1
     have hε : 0 < ε := by
       dsimp [ε]
@@ -504,7 +518,7 @@ theorem exists_thinKitePatch_inter_leftSegment_eq_singleton {q : Plane}
     apply Set.Subset.antisymm
     · rintro p ⟨hpPatch, hpSegment⟩
       by_cases hpLeft : p = planePoint (-1) 0
-      · simp [hpLeft]
+      · simp only [hpLeft, Set.mem_singleton_iff]
       rw [segment_eq_image_lineMap] at hpSegment
       obtain ⟨t, ht, rfl⟩ := hpSegment
       have htne : t ≠ 0 := by
@@ -515,26 +529,26 @@ theorem exists_thinKitePatch_inter_leftSegment_eq_singleton {q : Plane}
       have hcone := thinKitePatch_subset_leftCone hδ.le hpPatch
       have hcoord0 :
           (AffineMap.lineMap (planePoint (-1) 0) q t) 0 + 1 = t * (q 0 + 1) := by
-        simp [AffineMap.lineMap_apply_module, planePoint]
+        simp only [AffineMap.lineMap_apply_module, PiLp.add_apply,
+          PiLp.smul_apply, planePoint_apply_zero, smul_eq_mul]
         ring
       have hcoord1 :
           (AffineMap.lineMap (planePoint (-1) 0) q t) 1 = t * q 1 := by
-        simp [AffineMap.lineMap_apply_module, planePoint]
+        simp only [AffineMap.lineMap_apply_module, PiLp.add_apply,
+          PiLp.smul_apply, planePoint_apply_one, smul_eq_mul, mul_zero, zero_add]
       rw [hcoord0, hcoord1] at hcone
       have hmargin : (1 + δ) * (q 0 + 1) < q 1 := by
         dsimp [ε] at hδε
         rw [lt_sub_iff_add_lt] at hδε
         have := (lt_div_iff₀ hx).mp hδε
-        nlinarith
+        simpa only [add_comm] using this
       exfalso
-      nlinarith
+      nlinarith only [htpos, hmargin, hcone]
     · intro p hp
       rw [Set.mem_singleton_iff] at hp
       subst p
       refine ⟨?_, left_mem_segment ℝ _ _⟩
-      exact ⟨planePoint (-1) 0, Or.inl <|
-        subset_convexHull ℝ _ ⟨2, rfl⟩, by
-          simp [thinKiteMap, planePoint]⟩
+      exact thinKitePatch_leftBase_mem δ
 
 /-- A segment leaving the right base vertex outside the triangle misses every sufficiently thin
 kite except at that vertex. -/
@@ -549,7 +563,7 @@ theorem exists_thinKitePatch_inter_rightSegment_eq_singleton {q : Plane}
     apply Set.Subset.antisymm
     · rintro p ⟨hpPatch, hpSegment⟩
       by_cases hpRight : p = planePoint 1 0
-      · simp [hpRight]
+      · simp only [hpRight, Set.mem_singleton_iff]
       rw [segment_eq_image_lineMap] at hpSegment
       obtain ⟨t, ht, rfl⟩ := hpSegment
       have htne : t ≠ 0 := by
@@ -560,30 +574,30 @@ theorem exists_thinKitePatch_inter_rightSegment_eq_singleton {q : Plane}
       have hcone := thinKitePatch_subset_rightCone hδ.le hpPatch
       have hcoord0 :
           1 - (AffineMap.lineMap (planePoint 1 0) q t) 0 = t * (1 - q 0) := by
-        simp [AffineMap.lineMap_apply_module, planePoint]
+        simp only [AffineMap.lineMap_apply_module, PiLp.add_apply,
+          PiLp.smul_apply, planePoint_apply_zero, smul_eq_mul]
         ring
       have hdx0 : 1 - q 0 = 0 := by
         rw [hcoord0] at hcone
-        nlinarith
+        nlinarith only [htpos, hx, hcone.1]
       have hcoord1 :
           (AffineMap.lineMap (planePoint 1 0) q t) 1 = t * q 1 := by
-        simp [AffineMap.lineMap_apply_module, planePoint]
+        simp only [AffineMap.lineMap_apply_module, PiLp.add_apply,
+          PiLp.smul_apply, planePoint_apply_one, smul_eq_mul, mul_zero, zero_add]
       rw [hcoord0, hdx0, mul_zero] at hcone
       rw [hcoord1] at hcone
-      have hdy0 : q 1 = 0 := by nlinarith
+      have hdy0 : q 1 = 0 := by nlinarith only [htpos, hcone]
       exfalso
       apply hq
       apply plane_ext
       · simp only [planePoint_apply_zero]
-        linarith
+        linarith only [hdx0]
       · simpa [planePoint] using hdy0
     · intro p hp
       rw [Set.mem_singleton_iff] at hp
       subst p
       refine ⟨?_, left_mem_segment ℝ _ _⟩
-      exact ⟨planePoint 1 0, Or.inr <|
-        subset_convexHull ℝ _ ⟨2, rfl⟩, by
-          simp [thinKiteMap, planePoint]⟩
+      exact thinKitePatch_rightBase_mem δ
   · let ε := -q 1 / (1 - q 0)
     have hε : 0 < ε := by
       dsimp [ε]
@@ -592,7 +606,7 @@ theorem exists_thinKitePatch_inter_rightSegment_eq_singleton {q : Plane}
     apply Set.Subset.antisymm
     · rintro p ⟨hpPatch, hpSegment⟩
       by_cases hpRight : p = planePoint 1 0
-      · simp [hpRight]
+      · simp only [hpRight, Set.mem_singleton_iff]
       rw [segment_eq_image_lineMap] at hpSegment
       obtain ⟨t, ht, rfl⟩ := hpSegment
       have htne : t ≠ 0 := by
@@ -603,24 +617,24 @@ theorem exists_thinKitePatch_inter_rightSegment_eq_singleton {q : Plane}
       have hcone := thinKitePatch_subset_rightCone hδ.le hpPatch
       have hcoord0 :
           1 - (AffineMap.lineMap (planePoint 1 0) q t) 0 = t * (1 - q 0) := by
-        simp [AffineMap.lineMap_apply_module, planePoint]
+        simp only [AffineMap.lineMap_apply_module, PiLp.add_apply,
+          PiLp.smul_apply, planePoint_apply_zero, smul_eq_mul]
         ring
       have hcoord1 :
           (AffineMap.lineMap (planePoint 1 0) q t) 1 = t * q 1 := by
-        simp [AffineMap.lineMap_apply_module, planePoint]
+        simp only [AffineMap.lineMap_apply_module, PiLp.add_apply,
+          PiLp.smul_apply, planePoint_apply_one, smul_eq_mul, mul_zero, zero_add]
       rw [hcoord0, hcoord1] at hcone
       have hmargin : δ * (1 - q 0) < -q 1 := by
         dsimp [ε] at hδε
         exact (lt_div_iff₀ hx).mp hδε
       exfalso
-      nlinarith
+      nlinarith only [htpos, hmargin, hcone]
     · intro p hp
       rw [Set.mem_singleton_iff] at hp
       subst p
       refine ⟨?_, left_mem_segment ℝ _ _⟩
-      exact ⟨planePoint 1 0, Or.inr <|
-        subset_convexHull ℝ _ ⟨2, rfl⟩, by
-          simp [thinKiteMap, planePoint]⟩
+      exact thinKitePatch_rightBase_mem δ
   · let ε := q 1 / (1 - q 0) - 1
     have hε : 0 < ε := by
       dsimp [ε]
@@ -630,7 +644,7 @@ theorem exists_thinKitePatch_inter_rightSegment_eq_singleton {q : Plane}
     apply Set.Subset.antisymm
     · rintro p ⟨hpPatch, hpSegment⟩
       by_cases hpRight : p = planePoint 1 0
-      · simp [hpRight]
+      · simp only [hpRight, Set.mem_singleton_iff]
       rw [segment_eq_image_lineMap] at hpSegment
       obtain ⟨t, ht, rfl⟩ := hpSegment
       have htne : t ≠ 0 := by
@@ -641,26 +655,26 @@ theorem exists_thinKitePatch_inter_rightSegment_eq_singleton {q : Plane}
       have hcone := thinKitePatch_subset_rightCone hδ.le hpPatch
       have hcoord0 :
           1 - (AffineMap.lineMap (planePoint 1 0) q t) 0 = t * (1 - q 0) := by
-        simp [AffineMap.lineMap_apply_module, planePoint]
+        simp only [AffineMap.lineMap_apply_module, PiLp.add_apply,
+          PiLp.smul_apply, planePoint_apply_zero, smul_eq_mul]
         ring
       have hcoord1 :
           (AffineMap.lineMap (planePoint 1 0) q t) 1 = t * q 1 := by
-        simp [AffineMap.lineMap_apply_module, planePoint]
+        simp only [AffineMap.lineMap_apply_module, PiLp.add_apply,
+          PiLp.smul_apply, planePoint_apply_one, smul_eq_mul, mul_zero, zero_add]
       rw [hcoord0, hcoord1] at hcone
       have hmargin : (1 + δ) * (1 - q 0) < q 1 := by
         dsimp [ε] at hδε
         rw [lt_sub_iff_add_lt] at hδε
         have := (lt_div_iff₀ hx).mp hδε
-        nlinarith
+        simpa only [add_comm] using this
       exfalso
-      nlinarith
+      nlinarith only [htpos, hmargin, hcone]
     · intro p hp
       rw [Set.mem_singleton_iff] at hp
       subst p
       refine ⟨?_, left_mem_segment ℝ _ _⟩
-      exact ⟨planePoint 1 0, Or.inr <|
-        subset_convexHull ℝ _ ⟨2, rfl⟩, by
-          simp [thinKiteMap, planePoint]⟩
+      exact thinKitePatch_rightBase_mem δ
 
 theorem thinKiteMap_zero_mem_triangle {q : Plane} (hq : q ∈ diamondPatch) :
     thinKiteMap 0 q ∈ convexHull ℝ (Set.range kiteTrianglePosition) := by
@@ -825,12 +839,12 @@ theorem thinKiteSource_lower {δ : ℝ} (hδ : 0 < δ) : -2 < thinKiteSource δ
 theorem thinKiteSource_upper {δ : ℝ} (hδ : 0 < δ) : thinKiteSource δ < 2 := by
   have hd : 0 < 1 + 2 * δ := by positivity
   rw [thinKiteSource, div_lt_iff₀ hd]
-  nlinarith
+  linarith only [hd]
 
 theorem thinKiteTarget_lower {δ : ℝ} (hδ : 0 < δ) : -2 < thinKiteTarget δ := by
   have hd : 0 < 1 + 2 * δ := by positivity
   rw [thinKiteTarget, lt_div_iff₀ hd]
-  nlinarith
+  linarith only [hd]
 
 theorem thinKiteTarget_upper {δ : ℝ} (hδ : 0 < δ) : thinKiteTarget δ < 2 := by
   have hd : 0 < 1 + 2 * δ := by positivity
diff --git a/LeanPool/ClassificationOfSurfaces/NormalForm.lean b/LeanPool/ClassificationOfSurfaces/NormalForm.lean
index c08123993a..a2b3b4813c 100644
--- a/LeanPool/ClassificationOfSurfaces/NormalForm.lean
+++ b/LeanPool/ClassificationOfSurfaces/NormalForm.lean
@@ -11,10 +11,6 @@ public import LeanPool.ClassificationOfSurfaces.Representatives
 import LeanPool.ClassificationOfSurfaces.FiniteCyclicCanonicalRealization
 import LeanPool.ClassificationOfSurfaces.FiniteCyclicSphereRealization
 import LeanPool.ClassificationOfSurfaces.FiniteCyclicTerminalNormalization
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Faithful normal-form classification
diff --git a/LeanPool/ClassificationOfSurfaces/P2DegenerateDisk.lean b/LeanPool/ClassificationOfSurfaces/P2DegenerateDisk.lean
index 213d93c879..ca9176e199 100644
--- a/LeanPool/ClassificationOfSurfaces/P2DegenerateDisk.lean
+++ b/LeanPool/ClassificationOfSurfaces/P2DegenerateDisk.lean
@@ -7,10 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.DiskSquare
 public import LeanPool.ClassificationOfSurfaces.SphereCarrierGeometry
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # The one-sided-degenerate P2 disk model
@@ -1183,12 +1179,14 @@ theorem exists_collarMap_eq_smul_teardropMap
   have hspos : 0 < s := hs0.lt_of_ne' (by
     simpa [s] using hheight)
   have hfactorLower : -1 ≤ 3 - 4 * a := by
-    nlinarith
+    linarith only [haOne]
   have hfactorUpper : 3 - 4 * a ≤ 1 := by
-    nlinarith
+    linarith only [haHalf]
   have hyBounds : -s ≤ y ∧ y ≤ s := by
     dsimp [y]
-    constructor <;> nlinarith
+    constructor
+    · simpa only [mul_neg_one] using mul_le_mul_of_nonneg_left hfactorLower hs0
+    · simpa only [mul_one] using mul_le_mul_of_nonneg_left hfactorUpper hs0
   have hySq : y ^ 2 ≤ s ^ 2 := by
     exact sq_le_sq' hyBounds.1 hyBounds.2
   let w : PolygonCell 2 :=
@@ -1200,16 +1198,16 @@ theorem exists_collarMap_eq_smul_teardropMap
         rw [Complex.normSq_apply]
         change
           upper.val.re * upper.val.re + y * y ≤ 1
-        nlinarith
+        nlinarith only [hupperSq, hySq]
       rw [Complex.normSq_eq_norm_sq] at hnormSq
-      nlinarith [norm_nonneg (Complex.mk upper.val.re y)]⟩
+      nlinarith only [hnormSq, norm_nonneg (Complex.mk upper.val.re y)]⟩
   have hwHeight : chordHeight w = s := by
     have hwSq := chordHeight_sq w
     have hupperSq := chordHeight_sq upper
     have hwre : w.val.re = upper.val.re := by rfl
     rw [hwre] at hwSq
     have hw0 := chordHeight_nonneg w
-    nlinarith
+    exact (sq_eq_sq₀ hw0 hs0).mp (hwSq.trans hupperSq.symm)
   have hwCircle : collarCirclePoint w = q := by
     rw [← hcircle]
     apply PolygonCell.ext
diff --git a/LeanPool/ClassificationOfSurfaces/RepresentativeCarrier.lean b/LeanPool/ClassificationOfSurfaces/RepresentativeCarrier.lean
index 3b4cdad4bf..06d4f0ab00 100644
--- a/LeanPool/ClassificationOfSurfaces/RepresentativeCarrier.lean
+++ b/LeanPool/ClassificationOfSurfaces/RepresentativeCarrier.lean
@@ -7,11 +7,7 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.CellComplexQuotient
 public import LeanPool.ClassificationOfSurfaces.LeanEval.ChallengeDeps
-import Mathlib.Analysis.SpecialFunctions.Bernstein
 import Mathlib.Analysis.SpecialFunctions.Complex.Circle
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Carrier bridge to the Eval quotient representatives
diff --git a/LeanPool/ClassificationOfSurfaces/SignedPresentation.lean b/LeanPool/ClassificationOfSurfaces/SignedPresentation.lean
index 7a89a7dfcb..94fbbe3410 100644
--- a/LeanPool/ClassificationOfSurfaces/SignedPresentation.lean
+++ b/LeanPool/ClassificationOfSurfaces/SignedPresentation.lean
@@ -6,10 +6,6 @@ Authors: Ryan McCorvie, Jack McCarthy
 module
 
 public import LeanPool.ClassificationOfSurfaces.CellComplex
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Finite signed-dart presentations
diff --git a/LeanPool/ClassificationOfSurfaces/SphereCarrierGeometry.lean b/LeanPool/ClassificationOfSurfaces/SphereCarrierGeometry.lean
index 32dc87d3b8..e1f0ec2d6f 100644
--- a/LeanPool/ClassificationOfSurfaces/SphereCarrierGeometry.lean
+++ b/LeanPool/ClassificationOfSurfaces/SphereCarrierGeometry.lean
@@ -7,11 +7,7 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.PolygonalQuotient
 import LeanPool.ClassificationOfSurfaces.RepresentativeCarrier
-import Mathlib.Analysis.SpecialFunctions.Bernstein
 import Mathlib.Analysis.SpecialFunctions.Complex.Circle
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Disk geometry for the sphere carrier
diff --git a/LeanPool/ClassificationOfSurfaces/SphereHemisphere.lean b/LeanPool/ClassificationOfSurfaces/SphereHemisphere.lean
index 72c3f952e4..01b5378c70 100644
--- a/LeanPool/ClassificationOfSurfaces/SphereHemisphere.lean
+++ b/LeanPool/ClassificationOfSurfaces/SphereHemisphere.lean
@@ -8,10 +8,6 @@ module
 public import LeanPool.ClassificationOfSurfaces.Representatives
 public import LeanPool.ClassificationOfSurfaces.CellComplexQuotient
 import LeanPool.ClassificationOfSurfaces.SphereCarrierGeometry
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Hemisphere maps for the two-monogon sphere
diff --git a/LeanPool/ClassificationOfSurfaces/SphereQuotientHomeomorph.lean b/LeanPool/ClassificationOfSurfaces/SphereQuotientHomeomorph.lean
index 7411504d74..5abef73f74 100644
--- a/LeanPool/ClassificationOfSurfaces/SphereQuotientHomeomorph.lean
+++ b/LeanPool/ClassificationOfSurfaces/SphereQuotientHomeomorph.lean
@@ -7,10 +7,6 @@ module
 
 public import LeanPool.ClassificationOfSurfaces.SphereHemisphere
 public import LeanPool.ClassificationOfSurfaces.SphereCarrierGeometry
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # The two-monogon quotient is the standard sphere
diff --git a/LeanPool/ClassificationOfSurfaces/StrongVertexStar.lean b/LeanPool/ClassificationOfSurfaces/StrongVertexStar.lean
index b027598933..2e8bab423c 100644
--- a/LeanPool/ClassificationOfSurfaces/StrongVertexStar.lean
+++ b/LeanPool/ClassificationOfSurfaces/StrongVertexStar.lean
@@ -9,10 +9,6 @@ public import LeanPool.ClassificationOfSurfaces.Moise.GeometricTriangulation
 public import Mathlib.Geometry.Manifold.Instances.Real
 import LeanPool.ClassificationOfSurfaces.Moise.PuncturedSurface
 import LeanPool.ClassificationOfSurfaces.Triangulation
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.Combinatorics.SimpleGraph.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Fixed-vertex stars in a surface triangulation
diff --git a/LeanPool/ClassificationOfSurfaces/Triangulation.lean b/LeanPool/ClassificationOfSurfaces/Triangulation.lean
index 9ac47574d2..3b33ba2f86 100644
--- a/LeanPool/ClassificationOfSurfaces/Triangulation.lean
+++ b/LeanPool/ClassificationOfSurfaces/Triangulation.lean
@@ -9,9 +9,6 @@ public import LeanPool.ClassificationOfSurfaces.Moise.IntrinsicComplex
 public import Mathlib.Geometry.Manifold.Instances.Real
 import LeanPool.ClassificationOfSurfaces.Moise.ChartInduction
 import LeanPool.ClassificationOfSurfaces.Moise.DualConnectivity
-import Mathlib.Analysis.SpecialFunctions.Bernstein
-import Mathlib.CategoryTheory.Category.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Finite surface triangulations