From 68c6b5cd484976c2e6f3ce8f78f87f5099bb9339 Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Wed, 21 Oct 2026 19:56:33 +0000
Subject: [PATCH 1/2] Reduce ConwaySoifer certificate compilation memory

---
 LeanPool/ConwaySoifer.lean                    |   1 -
 .../ConwaySoifer/Certificates/Checker.lean    |   1 -
 .../Certificates/CheckerSound.lean            |   7 +-
 .../ConwaySoifer/Certificates/IntPoly.lean    |   7 +-
 .../Certificates/IntervalCover.lean           |   3 +-
 .../Certificates/KernelReplay.lean            |   2 +-
 LeanPool/ConwaySoifer/Certificates/Model.lean |   1 -
 .../ConwaySoifer/Certificates/ModelSound.lean |   7 +-
 .../ConwaySoifer/Certificates/Witness.lean    |   2 +-
 .../Certificates/WitnessedArithmetic.lean     |   5 +-
 .../ConwaySoifer/Geometry/AcrossFacts.lean    |   7 +-
 LeanPool/ConwaySoifer/Geometry/AownFacts.lean |   7 +-
 LeanPool/ConwaySoifer/Geometry/Area.lean      |   8 +-
 LeanPool/ConwaySoifer/Geometry/Basic.lean     |   6 +-
 LeanPool/ConwaySoifer/Geometry/Budget.lean    |   4 +-
 LeanPool/ConwaySoifer/Geometry/Canonical.lean |   3 +-
 LeanPool/ConwaySoifer/Geometry/Cap.lean       |   7 +-
 LeanPool/ConwaySoifer/Geometry/CornerCap.lean |   7 +-
 LeanPool/ConwaySoifer/Geometry/Diameter.lean  |   3 +-
 .../ConwaySoifer/Geometry/Halfspaces.lean     |   3 +-
 LeanPool/ConwaySoifer/Geometry/Locality.lean  |   3 +-
 LeanPool/ConwaySoifer/Geometry/Normal.lean    |   2 +-
 .../ConwaySoifer/Geometry/Normalization.lean  |   7 +-
 LeanPool/ConwaySoifer/Geometry/Oblique.lean   |   5 +-
 LeanPool/ConwaySoifer/Geometry/Owners.lean    |   4 +-
 LeanPool/ConwaySoifer/Geometry/Rays.lean      |   7 +-
 .../ConwaySoifer/Geometry/ReceiverFacts.lean  |   1 -
 LeanPool/ConwaySoifer/Geometry/Scaling.lean   |   3 +-
 LeanPool/ConwaySoifer/Geometry/SideFacts.lean |   7 +-
 LeanPool/ConwaySoifer/Geometry/Support.lean   |   8 +-
 LeanPool/ConwaySoifer/Geometry/Symmetry.lean  |   5 +-
 .../Geometry/TriangleHalfspaces.lean          |   5 +-
 .../SevenTriangles/Geometry/Area.lean         |   8 +-
 .../SevenTriangles/Geometry/Basic.lean        |   6 +-
 .../SevenTriangles/Geometry/Diameter.lean     |   5 +-
 .../SevenTriangles/Geometry/Support.lean      |   9 +-
 .../SevenTriangles/Geometry/Wedge.lean        |   9 +-
 .../Simplified/Certificates/AllChecked.lean   |   2 -
 .../Simplified/Certificates/AllData.lean      |   1 -
 .../Simplified/Certificates/Coverage.lean     |   3 +-
 .../Certificates/Steps/Aown1200001300000.lean | 110 ++++-
 .../Certificates/Steps/Aown1500001600003.lean | 456 +++++++++++++++++-
 .../Certificates/Steps/Aown1600001700001.lean | 135 +++++-
 .../Certificates/Steps/Aown1600001700005.lean | 379 ++++++++++++++-
 .../Simplified/Complements/AcrossLarge.lean   |   6 +-
 .../Simplified/Complements/AcrossSmall.lean   |   6 +-
 .../Simplified/Complements/AownLarge.lean     |   4 +-
 .../Simplified/Complements/AownSmall.lean     |   5 +-
 .../Simplified/Complements/SextSmall.lean     |   6 +-
 .../Simplified/Complements/SintSmall.lean     |   6 +-
 .../Simplified/Geometry/AcrossArea.lean       |   5 +-
 .../Simplified/Geometry/AcrossFour.lean       |   6 +-
 .../Geometry/AcrossLargeCentre.lean           |   4 +-
 .../Simplified/Geometry/AcrossLargeSide.lean  |   4 +-
 .../Simplified/Geometry/Affine.lean           |   2 +-
 .../Simplified/Geometry/AownArea.lean         |   8 +-
 .../Simplified/Geometry/AownCentral.lean      |   6 +-
 .../Simplified/Geometry/AownChains.lean       |   6 +-
 .../Simplified/Geometry/AownCut.lean          |   5 +-
 .../Simplified/Geometry/Bridge.lean           |   4 +-
 .../Simplified/Geometry/BridgeLocal.lean      |   6 +-
 .../Simplified/Geometry/CentralWitnesses.lean |   6 +-
 .../Simplified/Geometry/Charging.lean         |   7 +-
 .../Simplified/Geometry/Core.lean             |   5 +-
 .../Simplified/Geometry/CoreLocal.lean        |   6 +-
 .../Simplified/Geometry/CornerAbsent.lean     |   3 +-
 .../Simplified/Geometry/ForbiddenCorner.lean  |   3 +-
 .../Simplified/Geometry/FullOwn.lean          |   6 +-
 .../Simplified/Geometry/HexSymmetry.lean      |   5 +-
 .../Simplified/Geometry/LocalSideCover.lean   |   2 +-
 .../Simplified/Geometry/MiddleThird.lean      |   4 +-
 .../Simplified/Geometry/Midpoint.lean         |   5 +-
 .../Simplified/Geometry/Profile0Q0.lean       |   6 +-
 .../Simplified/Geometry/Profile0Q1.lean       |   6 +-
 .../Simplified/Geometry/Profile0Q2.lean       |   6 +-
 .../Simplified/Geometry/Profile1Q0.lean       |   6 +-
 .../Simplified/Geometry/Profile1Q1.lean       |   6 +-
 .../Simplified/Geometry/Profile1Q2.lean       |   6 +-
 .../Simplified/Geometry/Profile2Q0.lean       |   6 +-
 .../Simplified/Geometry/Profile2Q1.lean       |   6 +-
 .../Simplified/Geometry/Profile2Q2.lean       |   6 +-
 .../Simplified/Geometry/Profile3Q0.lean       |   6 +-
 .../Simplified/Geometry/Profile3Q1.lean       |   6 +-
 .../Simplified/Geometry/Profile3Q2.lean       |   6 +-
 .../Simplified/Geometry/Profile4Q0.lean       |   6 +-
 .../Simplified/Geometry/Profile4Q1.lean       |   6 +-
 .../Simplified/Geometry/Profile4Q2.lean       |   6 +-
 .../Simplified/Geometry/Profile5Q0.lean       |   6 +-
 .../Simplified/Geometry/Profile5Q1.lean       |   6 +-
 .../Simplified/Geometry/Profile5Q2.lean       |   6 +-
 .../Simplified/Geometry/Profile6Q0.lean       |   6 +-
 .../Simplified/Geometry/Profile6Q1.lean       |   6 +-
 .../Simplified/Geometry/Profile6Q2.lean       |   6 +-
 .../Simplified/Geometry/Profile7Q0.lean       |   6 +-
 .../Simplified/Geometry/Profile7Q1.lean       |   6 +-
 .../Simplified/Geometry/Profile7Q2.lean       |   6 +-
 .../Simplified/Geometry/ProfileWitness.lean   |   5 +-
 .../Simplified/Geometry/Receiver.lean         |   6 +-
 .../Simplified/Geometry/SideChains.lean       |   4 +-
 .../Simplified/Geometry/SintCorner.lean       |   6 +-
 .../Simplified/Geometry/SupportFan.lean       |   3 +-
 .../Simplified/Geometry/ThreeCentral.lean     |   6 +-
 .../Simplified/Geometry/ThreeWitnesses.lean   |   4 +-
 .../Simplified/Normalization.lean             |   1 -
 LeanPool/ConwaySoifer/Simplified/Theorem.lean |   2 +-
 105 files changed, 1469 insertions(+), 124 deletions(-)

diff --git a/LeanPool/ConwaySoifer.lean b/LeanPool/ConwaySoifer.lean
index 3623adbec8..25fa30a31b 100644
--- a/LeanPool/ConwaySoifer.lean
+++ b/LeanPool/ConwaySoifer.lean
@@ -6,7 +6,6 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Simplified.Theorem
-import Mathlib.Tactic
 
 /-!
 # Conway–Soifer covering conjecture for n = 3
diff --git a/LeanPool/ConwaySoifer/Certificates/Checker.lean b/LeanPool/ConwaySoifer/Certificates/Checker.lean
index 2ed5e81411..f56c5e8635 100644
--- a/LeanPool/ConwaySoifer/Certificates/Checker.lean
+++ b/LeanPool/ConwaySoifer/Certificates/Checker.lean
@@ -8,7 +8,6 @@ module
 public import LeanPool.ConwaySoifer.Certificates.IntPoly
 public import Mathlib.Data.Int.Sqrt
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
 
 /-!
 # The contact-sensitive exclusion checker (computable part)
diff --git a/LeanPool/ConwaySoifer/Certificates/CheckerSound.lean b/LeanPool/ConwaySoifer/Certificates/CheckerSound.lean
index 86ae29dccf..7f772cdb6e 100644
--- a/LeanPool/ConwaySoifer/Certificates/CheckerSound.lean
+++ b/LeanPool/ConwaySoifer/Certificates/CheckerSound.lean
@@ -8,7 +8,12 @@ module
 public import LeanPool.ConwaySoifer.Certificates.Model
 public import LeanPool.ConwaySoifer.Geometry.Support
 public import LeanPool.ConwaySoifer.Geometry.Owners
-import Mathlib.Tactic
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # Soundness of the contact-sensitive checker
diff --git a/LeanPool/ConwaySoifer/Certificates/IntPoly.lean b/LeanPool/ConwaySoifer/Certificates/IntPoly.lean
index 4e2ea43af2..817a6ea10a 100644
--- a/LeanPool/ConwaySoifer/Certificates/IntPoly.lean
+++ b/LeanPool/ConwaySoifer/Certificates/IntPoly.lean
@@ -7,7 +7,12 @@ module
 
 public import Mathlib.Basic.Real.Basic
 public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
-import Mathlib.Tactic
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.LinearCombination
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # Integer polynomials and verified Bernstein sign checkers
diff --git a/LeanPool/ConwaySoifer/Certificates/IntervalCover.lean b/LeanPool/ConwaySoifer/Certificates/IntervalCover.lean
index 108b502941..cf068f5220 100644
--- a/LeanPool/ConwaySoifer/Certificates/IntervalCover.lean
+++ b/LeanPool/ConwaySoifer/Certificates/IntervalCover.lean
@@ -6,7 +6,8 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Certificates.ModelSound
-import Mathlib.Tactic
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
 
 /-!
 # IntervalCover
diff --git a/LeanPool/ConwaySoifer/Certificates/KernelReplay.lean b/LeanPool/ConwaySoifer/Certificates/KernelReplay.lean
index d5db6422f4..5a4d190e56 100644
--- a/LeanPool/ConwaySoifer/Certificates/KernelReplay.lean
+++ b/LeanPool/ConwaySoifer/Certificates/KernelReplay.lean
@@ -6,7 +6,7 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Certificates.Witness
-import Mathlib.Tactic
+import Mathlib.Tactic.NormNum.Basic
 
 /-! Extensional checkpoint lemmas for kernel-checked certificate replay.
 Concrete checkpoints are untrusted data; every transition is proved in Lean. -/
diff --git a/LeanPool/ConwaySoifer/Certificates/Model.lean b/LeanPool/ConwaySoifer/Certificates/Model.lean
index 1b3c280960..58de94c6ec 100644
--- a/LeanPool/ConwaySoifer/Certificates/Model.lean
+++ b/LeanPool/ConwaySoifer/Certificates/Model.lean
@@ -7,7 +7,6 @@ module
 
 public import LeanPool.ConwaySoifer.Certificates.Checker
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
 
 /-!
 # Certificate data and the initial necessary model
diff --git a/LeanPool/ConwaySoifer/Certificates/ModelSound.lean b/LeanPool/ConwaySoifer/Certificates/ModelSound.lean
index fcd25748b1..330ed76b8c 100644
--- a/LeanPool/ConwaySoifer/Certificates/ModelSound.lean
+++ b/LeanPool/ConwaySoifer/Certificates/ModelSound.lean
@@ -7,7 +7,12 @@ module
 
 public import LeanPool.ConwaySoifer.Certificates.CheckerSound
 public import LeanPool.ConwaySoifer.Geometry.Canonical
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Ring
 
 /-!
 # The initial model follows from the canonical case hypotheses
diff --git a/LeanPool/ConwaySoifer/Certificates/Witness.lean b/LeanPool/ConwaySoifer/Certificates/Witness.lean
index edc50a889a..26b854d264 100644
--- a/LeanPool/ConwaySoifer/Certificates/Witness.lean
+++ b/LeanPool/ConwaySoifer/Certificates/Witness.lean
@@ -6,7 +6,7 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Certificates.WitnessedArithmetic
-import Mathlib.Tactic
+import Mathlib.Tactic.NormNum.Basic
 
 /-! Untrusted exclusion hints with kernel-checked local arithmetic.
 The producer chooses a method, fan, or split; soundness does not trust the search. -/
diff --git a/LeanPool/ConwaySoifer/Certificates/WitnessedArithmetic.lean b/LeanPool/ConwaySoifer/Certificates/WitnessedArithmetic.lean
index a8efa1ce7a..7b4933ac9d 100644
--- a/LeanPool/ConwaySoifer/Certificates/WitnessedArithmetic.lean
+++ b/LeanPool/ConwaySoifer/Certificates/WitnessedArithmetic.lean
@@ -6,7 +6,10 @@ Authors: Vladislav Kuznetsov, Lean Pool contributors
 module
 
 public import LeanPool.ConwaySoifer.Certificates.CheckerSound
-import Mathlib.Tactic
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
 
 /-! Explicit arithmetic witnesses avoid re-running proposal searches in the kernel. -/
 
diff --git a/LeanPool/ConwaySoifer/Geometry/AcrossFacts.lean b/LeanPool/ConwaySoifer/Geometry/AcrossFacts.lean
index 713f40a201..b18823a53e 100644
--- a/LeanPool/ConwaySoifer/Geometry/AcrossFacts.lean
+++ b/LeanPool/ConwaySoifer/Geometry/AcrossFacts.lean
@@ -6,7 +6,12 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Geometry.AownFacts
-import Mathlib.Tactic
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.FunProp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # §8.1: the small `Across` regime `s ≤ 1/400`
diff --git a/LeanPool/ConwaySoifer/Geometry/AownFacts.lean b/LeanPool/ConwaySoifer/Geometry/AownFacts.lean
index 5b982f6adc..89068f6d36 100644
--- a/LeanPool/ConwaySoifer/Geometry/AownFacts.lean
+++ b/LeanPool/ConwaySoifer/Geometry/AownFacts.lean
@@ -6,7 +6,12 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Geometry.Normalization
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.FunProp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # §6: the strengthening of `Aown` for `s ≤ 1/14`
diff --git a/LeanPool/ConwaySoifer/Geometry/Area.lean b/LeanPool/ConwaySoifer/Geometry/Area.lean
index 96e6984a4c..29bae4a85c 100644
--- a/LeanPool/ConwaySoifer/Geometry/Area.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Area.lean
@@ -11,7 +11,13 @@ public import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 public import Mathlib.MeasureTheory.Measure.Haar.OfBasis
 public import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
 public import Mathlib.LinearAlgebra.Basis.Fin
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.FunProp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.NormNum.RealSqrt
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 Lebesgue area in triangular coordinates. Physical area is sqrt(3)/2 times
diff --git a/LeanPool/ConwaySoifer/Geometry/Basic.lean b/LeanPool/ConwaySoifer/Geometry/Basic.lean
index dc72d37a8a..4e7c7d6d8f 100644
--- a/LeanPool/ConwaySoifer/Geometry/Basic.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Basic.lean
@@ -8,7 +8,11 @@ module
 public import Mathlib.Analysis.Convex.Hull
 public import Mathlib.Basic.Real.Basic
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.NormNum.RealSqrt
+import Mathlib.Tactic.Ring
 
 /-!
 The point `(a, b)` represents `(a+b/2, sqrt(3)*b/2)` in the Euclidean plane.
diff --git a/LeanPool/ConwaySoifer/Geometry/Budget.lean b/LeanPool/ConwaySoifer/Geometry/Budget.lean
index 5799b376a4..51cb184bf5 100644
--- a/LeanPool/ConwaySoifer/Geometry/Budget.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Budget.lean
@@ -9,7 +9,9 @@ public import LeanPool.ConwaySoifer.Geometry.CornerCap
 public import LeanPool.ConwaySoifer.Geometry.Normal
 public import LeanPool.ConwaySoifer.Geometry.Oblique
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
 
 /-!
 # The area budget with corner help and the bound `s < 11/25`
diff --git a/LeanPool/ConwaySoifer/Geometry/Canonical.lean b/LeanPool/ConwaySoifer/Geometry/Canonical.lean
index 0698a42a63..5c633f34c3 100644
--- a/LeanPool/ConwaySoifer/Geometry/Canonical.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Canonical.lean
@@ -7,7 +7,8 @@ module
 
 public import LeanPool.ConwaySoifer.Geometry.Owners
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.NormNum.Basic
 
 /-!
 # The four normalized contact cases
diff --git a/LeanPool/ConwaySoifer/Geometry/Cap.lean b/LeanPool/ConwaySoifer/Geometry/Cap.lean
index bb34c5a760..6de5d210f2 100644
--- a/LeanPool/ConwaySoifer/Geometry/Cap.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Cap.lean
@@ -9,7 +9,12 @@ public import LeanPool.ConwaySoifer.Geometry.Support
 public import LeanPool.ConwaySoifer.Geometry.Area
 public import Mathlib.MeasureTheory.Measure.Haar.NormedSpace
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # Caps of a triangle cut by a line
diff --git a/LeanPool/ConwaySoifer/Geometry/CornerCap.lean b/LeanPool/ConwaySoifer/Geometry/CornerCap.lean
index 6941089116..88d5da3e1a 100644
--- a/LeanPool/ConwaySoifer/Geometry/CornerCap.lean
+++ b/LeanPool/ConwaySoifer/Geometry/CornerCap.lean
@@ -7,7 +7,12 @@ module
 
 public import LeanPool.ConwaySoifer.Geometry.Cap
 public import LeanPool.ConwaySoifer.Geometry.Canonical
-import Mathlib.Tactic
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.FunProp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # The universal corner cap and the external-midpoint cost
diff --git a/LeanPool/ConwaySoifer/Geometry/Diameter.lean b/LeanPool/ConwaySoifer/Geometry/Diameter.lean
index 651368dde7..7c060c222d 100644
--- a/LeanPool/ConwaySoifer/Geometry/Diameter.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Diameter.lean
@@ -6,7 +6,8 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Geometry.Basic
-import Mathlib.Tactic
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
 
 /-! The convexification argument is adapted from SevenTriangles.Geometry.Diameter,
 commit b17ca52a395519f43fc15f83fb49a5dd69996225, to triangular coordinates,
diff --git a/LeanPool/ConwaySoifer/Geometry/Halfspaces.lean b/LeanPool/ConwaySoifer/Geometry/Halfspaces.lean
index 9a62adf94e..7f16e26121 100644
--- a/LeanPool/ConwaySoifer/Geometry/Halfspaces.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Halfspaces.lean
@@ -6,7 +6,8 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Geometry.Rays
-import Mathlib.Tactic
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
 
 /-!
 Necessary outward-normal conditions for genuine full ray endpoints and strict
diff --git a/LeanPool/ConwaySoifer/Geometry/Locality.lean b/LeanPool/ConwaySoifer/Geometry/Locality.lean
index d920741a57..c49757392b 100644
--- a/LeanPool/ConwaySoifer/Geometry/Locality.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Locality.lean
@@ -6,7 +6,8 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Geometry.Canonical
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
 
 /-!
 # Locality: which owners can meet a boundary segment
diff --git a/LeanPool/ConwaySoifer/Geometry/Normal.lean b/LeanPool/ConwaySoifer/Geometry/Normal.lean
index 210804bc80..a9ee18b6ff 100644
--- a/LeanPool/ConwaySoifer/Geometry/Normal.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Normal.lean
@@ -7,7 +7,7 @@ module
 
 public import LeanPool.ConwaySoifer.Geometry.Symmetry
 public import LeanPool.ConwaySoifer.Geometry.Owners
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
 
 /-!
 # Moving the minimal side section to `vertex 0`
diff --git a/LeanPool/ConwaySoifer/Geometry/Normalization.lean b/LeanPool/ConwaySoifer/Geometry/Normalization.lean
index 1629b2a4a2..cb2810ccd8 100644
--- a/LeanPool/ConwaySoifer/Geometry/Normalization.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Normalization.lean
@@ -8,7 +8,12 @@ module
 public import LeanPool.ConwaySoifer.Geometry.Budget
 public import LeanPool.ConwaySoifer.Geometry.Locality
 public import LeanPool.ConwaySoifer.Geometry.Canonical
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Ring
 
 /-!
 # Geometric normalization: every subunit cover is a canonical contact case
diff --git a/LeanPool/ConwaySoifer/Geometry/Oblique.lean b/LeanPool/ConwaySoifer/Geometry/Oblique.lean
index 24be250251..adb11009b9 100644
--- a/LeanPool/ConwaySoifer/Geometry/Oblique.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Oblique.lean
@@ -7,7 +7,10 @@ module
 
 public import LeanPool.ConwaySoifer.Geometry.Area
 public import LeanPool.ConwaySoifer.SevenTriangles.Geometry.Wedge
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Ring
 
 /-!
 # Bridge to the vendored oblique-coordinate library
diff --git a/LeanPool/ConwaySoifer/Geometry/Owners.lean b/LeanPool/ConwaySoifer/Geometry/Owners.lean
index 048d396142..ccdeb462bf 100644
--- a/LeanPool/ConwaySoifer/Geometry/Owners.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Owners.lean
@@ -7,7 +7,9 @@ module
 
 public import LeanPool.ConwaySoifer.Geometry.TriangleHalfspaces
 public import Mathlib.Data.Fintype.Lattice
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
 
 /-!
 # Owners
diff --git a/LeanPool/ConwaySoifer/Geometry/Rays.lean b/LeanPool/ConwaySoifer/Geometry/Rays.lean
index 8c2f5ff50a..b8d8e27734 100644
--- a/LeanPool/ConwaySoifer/Geometry/Rays.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Rays.lean
@@ -9,7 +9,12 @@ public import LeanPool.ConwaySoifer.Geometry.Diameter
 public import Mathlib.Analysis.Convex.Topology
 public import Mathlib.Topology.Order.Monotone
 public import Mathlib.Topology.Order.DenselyOrdered
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.FunProp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 Full ray sections of the actual closed filled triangles. The transfer theorem
diff --git a/LeanPool/ConwaySoifer/Geometry/ReceiverFacts.lean b/LeanPool/ConwaySoifer/Geometry/ReceiverFacts.lean
index 7b97e0bd55..37a7a346b0 100644
--- a/LeanPool/ConwaySoifer/Geometry/ReceiverFacts.lean
+++ b/LeanPool/ConwaySoifer/Geometry/ReceiverFacts.lean
@@ -6,7 +6,6 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Geometry.Symmetry
-import Mathlib.Tactic
 
 /-! Receiver indices and reflection, extracted from the former SmallS module. -/
 
diff --git a/LeanPool/ConwaySoifer/Geometry/Scaling.lean b/LeanPool/ConwaySoifer/Geometry/Scaling.lean
index c1f30f183c..0491eb4094 100644
--- a/LeanPool/ConwaySoifer/Geometry/Scaling.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Scaling.lean
@@ -6,7 +6,8 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Geometry.Basic
-import Mathlib.Tactic
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
 
 /-! Scaling transfers any proof of the side-three lower bound. -/
 
diff --git a/LeanPool/ConwaySoifer/Geometry/SideFacts.lean b/LeanPool/ConwaySoifer/Geometry/SideFacts.lean
index 4c5b141eb9..289d8bb2b8 100644
--- a/LeanPool/ConwaySoifer/Geometry/SideFacts.lean
+++ b/LeanPool/ConwaySoifer/Geometry/SideFacts.lean
@@ -7,7 +7,12 @@ module
 
 public import LeanPool.ConwaySoifer.Geometry.AcrossFacts
 public import LeanPool.ConwaySoifer.Geometry.ReceiverFacts
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Ring
 
 /-! Shared geometric facts for both small-case proofs; no certificate evaluations. -/
 
diff --git a/LeanPool/ConwaySoifer/Geometry/Support.lean b/LeanPool/ConwaySoifer/Geometry/Support.lean
index 665f8cdc71..a9fbaf8c80 100644
--- a/LeanPool/ConwaySoifer/Geometry/Support.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Support.lean
@@ -8,7 +8,13 @@ module
 public import LeanPool.ConwaySoifer.Geometry.TriangleHalfspaces
 public import Mathlib.Analysis.Real.Sqrt
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.RealSqrt
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # Support forms and orientations of equilateral triangles in triangular coordinates
diff --git a/LeanPool/ConwaySoifer/Geometry/Symmetry.lean b/LeanPool/ConwaySoifer/Geometry/Symmetry.lean
index ff9becdf4e..728498ed0a 100644
--- a/LeanPool/ConwaySoifer/Geometry/Symmetry.lean
+++ b/LeanPool/ConwaySoifer/Geometry/Symmetry.lean
@@ -8,7 +8,10 @@ module
 public import LeanPool.ConwaySoifer.Geometry.Canonical
 public import LeanPool.ConwaySoifer.Geometry.Support
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Ring
 
 /-!
 # The symmetry group of the target triangle
diff --git a/LeanPool/ConwaySoifer/Geometry/TriangleHalfspaces.lean b/LeanPool/ConwaySoifer/Geometry/TriangleHalfspaces.lean
index 6696f5c4ed..d32d8d4d1e 100644
--- a/LeanPool/ConwaySoifer/Geometry/TriangleHalfspaces.lean
+++ b/LeanPool/ConwaySoifer/Geometry/TriangleHalfspaces.lean
@@ -8,7 +8,10 @@ module
 public import LeanPool.ConwaySoifer.Geometry.Halfspaces
 public import Mathlib.Analysis.Convex.Combination
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
 
 /-!
 A filled nondegenerate triangle is exactly an intersection of three explicit
diff --git a/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Area.lean b/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Area.lean
index c6e63cfbdf..76c4456343 100644
--- a/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Area.lean
+++ b/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Area.lean
@@ -15,7 +15,13 @@ public import Mathlib.Topology.Algebra.Module.FiniteDimension
 public import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
 public import Mathlib.LinearAlgebra.Basis.Fin
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.FunProp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # Areas in skew coordinates
diff --git a/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Basic.lean b/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Basic.lean
index 2c751f6e2e..90f4ff9b75 100644
--- a/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Basic.lean
+++ b/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Basic.lean
@@ -8,7 +8,11 @@ module
 public import Mathlib.Analysis.Convex.Hull
 public import Mathlib.Basic.Real.Basic
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.NormNum.RealSqrt
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # Rational coordinates for the covering problem
diff --git a/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Diameter.lean b/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Diameter.lean
index d50835bd8e..a5d4dd288d 100644
--- a/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Diameter.lean
+++ b/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Diameter.lean
@@ -7,7 +7,10 @@ module
 
 public import LeanPool.ConwaySoifer.SevenTriangles.Geometry.Basic
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Ring
 
 /-! Diameter bounds for the filled convex hull, in the project's Euclidean coordinates. -/
 
diff --git a/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Support.lean b/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Support.lean
index 30ad3d735d..0780ad2f40 100644
--- a/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Support.lean
+++ b/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Support.lean
@@ -7,7 +7,14 @@ module
 
 public import LeanPool.ConwaySoifer.SevenTriangles.Geometry.Basic
 public import Mathlib.Analysis.Real.Sqrt
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.NormNum.RealSqrt
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # Algebra of support forms
diff --git a/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Wedge.lean b/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Wedge.lean
index fc265e2971..783a502356 100644
--- a/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Wedge.lean
+++ b/LeanPool/ConwaySoifer/SevenTriangles/Geometry/Wedge.lean
@@ -7,7 +7,14 @@ module
 
 public import LeanPool.ConwaySoifer.SevenTriangles.Geometry.Area
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.FunProp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.LinearCombination
+import Mathlib.Tactic.NormNum.RealSqrt
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # The 120-degree wedge and the area-loss lemma
diff --git a/LeanPool/ConwaySoifer/Simplified/Certificates/AllChecked.lean b/LeanPool/ConwaySoifer/Simplified/Certificates/AllChecked.lean
index c262666aba..9ee36e86df 100644
--- a/LeanPool/ConwaySoifer/Simplified/Certificates/AllChecked.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Certificates/AllChecked.lean
@@ -106,8 +106,6 @@ public import LeanPool.ConwaySoifer.Simplified.Certificates.Checked.Across102500
 public import LeanPool.ConwaySoifer.Simplified.Certificates.Checked.Across107500112500
 public import LeanPool.ConwaySoifer.Simplified.Certificates.Checked.Across112500117500
 public import LeanPool.ConwaySoifer.Simplified.Certificates.Checked.Across117500122500
-import Mathlib.Tactic
-import Mathlib.Tactic.FinCases
 
 /-!
 # AllChecked
diff --git a/LeanPool/ConwaySoifer/Simplified/Certificates/AllData.lean b/LeanPool/ConwaySoifer/Simplified/Certificates/AllData.lean
index 7d36925143..286f166bff 100644
--- a/LeanPool/ConwaySoifer/Simplified/Certificates/AllData.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Certificates/AllData.lean
@@ -105,7 +105,6 @@ public import LeanPool.ConwaySoifer.Simplified.Certificates.Data.Across102500107
 public import LeanPool.ConwaySoifer.Simplified.Certificates.Data.Across107500112500
 public import LeanPool.ConwaySoifer.Simplified.Certificates.Data.Across112500117500
 public import LeanPool.ConwaySoifer.Simplified.Certificates.Data.Across117500122500
-import Mathlib.Tactic
 
 /-!
 # AllData
diff --git a/LeanPool/ConwaySoifer/Simplified/Certificates/Coverage.lean b/LeanPool/ConwaySoifer/Simplified/Certificates/Coverage.lean
index ce97683b01..ef8d7d81ec 100644
--- a/LeanPool/ConwaySoifer/Simplified/Certificates/Coverage.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Certificates/Coverage.lean
@@ -7,7 +7,8 @@ module
 
 public import LeanPool.ConwaySoifer.Certificates.IntervalCover
 public import LeanPool.ConwaySoifer.Simplified.Certificates.AllChecked
-import Mathlib.Tactic
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
 
 /-! Exact half-open interval cover for the third-pass selection only. -/
 
diff --git a/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1200001300000.lean b/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1200001300000.lean
index 39d50fc87b..e9f7ac79a7 100644
--- a/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1200001300000.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1200001300000.lean
@@ -547,6 +547,13 @@ theorem next2 : model2.insert step2 = model3 := by
   apply Model.ext_fields
   all_goals intro j; fin_cases j <;> decide +kernel
 
+-- Limit kernel memory by checking this fan tail separately.
+private theorem checkedFan3Owner0Part0 :
+    fan3Owner0Part0.check (model3.B 0 ++ [step3.q]) 9000000000000
+      (model3.caps 0) 0 1 100 12
+      ([313200000000, 2610000000000], [313200000000, 2610000000000]) = true := by
+  decide +kernel
+
 theorem excluded3_0 : ExcludedOn (model3.B 0 ++ [step3.q]) 9000000000000 (model3.caps 0) (model3.ord
     0) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([1393200000000, 2610000000000], [313200000000,
@@ -558,7 +565,12 @@ theorem excluded3_0 : ExcludedOn (model3.B 0 ++ [step3.q]) 9000000000000 (model3
       (some (7, 1, 7)) fan3Owner0Part0)))))) (den := 9000000000000) (fuel := 12) (by decide +kernel)
       0 1
       100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan3Owner0Part0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded3_1 : ExcludedOn (model3.B 1 ++ [step3.q]) 9000000000000 (model3.caps 1) (model3.ord
     1) 0 1 100 := by
@@ -649,6 +661,13 @@ theorem next3 : model3.insert step3 = model4 := by
   apply Model.ext_fields
   all_goals intro j; fin_cases j <;> decide +kernel
 
+-- Limit kernel memory by checking this fan tail separately.
+private theorem checkedFan4Owner0Part0 :
+    fan4Owner0Part0.check (model4.B 0 ++ [step4.q]) 9000000000000
+      (model4.caps 0) 0 1 100 12
+      ([7186800000000, -2610000000000], [1706400000000, 5220000000000]) = true := by
+  decide +kernel
+
 theorem excluded4_0 : ExcludedOn (model4.B 0 ++ [step4.q]) 9000000000000 (model4.caps 0) (model4.ord
     0) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([7813200000000, 2610000000000], [453600000000,
@@ -661,7 +680,12 @@ theorem excluded4_0 : ExcludedOn (model4.B 0 ++ [step4.q]) 9000000000000 (model4
       5220000000000]) (some (6, 1, 7)) (some (6, 1, 7)) fan4Owner0Part0)))))))) (den :=
       9000000000000) (fuel := 12) (by decide +kernel) 0
       1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan4Owner0Part0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded4_1 : ExcludedOn (model4.B 1 ++ [step4.q]) 9000000000000 (model4.caps 1) (model4.ord
     1) 0 1 100 := by
@@ -755,6 +779,13 @@ theorem next4 : model4.insert step4 = model5 := by
   apply Model.ext_fields
   all_goals intro j; fin_cases j <;> decide +kernel
 
+-- Limit kernel memory by checking this fan tail separately.
+private theorem checkedFan5Owner0Part0 :
+    fan5Owner0Part0.check (model5.B 0 ++ [step5.q]) 9000000000000
+      (model5.caps 0) 0 1 100 12
+      ([7093200000000, 2610000000000], [2533200000000, 2610000000000]) = true := by
+  decide +kernel
+
 theorem excluded5_0 : ExcludedOn (model5.B 0 ++ [step5.q]) 9000000000000 (model5.caps 0) (model5.ord
     0) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([6780000000000], [1140000000000]) (some (6, 1,
@@ -764,7 +795,12 @@ theorem excluded5_0 : ExcludedOn (model5.B 0 ++ [step5.q]) 9000000000000 (model5
       (some (6, 1, 7)) (some (6, 1, 7)) (.next ([7093200000000, 2610000000000], [2533200000000,
       2610000000000]) (some (6, 1, 7)) (some (6, 1, 7)) fan5Owner0Part0)))))) (den :=
       9000000000000) (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan5Owner0Part0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded5_1 : ExcludedOn (model5.B 1 ++ [step5.q]) 9000000000000 (model5.caps 1) (model5.ord
     1) 0 1 100 := by
@@ -910,6 +946,66 @@ theorem next6 : model6.insert step6 = model7 := by
   apply Model.ext_fields
   all_goals intro j; fin_cases j <;> decide +kernel
 
+-- Verify the shared tails in one proof to bound the kernel working set.
+private theorem checkedFan7Owner0Part3Checks :
+    (fan7Owner0Part0.check (model7.B 0 ++ [step7.q]) 9000000000000
+      (model7.caps 0) 0 3836 15494700 12
+      ([116400000000, 5220000000000], [196800000000, -2610000000000]) = true) ∧
+    (fan7Owner0Part1.check (model7.B 0 ++ [step7.q]) 9000000000000
+      (model7.caps 0) 3836 60106 15494700 12
+      ([626400000000, 5220000000000], [766800000000, -2610000000000]) = true) ∧
+    (fan7Owner0Part2.check (model7.B 0 ++ [step7.q]) 9000000000000
+      (model7.caps 0) 60106 116376 15494700 12
+      ([626400000000, 5220000000000], [766800000000, -2610000000000]) = true) ∧
+    (fan7Owner0Part3.check (model7.B 0 ++ [step7.q]) 9000000000000
+      (model7.caps 0) 2984 3973 397300 12
+      ([6705000000000], [2805000000000]) = true) := by
+  have checkedTail0 :
+      fan7Owner0Part0.check (model7.B 0 ++ [step7.q]) 9000000000000
+        (model7.caps 0) 0 3836 15494700 12
+        ([116400000000, 5220000000000], [196800000000, -2610000000000]) = true := by
+    decide +kernel
+  have checkedTail1 :
+      fan7Owner0Part1.check (model7.B 0 ++ [step7.q]) 9000000000000
+        (model7.caps 0) 3836 60106 15494700 12
+        ([626400000000, 5220000000000], [766800000000, -2610000000000]) = true := by
+    decide +kernel
+  have checkedTail2 :
+      fan7Owner0Part2.check (model7.B 0 ++ [step7.q]) 9000000000000
+        (model7.caps 0) 60106 116376 15494700 12
+        ([626400000000, 5220000000000], [766800000000, -2610000000000]) = true := by
+    decide +kernel
+  have checkedTail3 :
+      fan7Owner0Part3.check (model7.B 0 ++ [step7.q]) 9000000000000
+        (model7.caps 0) 2984 3973 397300 12
+        ([6705000000000], [2805000000000]) = true := by
+    decide +kernel
+  exact ⟨checkedTail0, checkedTail1, checkedTail2, checkedTail3⟩
+
+private theorem checkedFan7Owner0Part0 :
+    fan7Owner0Part0.check (model7.B 0 ++ [step7.q]) 9000000000000
+      (model7.caps 0) 0 3836 15494700 12
+      ([116400000000, 5220000000000], [196800000000, -2610000000000]) = true := by
+  exact checkedFan7Owner0Part3Checks.1
+
+private theorem checkedFan7Owner0Part1 :
+    fan7Owner0Part1.check (model7.B 0 ++ [step7.q]) 9000000000000
+      (model7.caps 0) 3836 60106 15494700 12
+      ([626400000000, 5220000000000], [766800000000, -2610000000000]) = true := by
+  exact checkedFan7Owner0Part3Checks.2.1
+
+private theorem checkedFan7Owner0Part2 :
+    fan7Owner0Part2.check (model7.B 0 ++ [step7.q]) 9000000000000
+      (model7.caps 0) 60106 116376 15494700 12
+      ([626400000000, 5220000000000], [766800000000, -2610000000000]) = true := by
+  exact checkedFan7Owner0Part3Checks.2.2.1
+
+private theorem checkedFan7Owner0Part3 :
+    fan7Owner0Part3.check (model7.B 0 ++ [step7.q]) 9000000000000
+      (model7.caps 0) 2984 3973 397300 12
+      ([6705000000000], [2805000000000]) = true := by
+  exact checkedFan7Owner0Part3Checks.2.2.2
+
 theorem excluded7_0 : ExcludedOn (model7.B 0 ++ [step7.q]) 9000000000000 (model7.caps 0) (model7.ord
     0) 0 1 100 := by
   apply ExclusionHint.sound (.split (0) (2984) (3973) (397300) (.split (0) (3836) (116376)
@@ -977,7 +1073,13 @@ theorem excluded7_0 : ExcludedOn (model7.B 0 ++ [step7.q]) 9000000000000 (model7
       (some (7, 1, 4)) (some (7, 1, 4)) fan7Owner0Part3))))))))))) (den := 9000000000000) (fuel :=
       12)
       (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan7Owner0Part0, checkedFan7Owner0Part1, checkedFan7Owner0Part2,
+      checkedFan7Owner0Part3,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded7_1 : ExcludedOn (model7.B 1 ++ [step7.q]) 9000000000000 (model7.caps 1) (model7.ord
     1) 0 1 100 := by
diff --git a/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1500001600003.lean b/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1500001600003.lean
index 3f581af25b..a1f76f0e40 100644
--- a/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1500001600003.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1500001600003.lean
@@ -688,12 +688,89 @@ def fan30Owner4Part0 : FanWitness := (.next ([3825000000000], [5400000000000]) (
     4)) (.next ([-4725000000000], [5475000000000]) (some (6, 2, 4)) (some (6, 2, 4)) (.terminal
     (some (6, 2, 4)) (some (0, 2, 6)) (some (6, 2, 6)))))))))))))))))))))))))))
 
+-- Verify the shared tails in one proof to bound the kernel working set.
+private theorem checkedFan24Owner0Part3Checks :
+    (fan24Owner0Part0.check (model24.B 0 ++ [step24.q]) 9000000000000
+      (model24.caps 0) 0 1 100 12
+      ([-1005000000000], [2880000000000]) = true) ∧
+    (fan24Owner0Part1.check (model24.B 0 ++ [step24.q]) 9000000000000
+      (model24.caps 0) 0 1 100 12
+      ([0, 0], [1134000000000, 7560000000000]) = true) ∧
+    (fan24Owner0Part2.check (model24.B 0 ++ [step24.q]) 9000000000000
+      (model24.caps 0) 0 1 100 12
+      ([3075000000000], [2100000000000]) = true) ∧
+    (fan24Owner0Part3.check (model24.B 0 ++ [step24.q]) 9000000000000
+      (model24.caps 0) 0 1 100 12
+      ([4275000000000], [45000000000]) = true) := by
+  have checkedTail0 :
+      fan24Owner0Part0.check (model24.B 0 ++ [step24.q]) 9000000000000
+        (model24.caps 0) 0 1 100 12
+        ([-1005000000000], [2880000000000]) = true := by
+    decide +kernel
+  have checkedTail1 :
+      fan24Owner0Part1.check (model24.B 0 ++ [step24.q]) 9000000000000
+        (model24.caps 0) 0 1 100 12
+        ([0, 0], [1134000000000, 7560000000000]) = true := by
+    delta fan24Owner0Part1
+    simp only [FanWitness.check, checkedTail0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail2 :
+      fan24Owner0Part2.check (model24.B 0 ++ [step24.q]) 9000000000000
+        (model24.caps 0) 0 1 100 12
+        ([3075000000000], [2100000000000]) = true := by
+    delta fan24Owner0Part2
+    simp only [FanWitness.check, checkedTail1,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail3 :
+      fan24Owner0Part3.check (model24.B 0 ++ [step24.q]) 9000000000000
+        (model24.caps 0) 0 1 100 12
+        ([4275000000000], [45000000000]) = true := by
+    delta fan24Owner0Part3
+    simp only [FanWitness.check, checkedTail2,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  exact ⟨checkedTail0, checkedTail1, checkedTail2, checkedTail3⟩
+
+private theorem checkedFan24Owner0Part0 :
+    fan24Owner0Part0.check (model24.B 0 ++ [step24.q]) 9000000000000
+      (model24.caps 0) 0 1 100 12
+      ([-1005000000000], [2880000000000]) = true := by
+  exact checkedFan24Owner0Part3Checks.1
+
+private theorem checkedFan24Owner0Part1 :
+    fan24Owner0Part1.check (model24.B 0 ++ [step24.q]) 9000000000000
+      (model24.caps 0) 0 1 100 12
+      ([0, 0], [1134000000000, 7560000000000]) = true := by
+  exact checkedFan24Owner0Part3Checks.2.1
+
+private theorem checkedFan24Owner0Part2 :
+    fan24Owner0Part2.check (model24.B 0 ++ [step24.q]) 9000000000000
+      (model24.caps 0) 0 1 100 12
+      ([3075000000000], [2100000000000]) = true := by
+  exact checkedFan24Owner0Part3Checks.2.2.1
+
+private theorem checkedFan24Owner0Part3 :
+    fan24Owner0Part3.check (model24.B 0 ++ [step24.q]) 9000000000000
+      (model24.caps 0) 0 1 100 12
+      ([4275000000000], [45000000000]) = true := by
+  exact checkedFan24Owner0Part3Checks.2.2.2
+
 theorem excluded24_0 : ExcludedOn (model24.B 0 ++ [step24.q]) 9000000000000 (model24.caps 0)
     (model24.ord 0) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([4275000000000], [45000000000]) (some (11, 2, 6))
       (some (11, 2, 6)) fan24Owner0Part3))
       (den := 9000000000000) (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan24Owner0Part3,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded24_1 : ExcludedOn (model24.B 1 ++ [step24.q]) 9000000000000 (model24.caps 1)
     (model24.ord 1) 0 1 100 := by
@@ -707,6 +784,13 @@ theorem excluded24_2 : ExcludedOn (model24.B 2 ++ [step24.q]) 9000000000000 (mod
       100 (by decide +kernel)
   decide +kernel
 
+-- Limit kernel memory by checking this fan tail separately.
+private theorem checkedFan24Owner4Part0 :
+    fan24Owner4Part0.check (model24.B 4 ++ [step24.q]) 9000000000000
+      (model24.caps 4) 0 1 100 12
+      ([4875000000000], [3450000000000, -9000000000000]) = true := by
+  decide +kernel
+
 theorem excluded24_4 : ExcludedOn (model24.B 4 ++ [step24.q]) 9000000000000 (model24.caps 4)
     (model24.ord 4) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([4725000000000, 0], [225000000000,
@@ -720,7 +804,12 @@ theorem excluded24_4 : ExcludedOn (model24.B 4 ++ [step24.q]) 9000000000000 (mod
       1, 6)) (.next ([4875000000000], [3450000000000, -9000000000000]) (some (4, 1, 6)) (some (4, 1,
       6)) fan24Owner4Part0)))))))))) (den := 9000000000000) (fuel := 12) (by decide +kernel)
       0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan24Owner4Part0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded24_5 : ExcludedOn (model24.B 5 ++ [step24.q]) 9000000000000 (model24.caps 5)
     (model24.ord 5) 0 1 100 := by
@@ -848,6 +937,78 @@ theorem next25 : model25.insert step25 = model26 := by
   apply Model.ext_fields
   all_goals intro j; fin_cases j <;> decide +kernel
 
+-- Verify the shared tails in one proof to bound the kernel working set.
+private theorem checkedFan26Owner0Part3Checks :
+    (fan26Owner0Part0.check (model26.B 0 ++ [step26.q]) 9000000000000
+      (model26.caps 0) 0 1 100 12
+      ([-3000000000000], [9450000000000]) = true) ∧
+    (fan26Owner0Part1.check (model26.B 0 ++ [step26.q]) 9000000000000
+      (model26.caps 0) 0 1 100 12
+      ([-45000000000], [4320000000000]) = true) ∧
+    (fan26Owner0Part2.check (model26.B 0 ++ [step26.q]) 9000000000000
+      (model26.caps 0) 0 1 100 12
+      ([1875000000000], [1005000000000]) = true) ∧
+    (fan26Owner0Part3.check (model26.B 0 ++ [step26.q]) 9000000000000
+      (model26.caps 0) 0 1 100 12
+      ([2250000000000], [45000000000]) = true) := by
+  have checkedTail0 :
+      fan26Owner0Part0.check (model26.B 0 ++ [step26.q]) 9000000000000
+        (model26.caps 0) 0 1 100 12
+        ([-3000000000000], [9450000000000]) = true := by
+    decide +kernel
+  have checkedTail1 :
+      fan26Owner0Part1.check (model26.B 0 ++ [step26.q]) 9000000000000
+        (model26.caps 0) 0 1 100 12
+        ([-45000000000], [4320000000000]) = true := by
+    delta fan26Owner0Part1
+    simp only [FanWitness.check, checkedTail0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail2 :
+      fan26Owner0Part2.check (model26.B 0 ++ [step26.q]) 9000000000000
+        (model26.caps 0) 0 1 100 12
+        ([1875000000000], [1005000000000]) = true := by
+    delta fan26Owner0Part2
+    simp only [FanWitness.check, checkedTail1,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail3 :
+      fan26Owner0Part3.check (model26.B 0 ++ [step26.q]) 9000000000000
+        (model26.caps 0) 0 1 100 12
+        ([2250000000000], [45000000000]) = true := by
+    delta fan26Owner0Part3
+    simp only [FanWitness.check, checkedTail2,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  exact ⟨checkedTail0, checkedTail1, checkedTail2, checkedTail3⟩
+
+private theorem checkedFan26Owner0Part0 :
+    fan26Owner0Part0.check (model26.B 0 ++ [step26.q]) 9000000000000
+      (model26.caps 0) 0 1 100 12
+      ([-3000000000000], [9450000000000]) = true := by
+  exact checkedFan26Owner0Part3Checks.1
+
+private theorem checkedFan26Owner0Part1 :
+    fan26Owner0Part1.check (model26.B 0 ++ [step26.q]) 9000000000000
+      (model26.caps 0) 0 1 100 12
+      ([-45000000000], [4320000000000]) = true := by
+  exact checkedFan26Owner0Part3Checks.2.1
+
+private theorem checkedFan26Owner0Part2 :
+    fan26Owner0Part2.check (model26.B 0 ++ [step26.q]) 9000000000000
+      (model26.caps 0) 0 1 100 12
+      ([1875000000000], [1005000000000]) = true := by
+  exact checkedFan26Owner0Part3Checks.2.2.1
+
+private theorem checkedFan26Owner0Part3 :
+    fan26Owner0Part3.check (model26.B 0 ++ [step26.q]) 9000000000000
+      (model26.caps 0) 0 1 100 12
+      ([2250000000000], [45000000000]) = true := by
+  exact checkedFan26Owner0Part3Checks.2.2.2
+
 theorem excluded26_0 : ExcludedOn (model26.B 0 ++ [step26.q]) 9000000000000 (model26.caps 0)
     (model26.ord 0) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([4275000000000], [45000000000]) (some (11, 2, 6))
@@ -855,7 +1016,12 @@ theorem excluded26_0 : ExcludedOn (model26.B 0 ++ [step26.q]) 9000000000000 (mod
       (.next ([2250000000000], [45000000000]) (some (11, 2, 6)) (some (11, 2, 6))
       fan26Owner0Part3))))
       (den := 9000000000000) (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan26Owner0Part3,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded26_1 : ExcludedOn (model26.B 1 ++ [step26.q]) 9000000000000 (model26.caps 1)
     (model26.ord 1) 0 1 100 := by
@@ -946,6 +1112,60 @@ theorem next26 : model26.insert step26 = model27 := by
   apply Model.ext_fields
   all_goals intro j; fin_cases j <;> decide +kernel
 
+-- Verify the shared tails in one proof to bound the kernel working set.
+private theorem checkedFan27Owner0Part2Checks :
+    (fan27Owner0Part0.check (model27.B 0 ++ [step27.q]) 9000000000000
+      (model27.caps 0) 0 1 100 12
+      ([-2025000000000], [8700000000000]) = true) ∧
+    (fan27Owner0Part1.check (model27.B 0 ++ [step27.q]) 9000000000000
+      (model27.caps 0) 0 1 100 12
+      ([705000000000], [5295000000000]) = true) ∧
+    (fan27Owner0Part2.check (model27.B 0 ++ [step27.q]) 9000000000000
+      (model27.caps 0) 0 1 100 12
+      ([7275000000000], [1725000000000]) = true) := by
+  have checkedTail0 :
+      fan27Owner0Part0.check (model27.B 0 ++ [step27.q]) 9000000000000
+        (model27.caps 0) 0 1 100 12
+        ([-2025000000000], [8700000000000]) = true := by
+    decide +kernel
+  have checkedTail1 :
+      fan27Owner0Part1.check (model27.B 0 ++ [step27.q]) 9000000000000
+        (model27.caps 0) 0 1 100 12
+        ([705000000000], [5295000000000]) = true := by
+    delta fan27Owner0Part1
+    simp only [FanWitness.check, checkedTail0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail2 :
+      fan27Owner0Part2.check (model27.B 0 ++ [step27.q]) 9000000000000
+        (model27.caps 0) 0 1 100 12
+        ([7275000000000], [1725000000000]) = true := by
+    delta fan27Owner0Part2
+    simp only [FanWitness.check, checkedTail1,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  exact ⟨checkedTail0, checkedTail1, checkedTail2⟩
+
+private theorem checkedFan27Owner0Part0 :
+    fan27Owner0Part0.check (model27.B 0 ++ [step27.q]) 9000000000000
+      (model27.caps 0) 0 1 100 12
+      ([-2025000000000], [8700000000000]) = true := by
+  exact checkedFan27Owner0Part2Checks.1
+
+private theorem checkedFan27Owner0Part1 :
+    fan27Owner0Part1.check (model27.B 0 ++ [step27.q]) 9000000000000
+      (model27.caps 0) 0 1 100 12
+      ([705000000000], [5295000000000]) = true := by
+  exact checkedFan27Owner0Part2Checks.2.1
+
+private theorem checkedFan27Owner0Part2 :
+    fan27Owner0Part2.check (model27.B 0 ++ [step27.q]) 9000000000000
+      (model27.caps 0) 0 1 100 12
+      ([7275000000000], [1725000000000]) = true := by
+  exact checkedFan27Owner0Part2Checks.2.2
+
 theorem excluded27_0 : ExcludedOn (model27.B 0 ++ [step27.q]) 9000000000000 (model27.caps 0)
     (model27.ord 0) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([4275000000000], [45000000000]) (some (7, 2, 11))
@@ -967,7 +1187,12 @@ theorem excluded27_0 : ExcludedOn (model27.B 0 ++ [step27.q]) 9000000000000 (mod
       ([7275000000000], [1725000000000]) (some (10, 2, 11)) (some (10, 2, 11))
       fan27Owner0Part2))))))))))))))))))
       (den := 9000000000000) (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan27Owner0Part2,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded27_1 : ExcludedOn (model27.B 1 ++ [step27.q]) 9000000000000 (model27.caps 1)
     (model27.ord 1) 0 1 100 := by
@@ -1063,6 +1288,60 @@ theorem next27 : model27.insert step27 = model28 := by
   apply Model.ext_fields
   all_goals intro j; fin_cases j <;> decide +kernel
 
+-- Verify the shared tails in one proof to bound the kernel working set.
+private theorem checkedFan28Owner0Part2Checks :
+    (fan28Owner0Part0.check (model28.B 0 ++ [step28.q]) 9000000000000
+      (model28.caps 0) 0 1 100 12
+      ([-1800000000000], [7500000000000]) = true) ∧
+    (fan28Owner0Part1.check (model28.B 0 ++ [step28.q]) 9000000000000
+      (model28.caps 0) 0 1 100 12
+      ([150000000000], [7050000000000]) = true) ∧
+    (fan28Owner0Part2.check (model28.B 0 ++ [step28.q]) 9000000000000
+      (model28.caps 0) 0 1 100 12
+      ([5700000000000], [1800000000000]) = true) := by
+  have checkedTail0 :
+      fan28Owner0Part0.check (model28.B 0 ++ [step28.q]) 9000000000000
+        (model28.caps 0) 0 1 100 12
+        ([-1800000000000], [7500000000000]) = true := by
+    decide +kernel
+  have checkedTail1 :
+      fan28Owner0Part1.check (model28.B 0 ++ [step28.q]) 9000000000000
+        (model28.caps 0) 0 1 100 12
+        ([150000000000], [7050000000000]) = true := by
+    delta fan28Owner0Part1
+    simp only [FanWitness.check, checkedTail0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail2 :
+      fan28Owner0Part2.check (model28.B 0 ++ [step28.q]) 9000000000000
+        (model28.caps 0) 0 1 100 12
+        ([5700000000000], [1800000000000]) = true := by
+    delta fan28Owner0Part2
+    simp only [FanWitness.check, checkedTail1,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  exact ⟨checkedTail0, checkedTail1, checkedTail2⟩
+
+private theorem checkedFan28Owner0Part0 :
+    fan28Owner0Part0.check (model28.B 0 ++ [step28.q]) 9000000000000
+      (model28.caps 0) 0 1 100 12
+      ([-1800000000000], [7500000000000]) = true := by
+  exact checkedFan28Owner0Part2Checks.1
+
+private theorem checkedFan28Owner0Part1 :
+    fan28Owner0Part1.check (model28.B 0 ++ [step28.q]) 9000000000000
+      (model28.caps 0) 0 1 100 12
+      ([150000000000], [7050000000000]) = true := by
+  exact checkedFan28Owner0Part2Checks.2.1
+
+private theorem checkedFan28Owner0Part2 :
+    fan28Owner0Part2.check (model28.B 0 ++ [step28.q]) 9000000000000
+      (model28.caps 0) 0 1 100 12
+      ([5700000000000], [1800000000000]) = true := by
+  exact checkedFan28Owner0Part2Checks.2.2
+
 theorem excluded28_0 : ExcludedOn (model28.B 0 ++ [step28.q]) 9000000000000 (model28.caps 0)
     (model28.ord 0) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([4275000000000], [45000000000]) (some (7, 2, 11))
@@ -1090,7 +1369,12 @@ theorem excluded28_0 : ExcludedOn (model28.B 0 ++ [step28.q]) 9000000000000 (mod
       (some (10, 2, 11)) (some (10, 2, 11)) (.next ([5700000000000], [1800000000000]) (some (10, 2,
       11)) (some (10, 2, 11)) fan28Owner0Part2))))))))))))))))))))))))
       (den := 9000000000000) (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan28Owner0Part2,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded28_1 : ExcludedOn (model28.B 1 ++ [step28.q]) 9000000000000 (model28.caps 1)
     (model28.ord 1) 0 1 100 := by
@@ -1186,6 +1470,147 @@ theorem next28 : model28.insert step28 = model29 := by
   apply Model.ext_fields
   all_goals intro j; fin_cases j <;> decide +kernel
 
+-- Verify the shared tails in one proof to bound the kernel working set.
+private theorem checkedFan29Owner0Part7Checks :
+    (fan29Owner0Part0.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 0 485 95100 12
+      ([-3900000000000], [9750000000000]) = true) ∧
+    (fan29Owner0Part1.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 0 485 95100 12
+      ([-45000000000], [4320000000000]) = true) ∧
+    (fan29Owner0Part2.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 0 485 95100 12
+      ([2997000000000, -2520000000000], [2106000000000, 5040000000000]) = true) ∧
+    (fan29Owner0Part3.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 0 485 95100 12
+      ([2250000000000], [45000000000]) = true) ∧
+    (fan29Owner0Part4.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 485 951 95100 12
+      ([-3828000000000, -2520000000000], [9756000000000, 5040000000000]) = true) ∧
+    (fan29Owner0Part5.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 485 951 95100 12
+      ([-192000000000, 2520000000000], [6948000000000, 2520000000000]) = true) ∧
+    (fan29Owner0Part6.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 485 951 95100 12
+      ([5100000000000], [4200000000000]) = true) ∧
+    (fan29Owner0Part7.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 485 951 95100 12
+      ([6156000000000, 5040000000000], [972000000000, -2520000000000]) = true) := by
+  have checkedTail0 :
+      fan29Owner0Part0.check (model29.B 0 ++ [step29.q]) 9000000000000
+        (model29.caps 0) 0 485 95100 12
+        ([-3900000000000], [9750000000000]) = true := by
+    decide +kernel
+  have checkedTail1 :
+      fan29Owner0Part1.check (model29.B 0 ++ [step29.q]) 9000000000000
+        (model29.caps 0) 0 485 95100 12
+        ([-45000000000], [4320000000000]) = true := by
+    delta fan29Owner0Part1
+    simp only [FanWitness.check, checkedTail0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail2 :
+      fan29Owner0Part2.check (model29.B 0 ++ [step29.q]) 9000000000000
+        (model29.caps 0) 0 485 95100 12
+        ([2997000000000, -2520000000000], [2106000000000, 5040000000000]) = true := by
+    delta fan29Owner0Part2
+    simp only [FanWitness.check, checkedTail1,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail3 :
+      fan29Owner0Part3.check (model29.B 0 ++ [step29.q]) 9000000000000
+        (model29.caps 0) 0 485 95100 12
+        ([2250000000000], [45000000000]) = true := by
+    delta fan29Owner0Part3
+    simp only [FanWitness.check, checkedTail2,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail4 :
+      fan29Owner0Part4.check (model29.B 0 ++ [step29.q]) 9000000000000
+        (model29.caps 0) 485 951 95100 12
+        ([-3828000000000, -2520000000000], [9756000000000, 5040000000000]) = true := by
+    decide +kernel
+  have checkedTail5 :
+      fan29Owner0Part5.check (model29.B 0 ++ [step29.q]) 9000000000000
+        (model29.caps 0) 485 951 95100 12
+        ([-192000000000, 2520000000000], [6948000000000, 2520000000000]) = true := by
+    delta fan29Owner0Part5
+    simp only [FanWitness.check, checkedTail4,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail6 :
+      fan29Owner0Part6.check (model29.B 0 ++ [step29.q]) 9000000000000
+        (model29.caps 0) 485 951 95100 12
+        ([5100000000000], [4200000000000]) = true := by
+    delta fan29Owner0Part6
+    simp only [FanWitness.check, checkedTail5,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail7 :
+      fan29Owner0Part7.check (model29.B 0 ++ [step29.q]) 9000000000000
+        (model29.caps 0) 485 951 95100 12
+        ([6156000000000, 5040000000000], [972000000000, -2520000000000]) = true := by
+    delta fan29Owner0Part7
+    simp only [FanWitness.check, checkedTail6,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  exact ⟨checkedTail0, checkedTail1, checkedTail2, checkedTail3, checkedTail4, checkedTail5,
+    checkedTail6, checkedTail7⟩
+
+private theorem checkedFan29Owner0Part0 :
+    fan29Owner0Part0.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 0 485 95100 12
+      ([-3900000000000], [9750000000000]) = true := by
+  exact checkedFan29Owner0Part7Checks.1
+
+private theorem checkedFan29Owner0Part1 :
+    fan29Owner0Part1.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 0 485 95100 12
+      ([-45000000000], [4320000000000]) = true := by
+  exact checkedFan29Owner0Part7Checks.2.1
+
+private theorem checkedFan29Owner0Part2 :
+    fan29Owner0Part2.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 0 485 95100 12
+      ([2997000000000, -2520000000000], [2106000000000, 5040000000000]) = true := by
+  exact checkedFan29Owner0Part7Checks.2.2.1
+
+private theorem checkedFan29Owner0Part3 :
+    fan29Owner0Part3.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 0 485 95100 12
+      ([2250000000000], [45000000000]) = true := by
+  exact checkedFan29Owner0Part7Checks.2.2.2.1
+
+private theorem checkedFan29Owner0Part4 :
+    fan29Owner0Part4.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 485 951 95100 12
+      ([-3828000000000, -2520000000000], [9756000000000, 5040000000000]) = true := by
+  exact checkedFan29Owner0Part7Checks.2.2.2.2.1
+
+private theorem checkedFan29Owner0Part5 :
+    fan29Owner0Part5.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 485 951 95100 12
+      ([-192000000000, 2520000000000], [6948000000000, 2520000000000]) = true := by
+  exact checkedFan29Owner0Part7Checks.2.2.2.2.2.1
+
+private theorem checkedFan29Owner0Part6 :
+    fan29Owner0Part6.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 485 951 95100 12
+      ([5100000000000], [4200000000000]) = true := by
+  exact checkedFan29Owner0Part7Checks.2.2.2.2.2.2.1
+
+private theorem checkedFan29Owner0Part7 :
+    fan29Owner0Part7.check (model29.B 0 ++ [step29.q]) 9000000000000
+      (model29.caps 0) 485 951 95100 12
+      ([6156000000000, 5040000000000], [972000000000, -2520000000000]) = true := by
+  exact checkedFan29Owner0Part7Checks.2.2.2.2.2.2.2
+
 theorem excluded29_0 : ExcludedOn (model29.B 0 ++ [step29.q]) 9000000000000 (model29.caps 0)
     (model29.ord 0) 0 1 100 := by
   apply ExclusionHint.sound (.split (0) (485) (951) (95100) (.witnessedFan (.next ([4275000000000],
@@ -1204,7 +1629,12 @@ theorem excluded29_0 : ExcludedOn (model29.B 0 ++ [step29.q]) 9000000000000 (mod
       2, 11)) (.next ([6156000000000, 5040000000000], [972000000000, -2520000000000]) (some (10, 2,
       11)) (some (10, 2, 11)) fan29Owner0Part7)))))))))))))
       (den := 9000000000000) (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan29Owner0Part3, checkedFan29Owner0Part7,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded29_1 : ExcludedOn (model29.B 1 ++ [step29.q]) 9000000000000 (model29.caps 1)
     (model29.ord 1) 0 1 100 := by
@@ -1299,6 +1729,13 @@ theorem excluded30_3 : ExcludedOn (model30.B 3 ++ [step30.q]) 9000000000000 (mod
       100 (by decide +kernel)
   decide +kernel
 
+-- Limit kernel memory by checking this fan tail separately.
+private theorem checkedFan30Owner4Part0 :
+    fan30Owner4Part0.check (model30.B 4 ++ [step30.q]) 9000000000000
+      (model30.caps 4) 0 1 100 12
+      ([1350000000000, 9000000000000], [1350000000000, 9000000000000]) = true := by
+  decide +kernel
+
 theorem excluded30_4 : ExcludedOn (model30.B 4 ++ [step30.q]) 9000000000000 (model30.caps 4)
     (model30.ord 4) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([4725000000000, 0], [225000000000,
@@ -1313,7 +1750,12 @@ theorem excluded30_4 : ExcludedOn (model30.B 4 ++ [step30.q]) 9000000000000 (mod
       9000000000000]) (some (6, 1, 3)) (some (6, 1, 3)) fan30Owner4Part0)))))))))) (den :=
       9000000000000) (fuel := 12)
       (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan30Owner4Part0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded30_5 : ExcludedOn (model30.B 5 ++ [step30.q]) 9000000000000 (model30.caps 5)
     (model30.ord 5) 0 1 100 := by
diff --git a/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700001.lean b/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700001.lean
index d91ad32c97..0ffd00e137 100644
--- a/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700001.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700001.lean
@@ -269,6 +269,13 @@ def fan15Owner0Part5 : FanWitness := (.next ([796800000000, 4980000000000], [104
     ([-1533000000000], [4785000000000]) (some (0, 4, 10)) (some (0, 4, 10))
     fan15Owner0Part4))))))))))))))))))))))))
 
+-- Limit kernel memory by checking this fan tail separately.
+private theorem checkedFan8Owner0Part0 :
+    fan8Owner0Part0.check (model8.B 0 ++ [step8.q]) 9000000000000
+      (model8.caps 0) 0 1 100 12
+      ([261600000000, -2490000000000], [796800000000, 4980000000000]) = true := by
+  decide +kernel
+
 theorem excluded8_0 : ExcludedOn (model8.B 0 ++ [step8.q]) 9000000000000 (model8.caps 0) (model8.ord
     0) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([1838400000000, 2490000000000], [398400000000,
@@ -295,7 +302,12 @@ theorem excluded8_0 : ExcludedOn (model8.B 0 ++ [step8.q]) 9000000000000 (model8
       ([261600000000, -2490000000000], [796800000000, 4980000000000]) (some (0, 10, 10)) (some (0,
       10, 10)) fan8Owner0Part0)))))))))))))))))))))) (den :=
       9000000000000) (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan8Owner0Part0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded8_1 : ExcludedOn (model8.B 1 ++ [step8.q]) 9000000000000 (model8.caps 1) (model8.ord
     1) 0 1 100 := by
@@ -534,6 +546,13 @@ theorem next10 : model10.insert step10 = model11 := by
   apply Model.ext_fields
   all_goals intro j; fin_cases j <;> decide +kernel
 
+-- Limit kernel memory by checking this fan tail separately.
+private theorem checkedFan11Owner0Part0 :
+    fan11Owner0Part0.check (model11.B 0 ++ [step11.q]) 9000000000000
+      (model11.caps 0) 0 1 100 12
+      ([398400000000, 2490000000000], [1838400000000, 2490000000000]) = true := by
+  decide +kernel
+
 theorem excluded11_0 : ExcludedOn (model11.B 0 ++ [step11.q]) 9000000000000 (model11.caps 0)
     (model11.ord 0) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([1838400000000, 2490000000000], [398400000000,
@@ -562,7 +581,12 @@ theorem excluded11_0 : ExcludedOn (model11.B 0 ++ [step11.q]) 9000000000000 (mod
       ([398400000000, 2490000000000], [1838400000000, 2490000000000]) (some (10, 4, 10)) (some (10,
       4, 10)) fan11Owner0Part0)))))))))))))))))))))))) (den := 9000000000000) (fuel := 12)
       (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan11Owner0Part0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded11_1 : ExcludedOn (model11.B 1 ++ [step11.q]) 9000000000000 (model11.caps 1)
     (model11.ord 1) 0 1 100 := by
@@ -926,6 +950,106 @@ theorem next14 : model14.insert step14 = model15 := by
   apply Model.ext_fields
   all_goals intro j; fin_cases j <;> decide +kernel
 
+-- Verify the shared tails in one proof to bound the kernel working set.
+private theorem checkedFan15Owner0Part5Checks :
+    (fan15Owner0Part0.check (model15.B 0 ++ [step15.q]) 9000000000000
+      (model15.caps 0) 0 740624 318861100 12
+      ([-660000000000], [2100000000000]) = true) ∧
+    (fan15Owner0Part1.check (model15.B 0 ++ [step15.q]) 9000000000000
+      (model15.caps 0) 0 740624 318861100 12
+      ([2193600000000, -2490000000000], [2329800000000, 4980000000000]) = true) ∧
+    (fan15Owner0Part2.check (model15.B 0 ++ [step15.q]) 9000000000000
+      (model15.caps 0) 740624 2083888 318861100 12
+      ([-1533000000000], [4785000000000]) = true) ∧
+    (fan15Owner0Part3.check (model15.B 0 ++ [step15.q]) 9000000000000
+      (model15.caps 0) 740624 2083888 318861100 12
+      ([796800000000, 4980000000000], [1041600000000, -2490000000000]) = true) ∧
+    (fan15Owner0Part4.check (model15.B 0 ++ [step15.q]) 9000000000000
+      (model15.caps 0) 2224 3403 340300 12
+      ([-1533000000000], [4785000000000]) = true) ∧
+    (fan15Owner0Part5.check (model15.B 0 ++ [step15.q]) 9000000000000
+      (model15.caps 0) 2224 3403 340300 12
+      ([660000000000], [780000000000]) = true) := by
+  have checkedTail0 :
+      fan15Owner0Part0.check (model15.B 0 ++ [step15.q]) 9000000000000
+        (model15.caps 0) 0 740624 318861100 12
+        ([-660000000000], [2100000000000]) = true := by
+    decide +kernel
+  have checkedTail1 :
+      fan15Owner0Part1.check (model15.B 0 ++ [step15.q]) 9000000000000
+        (model15.caps 0) 0 740624 318861100 12
+        ([2193600000000, -2490000000000], [2329800000000, 4980000000000]) = true := by
+    delta fan15Owner0Part1
+    simp only [FanWitness.check, checkedTail0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail2 :
+      fan15Owner0Part2.check (model15.B 0 ++ [step15.q]) 9000000000000
+        (model15.caps 0) 740624 2083888 318861100 12
+        ([-1533000000000], [4785000000000]) = true := by
+    decide +kernel
+  have checkedTail3 :
+      fan15Owner0Part3.check (model15.B 0 ++ [step15.q]) 9000000000000
+        (model15.caps 0) 740624 2083888 318861100 12
+        ([796800000000, 4980000000000], [1041600000000, -2490000000000]) = true := by
+    delta fan15Owner0Part3
+    simp only [FanWitness.check, checkedTail2,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail4 :
+      fan15Owner0Part4.check (model15.B 0 ++ [step15.q]) 9000000000000
+        (model15.caps 0) 2224 3403 340300 12
+        ([-1533000000000], [4785000000000]) = true := by
+    decide +kernel
+  have checkedTail5 :
+      fan15Owner0Part5.check (model15.B 0 ++ [step15.q]) 9000000000000
+        (model15.caps 0) 2224 3403 340300 12
+        ([660000000000], [780000000000]) = true := by
+    delta fan15Owner0Part5
+    simp only [FanWitness.check, checkedTail4,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  exact ⟨checkedTail0, checkedTail1, checkedTail2, checkedTail3, checkedTail4, checkedTail5⟩
+
+private theorem checkedFan15Owner0Part0 :
+    fan15Owner0Part0.check (model15.B 0 ++ [step15.q]) 9000000000000
+      (model15.caps 0) 0 740624 318861100 12
+      ([-660000000000], [2100000000000]) = true := by
+  exact checkedFan15Owner0Part5Checks.1
+
+private theorem checkedFan15Owner0Part1 :
+    fan15Owner0Part1.check (model15.B 0 ++ [step15.q]) 9000000000000
+      (model15.caps 0) 0 740624 318861100 12
+      ([2193600000000, -2490000000000], [2329800000000, 4980000000000]) = true := by
+  exact checkedFan15Owner0Part5Checks.2.1
+
+private theorem checkedFan15Owner0Part2 :
+    fan15Owner0Part2.check (model15.B 0 ++ [step15.q]) 9000000000000
+      (model15.caps 0) 740624 2083888 318861100 12
+      ([-1533000000000], [4785000000000]) = true := by
+  exact checkedFan15Owner0Part5Checks.2.2.1
+
+private theorem checkedFan15Owner0Part3 :
+    fan15Owner0Part3.check (model15.B 0 ++ [step15.q]) 9000000000000
+      (model15.caps 0) 740624 2083888 318861100 12
+      ([796800000000, 4980000000000], [1041600000000, -2490000000000]) = true := by
+  exact checkedFan15Owner0Part5Checks.2.2.2.1
+
+private theorem checkedFan15Owner0Part4 :
+    fan15Owner0Part4.check (model15.B 0 ++ [step15.q]) 9000000000000
+      (model15.caps 0) 2224 3403 340300 12
+      ([-1533000000000], [4785000000000]) = true := by
+  exact checkedFan15Owner0Part5Checks.2.2.2.2.1
+
+private theorem checkedFan15Owner0Part5 :
+    fan15Owner0Part5.check (model15.B 0 ++ [step15.q]) 9000000000000
+      (model15.caps 0) 2224 3403 340300 12
+      ([660000000000], [780000000000]) = true := by
+  exact checkedFan15Owner0Part5Checks.2.2.2.2.2
+
 theorem excluded15_0 : ExcludedOn (model15.B 0 ++ [step15.q]) 9000000000000 (model15.caps 0)
     (model15.ord 0) 0 1 100 := by
   apply ExclusionHint.sound (.split (0) (2224) (3403) (340300) (.split (0) (740624) (2083888)
@@ -983,7 +1107,12 @@ theorem excluded15_0 : ExcludedOn (model15.B 0 ++ [step15.q]) 9000000000000 (mod
       [2193000000000]) (some (10, 3, 10)) (some (10, 3, 10)) (.next ([660000000000], [780000000000])
       (some (10, 3, 10)) (some (10, 3, 10)) fan15Owner0Part5))))))))))))))))))) (den :=
       9000000000000) (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan15Owner0Part1, checkedFan15Owner0Part3, checkedFan15Owner0Part5,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded15_1 : ExcludedOn (model15.B 1 ++ [step15.q]) 9000000000000 (model15.caps 1)
     (model15.ord 1) 0 1 100 := by
diff --git a/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700005.lean b/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700005.lean
index 72f39791dd..436d012e6e 100644
--- a/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700005.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700005.lean
@@ -758,6 +758,42 @@ theorem next41 : model41.insert step41 = model42 := by
   apply Model.ext_fields
   all_goals intro j; fin_cases j <;> decide +kernel
 
+-- Verify the shared tails in one proof to bound the kernel working set.
+private theorem checkedFan42Owner0Part1Checks :
+    (fan42Owner0Part0.check (model42.B 0 ++ [step42.q]) 9000000000000
+      (model42.caps 0) 0 1 100 12
+      ([-630000000000], [5895000000000]) = true) ∧
+    (fan42Owner0Part1.check (model42.B 0 ++ [step42.q]) 9000000000000
+      (model42.caps 0) 0 1 100 12
+      ([796800000000, 4980000000000], [261600000000, -2490000000000]) = true) := by
+  have checkedTail0 :
+      fan42Owner0Part0.check (model42.B 0 ++ [step42.q]) 9000000000000
+        (model42.caps 0) 0 1 100 12
+        ([-630000000000], [5895000000000]) = true := by
+    decide +kernel
+  have checkedTail1 :
+      fan42Owner0Part1.check (model42.B 0 ++ [step42.q]) 9000000000000
+        (model42.caps 0) 0 1 100 12
+        ([796800000000, 4980000000000], [261600000000, -2490000000000]) = true := by
+    delta fan42Owner0Part1
+    simp only [FanWitness.check, checkedTail0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  exact ⟨checkedTail0, checkedTail1⟩
+
+private theorem checkedFan42Owner0Part0 :
+    fan42Owner0Part0.check (model42.B 0 ++ [step42.q]) 9000000000000
+      (model42.caps 0) 0 1 100 12
+      ([-630000000000], [5895000000000]) = true := by
+  exact checkedFan42Owner0Part1Checks.1
+
+private theorem checkedFan42Owner0Part1 :
+    fan42Owner0Part1.check (model42.B 0 ++ [step42.q]) 9000000000000
+      (model42.caps 0) 0 1 100 12
+      ([796800000000, 4980000000000], [261600000000, -2490000000000]) = true := by
+  exact checkedFan42Owner0Part1Checks.2
+
 theorem excluded42_0 : ExcludedOn (model42.B 0 ++ [step42.q]) 9000000000000 (model42.caps 0)
     (model42.ord 0) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([8640000000000], [210000000000]) (some (8, 2, 5))
@@ -773,7 +809,12 @@ theorem excluded42_0 : ExcludedOn (model42.B 0 ++ [step42.q]) 9000000000000 (mod
       2, 5)) (.next ([796800000000, 4980000000000], [261600000000, -2490000000000]) (some (8, 2, 5))
       (some (8, 2, 5)) fan42Owner0Part1)))))))))))) (den := 9000000000000) (fuel
       := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan42Owner0Part1,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded42_1 : ExcludedOn (model42.B 1 ++ [step42.q]) 9000000000000 (model42.caps 1)
     (model42.ord 1) 0 1 100 := by
@@ -781,6 +822,13 @@ theorem excluded42_1 : ExcludedOn (model42.B 1 ++ [step42.q]) 9000000000000 (mod
       100 (by decide +kernel)
   decide +kernel
 
+-- Limit kernel memory by checking this fan tail separately.
+private theorem checkedFan42Owner2Part0 :
+    fan42Owner2Part0.check (model42.B 2 ++ [step42.q]) 9000000000000
+      (model42.caps 2) 0 1 100 12
+      ([435000000000], [7125000000000]) = true := by
+  decide +kernel
+
 theorem excluded42_2 : ExcludedOn (model42.B 2 ++ [step42.q]) 9000000000000 (model42.caps 2)
     (model42.ord 2) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([6480000000000, 0], [210000000000,
@@ -806,7 +854,12 @@ theorem excluded42_2 : ExcludedOn (model42.B 2 ++ [step42.q]) 9000000000000 (mod
       (some (7, 2, 5)) (.next ([435000000000], [7125000000000]) (some (7, 2, 5)) (some (7, 2, 5))
       fan42Owner2Part0)))))))))))))))))))))))) (den :=
       9000000000000) (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan42Owner2Part0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded42_4 : ExcludedOn (model42.B 4 ++ [step42.q]) 9000000000000 (model42.caps 4)
     (model42.ord 4) 0 1 100 := by
@@ -871,6 +924,42 @@ theorem excluded43_1 : ExcludedOn (model43.B 1 ++ [step43.q]) 9000000000000 (mod
       100 (by decide +kernel)
   decide +kernel
 
+-- Verify the shared tails in one proof to bound the kernel working set.
+private theorem checkedFan43Owner2Part1Checks :
+    (fan43Owner2Part0.check (model43.B 2 ++ [step43.q]) 9000000000000
+      (model43.caps 2) 0 1 100 12
+      ([0, -9000000000000], [3375000000000]) = true) ∧
+    (fan43Owner2Part1.check (model43.B 2 ++ [step43.q]) 9000000000000
+      (model43.caps 2) 0 1 100 12
+      ([7875000000000, 0], [480000000000, 9000000000000]) = true) := by
+  have checkedTail0 :
+      fan43Owner2Part0.check (model43.B 2 ++ [step43.q]) 9000000000000
+        (model43.caps 2) 0 1 100 12
+        ([0, -9000000000000], [3375000000000]) = true := by
+    decide +kernel
+  have checkedTail1 :
+      fan43Owner2Part1.check (model43.B 2 ++ [step43.q]) 9000000000000
+        (model43.caps 2) 0 1 100 12
+        ([7875000000000, 0], [480000000000, 9000000000000]) = true := by
+    delta fan43Owner2Part1
+    simp only [FanWitness.check, checkedTail0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  exact ⟨checkedTail0, checkedTail1⟩
+
+private theorem checkedFan43Owner2Part0 :
+    fan43Owner2Part0.check (model43.B 2 ++ [step43.q]) 9000000000000
+      (model43.caps 2) 0 1 100 12
+      ([0, -9000000000000], [3375000000000]) = true := by
+  exact checkedFan43Owner2Part1Checks.1
+
+private theorem checkedFan43Owner2Part1 :
+    fan43Owner2Part1.check (model43.B 2 ++ [step43.q]) 9000000000000
+      (model43.caps 2) 0 1 100 12
+      ([7875000000000, 0], [480000000000, 9000000000000]) = true := by
+  exact checkedFan43Owner2Part1Checks.2
+
 theorem excluded43_2 : ExcludedOn (model43.B 2 ++ [step43.q]) 9000000000000 (model43.caps 2)
     (model43.ord 2) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([3375000000000, -9000000000000], [0,
@@ -878,6 +967,18 @@ theorem excluded43_2 : ExcludedOn (model43.B 2 ++ [step43.q]) 9000000000000 (mod
       9000000000000]) (some (0, 7, 4)) (some (0, 7, 4)) (.next ([7875000000000, 0], [480000000000,
       9000000000000]) (some (0, 7, 4)) (some (0, 7, 4)) fan43Owner2Part1))))
       (den := 9000000000000) (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan43Owner2Part1,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
+
+-- Limit kernel memory by checking this fan tail separately.
+private theorem checkedFan43Owner3Part0 :
+    fan43Owner3Part0.check (model43.B 3 ++ [step43.q]) 9000000000000
+      (model43.caps 3) 0 1 100 12
+      ([5820000000000], [210000000000]) = true := by
   decide +kernel
 
 theorem excluded43_3 : ExcludedOn (model43.B 3 ++ [step43.q]) 9000000000000 (model43.caps 3)
@@ -886,7 +987,12 @@ theorem excluded43_3 : ExcludedOn (model43.B 3 ++ [step43.q]) 9000000000000 (mod
       (some (4, 0, 5)) fan43Owner3Part0)) (den := 9000000000000) (fuel := 12) (by decide +kernel) 0
       1 100
       (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan43Owner3Part0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded43_4 : ExcludedOn (model43.B 4 ++ [step43.q]) 9000000000000 (model43.caps 4)
     (model43.ord 4) 0 1 100 := by
@@ -951,6 +1057,139 @@ theorem excluded44_1 : ExcludedOn (model44.B 1 ++ [step44.q]) 9000000000000 (mod
       100 (by decide +kernel)
   decide +kernel
 
+-- Verify the shared tails in one proof to bound the kernel working set.
+private theorem checkedFan44Owner2Part7Checks :
+    (fan44Owner2Part0.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 0 4464 2064600 12
+      ([-1440000000000, -9000000000000], [9000000000000, 0]) = true) ∧
+    (fan44Owner2Part1.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 0 4464 2064600 12
+      ([6165000000000], [2145000000000]) = true) ∧
+    (fan44Owner2Part2.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 4464 7533 2064600 12
+      ([-45000000000, -9000000000000], [480000000000, 0]) = true) ∧
+    (fan44Owner2Part3.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 4464 7533 2064600 12
+      ([5040000000000], [1395000000000]) = true) ∧
+    (fan44Owner2Part4.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 7533 10619 2064600 12
+      ([-1005000000000, -9000000000000], [8565000000000, 9000000000000]) = true) ∧
+    (fan44Owner2Part5.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 7533 10619 2064600 12
+      ([6165000000000], [2145000000000]) = true) ∧
+    (fan44Owner2Part6.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 287 558 55800 12
+      ([-210000000000, -9000000000000], [6690000000000, 9000000000000]) = true) ∧
+    (fan44Owner2Part7.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 287 558 55800 12
+      ([7605000000000, 0], [960000000000, 9000000000000]) = true) := by
+  have checkedTail0 :
+      fan44Owner2Part0.check (model44.B 2 ++ [step44.q]) 9000000000000
+        (model44.caps 2) 0 4464 2064600 12
+        ([-1440000000000, -9000000000000], [9000000000000, 0]) = true := by
+    decide +kernel
+  have checkedTail1 :
+      fan44Owner2Part1.check (model44.B 2 ++ [step44.q]) 9000000000000
+        (model44.caps 2) 0 4464 2064600 12
+        ([6165000000000], [2145000000000]) = true := by
+    delta fan44Owner2Part1
+    simp only [FanWitness.check, checkedTail0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail2 :
+      fan44Owner2Part2.check (model44.B 2 ++ [step44.q]) 9000000000000
+        (model44.caps 2) 4464 7533 2064600 12
+        ([-45000000000, -9000000000000], [480000000000, 0]) = true := by
+    decide +kernel
+  have checkedTail3 :
+      fan44Owner2Part3.check (model44.B 2 ++ [step44.q]) 9000000000000
+        (model44.caps 2) 4464 7533 2064600 12
+        ([5040000000000], [1395000000000]) = true := by
+    delta fan44Owner2Part3
+    simp only [FanWitness.check, checkedTail2,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail4 :
+      fan44Owner2Part4.check (model44.B 2 ++ [step44.q]) 9000000000000
+        (model44.caps 2) 7533 10619 2064600 12
+        ([-1005000000000, -9000000000000], [8565000000000, 9000000000000]) = true := by
+    decide +kernel
+  have checkedTail5 :
+      fan44Owner2Part5.check (model44.B 2 ++ [step44.q]) 9000000000000
+        (model44.caps 2) 7533 10619 2064600 12
+        ([6165000000000], [2145000000000]) = true := by
+    delta fan44Owner2Part5
+    simp only [FanWitness.check, checkedTail4,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  have checkedTail6 :
+      fan44Owner2Part6.check (model44.B 2 ++ [step44.q]) 9000000000000
+        (model44.caps 2) 287 558 55800 12
+        ([-210000000000, -9000000000000], [6690000000000, 9000000000000]) = true := by
+    decide +kernel
+  have checkedTail7 :
+      fan44Owner2Part7.check (model44.B 2 ++ [step44.q]) 9000000000000
+        (model44.caps 2) 287 558 55800 12
+        ([7605000000000, 0], [960000000000, 9000000000000]) = true := by
+    delta fan44Owner2Part7
+    simp only [FanWitness.check, checkedTail6,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  exact ⟨checkedTail0, checkedTail1, checkedTail2, checkedTail3, checkedTail4, checkedTail5,
+    checkedTail6, checkedTail7⟩
+
+private theorem checkedFan44Owner2Part0 :
+    fan44Owner2Part0.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 0 4464 2064600 12
+      ([-1440000000000, -9000000000000], [9000000000000, 0]) = true := by
+  exact checkedFan44Owner2Part7Checks.1
+
+private theorem checkedFan44Owner2Part1 :
+    fan44Owner2Part1.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 0 4464 2064600 12
+      ([6165000000000], [2145000000000]) = true := by
+  exact checkedFan44Owner2Part7Checks.2.1
+
+private theorem checkedFan44Owner2Part2 :
+    fan44Owner2Part2.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 4464 7533 2064600 12
+      ([-45000000000, -9000000000000], [480000000000, 0]) = true := by
+  exact checkedFan44Owner2Part7Checks.2.2.1
+
+private theorem checkedFan44Owner2Part3 :
+    fan44Owner2Part3.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 4464 7533 2064600 12
+      ([5040000000000], [1395000000000]) = true := by
+  exact checkedFan44Owner2Part7Checks.2.2.2.1
+
+private theorem checkedFan44Owner2Part4 :
+    fan44Owner2Part4.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 7533 10619 2064600 12
+      ([-1005000000000, -9000000000000], [8565000000000, 9000000000000]) = true := by
+  exact checkedFan44Owner2Part7Checks.2.2.2.2.1
+
+private theorem checkedFan44Owner2Part5 :
+    fan44Owner2Part5.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 7533 10619 2064600 12
+      ([6165000000000], [2145000000000]) = true := by
+  exact checkedFan44Owner2Part7Checks.2.2.2.2.2.1
+
+private theorem checkedFan44Owner2Part6 :
+    fan44Owner2Part6.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 287 558 55800 12
+      ([-210000000000, -9000000000000], [6690000000000, 9000000000000]) = true := by
+  exact checkedFan44Owner2Part7Checks.2.2.2.2.2.2.1
+
+private theorem checkedFan44Owner2Part7 :
+    fan44Owner2Part7.check (model44.B 2 ++ [step44.q]) 9000000000000
+      (model44.caps 2) 287 558 55800 12
+      ([7605000000000, 0], [960000000000, 9000000000000]) = true := by
+  exact checkedFan44Owner2Part7Checks.2.2.2.2.2.2.2
+
 theorem excluded44_2 : ExcludedOn (model44.B 2 ++ [step44.q]) 9000000000000 (model44.caps 2)
     (model44.ord 2) 0 1 100 := by
   apply ExclusionHint.sound (.split (0) (287) (558) (55800) (.split (0) (4464) (10619) (2064600)
@@ -993,6 +1232,19 @@ theorem excluded44_2 : ExcludedOn (model44.B 2 ++ [step44.q]) 9000000000000 (mod
       9000000000000]) (some (0, 7, 4)) (some (0, 7, 4)) (.next ([7605000000000, 0], [960000000000,
       9000000000000]) (some (0, 7, 4)) (some (0, 7, 4)) fan44Owner2Part7)))))
       (den := 9000000000000) (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan44Owner2Part1, checkedFan44Owner2Part3, checkedFan44Owner2Part5,
+      checkedFan44Owner2Part7,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
+
+-- Limit kernel memory by checking this fan tail separately.
+private theorem checkedFan44Owner3Part0 :
+    fan44Owner3Part0.check (model44.B 3 ++ [step44.q]) 9000000000000
+      (model44.caps 3) 0 1 100 12
+      ([7815000000000], [0, 9000000000000]) = true := by
   decide +kernel
 
 theorem excluded44_3 : ExcludedOn (model44.B 3 ++ [step44.q]) 9000000000000 (model44.caps 3)
@@ -1000,7 +1252,12 @@ theorem excluded44_3 : ExcludedOn (model44.B 3 ++ [step44.q]) 9000000000000 (mod
   apply ExclusionHint.sound (.witnessedFan (.next ([7815000000000], [0, 9000000000000]) (some (3, 0,
       5)) (some (4, 0, 5)) fan44Owner3Part0)) (den := 9000000000000) (fuel
       := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan44Owner3Part0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded44_4 : ExcludedOn (model44.B 4 ++ [step44.q]) 9000000000000 (model44.caps 4)
     (model44.ord 4) 0 1 100 := by
@@ -1059,6 +1316,42 @@ theorem next44 : model44.insert step44 = model45 := by
   apply Model.ext_fields
   all_goals intro j; fin_cases j <;> decide +kernel
 
+-- Verify the shared tails in one proof to bound the kernel working set.
+private theorem checkedFan45Owner0Part1Checks :
+    (fan45Owner0Part0.check (model45.B 0 ++ [step45.q]) 9000000000000
+      (model45.caps 0) 0 1 100 12
+      ([-1185000000000], [8895000000000]) = true) ∧
+    (fan45Owner0Part1.check (model45.B 0 ++ [step45.q]) 9000000000000
+      (model45.caps 0) 0 1 100 12
+      ([6390000000000], [1695000000000]) = true) := by
+  have checkedTail0 :
+      fan45Owner0Part0.check (model45.B 0 ++ [step45.q]) 9000000000000
+        (model45.caps 0) 0 1 100 12
+        ([-1185000000000], [8895000000000]) = true := by
+    decide +kernel
+  have checkedTail1 :
+      fan45Owner0Part1.check (model45.B 0 ++ [step45.q]) 9000000000000
+        (model45.caps 0) 0 1 100 12
+        ([6390000000000], [1695000000000]) = true := by
+    delta fan45Owner0Part1
+    simp only [FanWitness.check, checkedTail0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  exact ⟨checkedTail0, checkedTail1⟩
+
+private theorem checkedFan45Owner0Part0 :
+    fan45Owner0Part0.check (model45.B 0 ++ [step45.q]) 9000000000000
+      (model45.caps 0) 0 1 100 12
+      ([-1185000000000], [8895000000000]) = true := by
+  exact checkedFan45Owner0Part1Checks.1
+
+private theorem checkedFan45Owner0Part1 :
+    fan45Owner0Part1.check (model45.B 0 ++ [step45.q]) 9000000000000
+      (model45.caps 0) 0 1 100 12
+      ([6390000000000], [1695000000000]) = true := by
+  exact checkedFan45Owner0Part1Checks.2
+
 theorem excluded45_0 : ExcludedOn (model45.B 0 ++ [step45.q]) 9000000000000 (model45.caps 0)
     (model45.ord 0) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([7050000000000], [360000000000]) (some (8, 9, 6))
@@ -1077,7 +1370,12 @@ theorem excluded45_0 : ExcludedOn (model45.B 0 ++ [step45.q]) 9000000000000 (mod
       [1440000000000]) (some (8, 9, 6)) (some (8, 9, 6)) (.next ([6390000000000], [1695000000000])
       (some (8, 9, 6)) (some (8, 9, 6)) fan45Owner0Part1)))))))))))))))) (den := 9000000000000)
       (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan45Owner0Part1,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded45_1 : ExcludedOn (model45.B 1 ++ [step45.q]) 9000000000000 (model45.caps 1)
     (model45.ord 1) 0 1 100 := by
@@ -1097,6 +1395,13 @@ theorem excluded45_3 : ExcludedOn (model45.B 3 ++ [step45.q]) 9000000000000 (mod
       100 (by decide +kernel)
   decide +kernel
 
+-- Limit kernel memory by checking this fan tail separately.
+private theorem checkedFan45Owner4Part0 :
+    fan45Owner4Part0.check (model45.B 4 ++ [step45.q]) 9000000000000
+      (model45.caps 4) 0 1 100 12
+      ([6375000000000], [915000000000]) = true := by
+  decide +kernel
+
 theorem excluded45_4 : ExcludedOn (model45.B 4 ++ [step45.q]) 9000000000000 (model45.caps 4)
     (model45.ord 4) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([7470000000000], [195000000000]) (some (3, 0, 5))
@@ -1104,7 +1409,12 @@ theorem excluded45_4 : ExcludedOn (model45.B 4 ++ [step45.q]) 9000000000000 (mod
       (.next ([6375000000000], [915000000000]) (some (3, 1, 5)) (some (3, 1, 5))
       fan45Owner4Part0)))) (den := 9000000000000)
       (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan45Owner4Part0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded45_6 : ExcludedOn (model45.B 6 ++ [step45.q]) 9000000000000 (model45.caps 6)
     (model45.ord 6) 0 1 100 := by
@@ -1167,6 +1477,42 @@ theorem next45 : model45.insert step45 = model46 := by
   apply Model.ext_fields
   all_goals intro j; fin_cases j <;> decide +kernel
 
+-- Verify the shared tails in one proof to bound the kernel working set.
+private theorem checkedFan46Owner0Part1Checks :
+    (fan46Owner0Part0.check (model46.B 0 ++ [step46.q]) 9000000000000
+      (model46.caps 0) 0 1 100 12
+      ([-780000000000], [5625000000000]) = true) ∧
+    (fan46Owner0Part1.check (model46.B 0 ++ [step46.q]) 9000000000000
+      (model46.caps 0) 0 1 100 12
+      ([4583400000000, 2490000000000], [1838400000000, 2490000000000]) = true) := by
+  have checkedTail0 :
+      fan46Owner0Part0.check (model46.B 0 ++ [step46.q]) 9000000000000
+        (model46.caps 0) 0 1 100 12
+        ([-780000000000], [5625000000000]) = true := by
+    decide +kernel
+  have checkedTail1 :
+      fan46Owner0Part1.check (model46.B 0 ++ [step46.q]) 9000000000000
+        (model46.caps 0) 0 1 100 12
+        ([4583400000000, 2490000000000], [1838400000000, 2490000000000]) = true := by
+    delta fan46Owner0Part1
+    simp only [FanWitness.check, checkedTail0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide +kernel
+  exact ⟨checkedTail0, checkedTail1⟩
+
+private theorem checkedFan46Owner0Part0 :
+    fan46Owner0Part0.check (model46.B 0 ++ [step46.q]) 9000000000000
+      (model46.caps 0) 0 1 100 12
+      ([-780000000000], [5625000000000]) = true := by
+  exact checkedFan46Owner0Part1Checks.1
+
+private theorem checkedFan46Owner0Part1 :
+    fan46Owner0Part1.check (model46.B 0 ++ [step46.q]) 9000000000000
+      (model46.caps 0) 0 1 100 12
+      ([4583400000000, 2490000000000], [1838400000000, 2490000000000]) = true := by
+  exact checkedFan46Owner0Part1Checks.2
+
 theorem excluded46_0 : ExcludedOn (model46.B 0 ++ [step46.q]) 9000000000000 (model46.caps 0)
     (model46.ord 0) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([7050000000000], [360000000000]) (some (8, 3, 6))
@@ -1188,7 +1534,12 @@ theorem excluded46_0 : ExcludedOn (model46.B 0 ++ [step46.q]) 9000000000000 (mod
       [1838400000000, 2490000000000]) (some (8, 3, 6)) (some (8, 3, 6))
       fan46Owner0Part1)))))))))))))))))) (den := 9000000000000)
       (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan46Owner0Part1,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded46_1 : ExcludedOn (model46.B 1 ++ [step46.q]) 9000000000000 (model46.caps 1)
     (model46.ord 1) 0 1 100 := by
@@ -1214,12 +1565,24 @@ theorem excluded46_4 : ExcludedOn (model46.B 4 ++ [step46.q]) 9000000000000 (mod
       100 (by decide +kernel)
   decide +kernel
 
+-- Limit kernel memory by checking this fan tail separately.
+private theorem checkedFan46Owner5Part0 :
+    fan46Owner5Part0.check (model46.B 5 ++ [step46.q]) 9000000000000
+      (model46.caps 5) 0 1 100 12
+      ([7560000000000, -9000000000000], [165000000000, 9000000000000]) = true := by
+  decide +kernel
+
 theorem excluded46_5 : ExcludedOn (model46.B 5 ++ [step46.q]) 9000000000000 (model46.caps 5)
     (model46.ord 5) 0 1 100 := by
   apply ExclusionHint.sound (.witnessedFan (.next ([7560000000000, -9000000000000], [165000000000,
       9000000000000]) (some (5, 0, 3)) (some (5, 1, 3)) fan46Owner5Part0)) (den
       := 9000000000000) (fuel := 12) (by decide +kernel) 0 1 100 (by decide +kernel)
-  decide +kernel
+  as_aux_lemma =>
+    simp only [ExclusionHint.check, FanWitness.check,
+      checkedFan46Owner5Part0,
+      Bool.and_eq_true, and_true]
+    repeat' apply And.intro
+    all_goals decide
 
 theorem excluded46_7 : ExcludedOn (model46.B 7 ++ [step46.q]) 9000000000000 (model46.caps 7)
     (model46.ord 7) 0 1 100 := by
diff --git a/LeanPool/ConwaySoifer/Simplified/Complements/AcrossLarge.lean b/LeanPool/ConwaySoifer/Simplified/Complements/AcrossLarge.lean
index cd92f94cfa..86ecc1b2f8 100644
--- a/LeanPool/ConwaySoifer/Simplified/Complements/AcrossLarge.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Complements/AcrossLarge.lean
@@ -8,7 +8,11 @@ module
 public import LeanPool.ConwaySoifer.Simplified.Geometry.AcrossLargeSide
 public import LeanPool.ConwaySoifer.Simplified.Geometry.AcrossLargeCentre
 public import LeanPool.ConwaySoifer.Geometry.SideFacts
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
 
 /-!
 # AcrossLarge
diff --git a/LeanPool/ConwaySoifer/Simplified/Complements/AcrossSmall.lean b/LeanPool/ConwaySoifer/Simplified/Complements/AcrossSmall.lean
index 95ecfffae9..2d26729343 100644
--- a/LeanPool/ConwaySoifer/Simplified/Complements/AcrossSmall.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Complements/AcrossSmall.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.AcrossArea
 public import LeanPool.ConwaySoifer.Simplified.Geometry.AcrossFour
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
 
 /-!
 # AcrossSmall
diff --git a/LeanPool/ConwaySoifer/Simplified/Complements/AownLarge.lean b/LeanPool/ConwaySoifer/Simplified/Complements/AownLarge.lean
index 270c04c05b..c5b7f7e175 100644
--- a/LeanPool/ConwaySoifer/Simplified/Complements/AownLarge.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Complements/AownLarge.lean
@@ -8,7 +8,9 @@ module
 public import LeanPool.ConwaySoifer.Simplified.Geometry.AownCut
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Midpoint
 public import LeanPool.ConwaySoifer.Geometry.AownFacts
-import Mathlib.Tactic
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
 
 /-!
 # AownLarge
diff --git a/LeanPool/ConwaySoifer/Simplified/Complements/AownSmall.lean b/LeanPool/ConwaySoifer/Simplified/Complements/AownSmall.lean
index 02208b7776..4e61052145 100644
--- a/LeanPool/ConwaySoifer/Simplified/Complements/AownSmall.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Complements/AownSmall.lean
@@ -7,7 +7,10 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.AownChains
 public import LeanPool.ConwaySoifer.Simplified.Geometry.AownCentral
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
 
 /-!
 # AownSmall
diff --git a/LeanPool/ConwaySoifer/Simplified/Complements/SextSmall.lean b/LeanPool/ConwaySoifer/Simplified/Complements/SextSmall.lean
index 5174674755..839932c6fb 100644
--- a/LeanPool/ConwaySoifer/Simplified/Complements/SextSmall.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Complements/SextSmall.lean
@@ -8,7 +8,11 @@ module
 public import LeanPool.ConwaySoifer.Simplified.Geometry.LocalSideCover
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SideChains
 public import LeanPool.ConwaySoifer.Simplified.Certificates.Coverage
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Ring
 
 /-!
 # SextSmall
diff --git a/LeanPool/ConwaySoifer/Simplified/Complements/SintSmall.lean b/LeanPool/ConwaySoifer/Simplified/Complements/SintSmall.lean
index 890dd67606..b97a741c08 100644
--- a/LeanPool/ConwaySoifer/Simplified/Complements/SintSmall.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Complements/SintSmall.lean
@@ -8,7 +8,11 @@ module
 public import LeanPool.ConwaySoifer.Simplified.Geometry.LocalSideCover
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SintCorner
 public import LeanPool.ConwaySoifer.Simplified.Certificates.Coverage
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Ring
 
 /-!
 # SintSmall
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossArea.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossArea.lean
index 87bece6250..f21a23505d 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossArea.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossArea.lean
@@ -6,7 +6,10 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Charging
-import Mathlib.Tactic
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # AcrossArea
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossFour.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossFour.lean
index ad0796f2ee..ed853f63a9 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossFour.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossFour.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossLargeCentre.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossLargeCentre.lean
index 1b590c2058..c3ce95b235 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossLargeCentre.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossLargeCentre.lean
@@ -7,7 +7,9 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossLargeSide.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossLargeSide.lean
index 6a66191ea7..f2ecb18c96 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossLargeSide.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/AcrossLargeSide.lean
@@ -7,7 +7,9 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Affine.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Affine.lean
index 050df04436..12ce8a05e1 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Affine.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Affine.lean
@@ -6,7 +6,7 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Geometry.Symmetry
-import Mathlib.Tactic
+import Mathlib.Tactic.Ring
 
 /-!
 # Affine
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/AownArea.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/AownArea.lean
index fb9ddc9f7a..c1d79d64d1 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/AownArea.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/AownArea.lean
@@ -6,7 +6,13 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Charging
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.FunProp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.NormNum.RealSqrt
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # AownArea
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/AownCentral.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/AownCentral.lean
index eb38319a8e..f261c35704 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/AownCentral.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/AownCentral.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/AownChains.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/AownChains.lean
index 27175e25e0..195ff452ea 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/AownChains.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/AownChains.lean
@@ -10,7 +10,11 @@ public import LeanPool.ConwaySoifer.Simplified.Geometry.AownArea
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SideChains
 public import LeanPool.ConwaySoifer.Simplified.Geometry.MiddleThird
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Core
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Ring
 
 /-!
 # AownChains
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/AownCut.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/AownCut.lean
index 20618cd7bc..0f4bfcac39 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/AownCut.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/AownCut.lean
@@ -6,7 +6,10 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.FullOwn
-import Mathlib.Tactic
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # AownCut
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Bridge.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Bridge.lean
index 0ba89b06e0..5a8b1dbe3c 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Bridge.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Bridge.lean
@@ -7,7 +7,9 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.BridgeLocal
 public import LeanPool.ConwaySoifer.Simplified.Geometry.HexSymmetry
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Ring
 
 /-!
 # Bridge
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/BridgeLocal.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/BridgeLocal.lean
index 0da91372b1..aed9b3d92d 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/BridgeLocal.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/BridgeLocal.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/CentralWitnesses.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/CentralWitnesses.lean
index 33b68e155d..b6146c8a30 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/CentralWitnesses.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/CentralWitnesses.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.ThreeCentral
 public import LeanPool.ConwaySoifer.Simplified.Geometry.ThreeWitnesses
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # CentralWitnesses
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Charging.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Charging.lean
index df412e824d..c7c6575dbe 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Charging.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Charging.lean
@@ -6,7 +6,12 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.CornerAbsent
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # Charging
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Core.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Core.lean
index 7687b47fc1..bd91ddbbf6 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Core.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Core.lean
@@ -7,7 +7,10 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.CoreLocal
 public import LeanPool.ConwaySoifer.Simplified.Geometry.HexSymmetry
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
 
 /-!
 # Core
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/CoreLocal.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/CoreLocal.lean
index ce826d8856..1b4656fdb9 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/CoreLocal.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/CoreLocal.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/CornerAbsent.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/CornerAbsent.lean
index 0bc8ca3a0a..a40c45bdfb 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/CornerAbsent.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/CornerAbsent.lean
@@ -8,7 +8,8 @@ module
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Midpoint
 public import LeanPool.ConwaySoifer.Simplified.Geometry.HexSymmetry
 public import LeanPool.ConwaySoifer.Geometry.SideFacts
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.NormNum.Basic
 
 /-!
 # CornerAbsent
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/ForbiddenCorner.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/ForbiddenCorner.lean
index b7081b16c8..b94953c04e 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/ForbiddenCorner.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/ForbiddenCorner.lean
@@ -6,7 +6,8 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Geometry.Support
-import Mathlib.Tactic
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
 
 /-! The forbidden corner section, proved directly on two closed orientation sectors.
 No Boolean geometry checks or external polynomial results are used. -/
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/FullOwn.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/FullOwn.lean
index 024ae38e50..ddd25f65f3 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/FullOwn.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/FullOwn.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Affine
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # FullOwn
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/HexSymmetry.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/HexSymmetry.lean
index 08a49dfcfa..a7084ce477 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/HexSymmetry.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/HexSymmetry.lean
@@ -7,7 +7,10 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Affine
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Ring
 
 /-!
 # HexSymmetry
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/LocalSideCover.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/LocalSideCover.lean
index c0ef6fffe5..45b192a6b9 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/LocalSideCover.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/LocalSideCover.lean
@@ -6,7 +6,7 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.CentralWitnesses
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
 
 /-!
 # LocalSideCover
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/MiddleThird.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/MiddleThird.lean
index cc6e857bd2..21f008a111 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/MiddleThird.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/MiddleThird.lean
@@ -7,7 +7,9 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Midpoint.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Midpoint.lean
index 3e27b7dd2f..25f1c26bb6 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Midpoint.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Midpoint.lean
@@ -7,7 +7,10 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.ForbiddenCorner
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Affine
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Ring
 
 /-!
 # Midpoint
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile0Q0.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile0Q0.lean
index e1c825c9ca..80612adc0d 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile0Q0.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile0Q0.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile0Q1.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile0Q1.lean
index 2f52b2f4ef..aaf78c1908 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile0Q1.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile0Q1.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile0Q2.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile0Q2.lean
index 6249846fd7..5a33eaf15b 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile0Q2.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile0Q2.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile1Q0.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile1Q0.lean
index aee7b145b4..6d9bb9167d 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile1Q0.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile1Q0.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile1Q1.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile1Q1.lean
index 0bec8010ee..58695aba27 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile1Q1.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile1Q1.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile1Q2.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile1Q2.lean
index 1e70064607..c47bff04fb 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile1Q2.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile1Q2.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile2Q0.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile2Q0.lean
index ad60d4d0bf..2d7f376a2f 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile2Q0.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile2Q0.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile2Q1.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile2Q1.lean
index 3f495c83ab..76a300e9da 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile2Q1.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile2Q1.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile2Q2.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile2Q2.lean
index 26954388b2..034ef054ba 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile2Q2.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile2Q2.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile3Q0.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile3Q0.lean
index 620d38fe29..dc7e77e495 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile3Q0.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile3Q0.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile3Q1.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile3Q1.lean
index 16028516c5..40e897ebae 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile3Q1.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile3Q1.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile3Q2.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile3Q2.lean
index 81f9cd3755..fb8cc80976 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile3Q2.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile3Q2.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile4Q0.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile4Q0.lean
index c92f577ce6..da4d26deed 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile4Q0.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile4Q0.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile4Q1.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile4Q1.lean
index e5ec558c1c..734c06ed6c 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile4Q1.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile4Q1.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile4Q2.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile4Q2.lean
index 38854d4486..570336591b 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile4Q2.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile4Q2.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile5Q0.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile5Q0.lean
index 828405b0d6..bff6c18b58 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile5Q0.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile5Q0.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile5Q1.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile5Q1.lean
index 12825a9dbb..f6883f32aa 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile5Q1.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile5Q1.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile5Q2.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile5Q2.lean
index f9c7e092d2..becefdddfb 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile5Q2.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile5Q2.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile6Q0.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile6Q0.lean
index b2f5fd0e15..c1a4a07e76 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile6Q0.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile6Q0.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile6Q1.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile6Q1.lean
index 23c633df89..f075211273 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile6Q1.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile6Q1.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile6Q2.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile6Q2.lean
index 476b5424f7..29e67f5370 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile6Q2.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile6Q2.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile7Q0.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile7Q0.lean
index 11776df07d..cddae3d875 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile7Q0.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile7Q0.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile7Q1.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile7Q1.lean
index dd184ac05a..03ba6d4b21 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile7Q1.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile7Q1.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile7Q2.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile7Q2.lean
index 32edb00534..0048650a5d 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Profile7Q2.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Profile7Q2.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/ProfileWitness.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/ProfileWitness.lean
index aeada4347c..fe594c4f0e 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/ProfileWitness.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/ProfileWitness.lean
@@ -30,7 +30,10 @@ public import LeanPool.ConwaySoifer.Simplified.Geometry.Profile7Q0
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Profile7Q1
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Profile7Q2
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Receiver
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Ring
 
 /-!
 # ProfileWitness
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/Receiver.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/Receiver.lean
index e0a84756e4..22705352dd 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/Receiver.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/Receiver.lean
@@ -8,7 +8,11 @@ module
 public import LeanPool.ConwaySoifer.Simplified.Geometry.ForbiddenCorner
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Affine
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Ring
 
 /-!
 # Receiver
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/SideChains.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/SideChains.lean
index 4dfea26c00..ddae39a49a 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/SideChains.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/SideChains.lean
@@ -7,7 +7,9 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Charging
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Bridge
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Ring
 
 /-!
 # SideChains
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/SintCorner.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/SintCorner.lean
index d3e821ff5d..e127ecfc6e 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/SintCorner.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/SintCorner.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SideChains
 public import LeanPool.ConwaySoifer.Simplified.Geometry.ProfileWitness
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-!
 # SintCorner
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/SupportFan.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/SupportFan.lean
index 1c5d76d40c..c4df74a3d0 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/SupportFan.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/SupportFan.lean
@@ -6,7 +6,8 @@ Authors: Vladislav Kuznetsov
 module
 
 public import LeanPool.ConwaySoifer.Geometry.Support
-import Mathlib.Tactic
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
 
 /-! Geometric orientation fans. Every cone uses the same support triple at
 both endpoints. All inputs are propositions about real points, not Boolean
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/ThreeCentral.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/ThreeCentral.lean
index cbb3086667..ab5395d1cb 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/ThreeCentral.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/ThreeCentral.lean
@@ -7,7 +7,11 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.SupportFan
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.Convert
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
 
 /-! Explicit real support fans for the handwritten geometric point set.
 The polynomial decompositions are proved by `ring`; their signs by `positivity`.
diff --git a/LeanPool/ConwaySoifer/Simplified/Geometry/ThreeWitnesses.lean b/LeanPool/ConwaySoifer/Simplified/Geometry/ThreeWitnesses.lean
index d1cbc5b305..cbd948d3ac 100644
--- a/LeanPool/ConwaySoifer/Simplified/Geometry/ThreeWitnesses.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Geometry/ThreeWitnesses.lean
@@ -7,7 +7,9 @@ module
 
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Receiver
 public import Mathlib.Data.Fin.VecNotation
-import Mathlib.Tactic
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum.Basic
 
 /-!
 # ThreeWitnesses
diff --git a/LeanPool/ConwaySoifer/Simplified/Normalization.lean b/LeanPool/ConwaySoifer/Simplified/Normalization.lean
index 44ac9dbbb9..19747927fa 100644
--- a/LeanPool/ConwaySoifer/Simplified/Normalization.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Normalization.lean
@@ -9,7 +9,6 @@ public import LeanPool.ConwaySoifer.Geometry.Normalization
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Core
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Bridge
 public import LeanPool.ConwaySoifer.Simplified.Geometry.Midpoint
-import Mathlib.Tactic
 
 /-!
 # Normalization
diff --git a/LeanPool/ConwaySoifer/Simplified/Theorem.lean b/LeanPool/ConwaySoifer/Simplified/Theorem.lean
index 9f90488dfe..aa1c43386e 100644
--- a/LeanPool/ConwaySoifer/Simplified/Theorem.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Theorem.lean
@@ -13,7 +13,7 @@ public import LeanPool.ConwaySoifer.Simplified.Complements.AownLarge
 public import LeanPool.ConwaySoifer.Simplified.Complements.AcrossSmall
 public import LeanPool.ConwaySoifer.Simplified.Complements.AcrossLarge
 public import LeanPool.ConwaySoifer.Geometry.Scaling
-import Mathlib.Tactic
+import Mathlib.Tactic.Linarith
 
 /-! The independent, unconditional assembly of the third-pass simplified proof. -/
 

From 0e26afd86c06e76007959fc163ed52749d0bf7b5 Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Wed, 21 Oct 2026 20:12:59 +0000
Subject: [PATCH 2/2] Remove unused private ConwaySoifer projection lemmas

---
 .../Certificates/Steps/Aown1500001600003.lean | 96 -------------------
 .../Certificates/Steps/Aown1600001700001.lean | 18 ----
 .../Certificates/Steps/Aown1600001700005.lean | 48 ----------
 3 files changed, 162 deletions(-)

diff --git a/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1500001600003.lean b/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1500001600003.lean
index a1f76f0e40..26952d9689 100644
--- a/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1500001600003.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1500001600003.lean
@@ -736,24 +736,6 @@ private theorem checkedFan24Owner0Part3Checks :
     all_goals decide +kernel
   exact ⟨checkedTail0, checkedTail1, checkedTail2, checkedTail3⟩
 
-private theorem checkedFan24Owner0Part0 :
-    fan24Owner0Part0.check (model24.B 0 ++ [step24.q]) 9000000000000
-      (model24.caps 0) 0 1 100 12
-      ([-1005000000000], [2880000000000]) = true := by
-  exact checkedFan24Owner0Part3Checks.1
-
-private theorem checkedFan24Owner0Part1 :
-    fan24Owner0Part1.check (model24.B 0 ++ [step24.q]) 9000000000000
-      (model24.caps 0) 0 1 100 12
-      ([0, 0], [1134000000000, 7560000000000]) = true := by
-  exact checkedFan24Owner0Part3Checks.2.1
-
-private theorem checkedFan24Owner0Part2 :
-    fan24Owner0Part2.check (model24.B 0 ++ [step24.q]) 9000000000000
-      (model24.caps 0) 0 1 100 12
-      ([3075000000000], [2100000000000]) = true := by
-  exact checkedFan24Owner0Part3Checks.2.2.1
-
 private theorem checkedFan24Owner0Part3 :
     fan24Owner0Part3.check (model24.B 0 ++ [step24.q]) 9000000000000
       (model24.caps 0) 0 1 100 12
@@ -985,24 +967,6 @@ private theorem checkedFan26Owner0Part3Checks :
     all_goals decide +kernel
   exact ⟨checkedTail0, checkedTail1, checkedTail2, checkedTail3⟩
 
-private theorem checkedFan26Owner0Part0 :
-    fan26Owner0Part0.check (model26.B 0 ++ [step26.q]) 9000000000000
-      (model26.caps 0) 0 1 100 12
-      ([-3000000000000], [9450000000000]) = true := by
-  exact checkedFan26Owner0Part3Checks.1
-
-private theorem checkedFan26Owner0Part1 :
-    fan26Owner0Part1.check (model26.B 0 ++ [step26.q]) 9000000000000
-      (model26.caps 0) 0 1 100 12
-      ([-45000000000], [4320000000000]) = true := by
-  exact checkedFan26Owner0Part3Checks.2.1
-
-private theorem checkedFan26Owner0Part2 :
-    fan26Owner0Part2.check (model26.B 0 ++ [step26.q]) 9000000000000
-      (model26.caps 0) 0 1 100 12
-      ([1875000000000], [1005000000000]) = true := by
-  exact checkedFan26Owner0Part3Checks.2.2.1
-
 private theorem checkedFan26Owner0Part3 :
     fan26Owner0Part3.check (model26.B 0 ++ [step26.q]) 9000000000000
       (model26.caps 0) 0 1 100 12
@@ -1148,18 +1112,6 @@ private theorem checkedFan27Owner0Part2Checks :
     all_goals decide +kernel
   exact ⟨checkedTail0, checkedTail1, checkedTail2⟩
 
-private theorem checkedFan27Owner0Part0 :
-    fan27Owner0Part0.check (model27.B 0 ++ [step27.q]) 9000000000000
-      (model27.caps 0) 0 1 100 12
-      ([-2025000000000], [8700000000000]) = true := by
-  exact checkedFan27Owner0Part2Checks.1
-
-private theorem checkedFan27Owner0Part1 :
-    fan27Owner0Part1.check (model27.B 0 ++ [step27.q]) 9000000000000
-      (model27.caps 0) 0 1 100 12
-      ([705000000000], [5295000000000]) = true := by
-  exact checkedFan27Owner0Part2Checks.2.1
-
 private theorem checkedFan27Owner0Part2 :
     fan27Owner0Part2.check (model27.B 0 ++ [step27.q]) 9000000000000
       (model27.caps 0) 0 1 100 12
@@ -1324,18 +1276,6 @@ private theorem checkedFan28Owner0Part2Checks :
     all_goals decide +kernel
   exact ⟨checkedTail0, checkedTail1, checkedTail2⟩
 
-private theorem checkedFan28Owner0Part0 :
-    fan28Owner0Part0.check (model28.B 0 ++ [step28.q]) 9000000000000
-      (model28.caps 0) 0 1 100 12
-      ([-1800000000000], [7500000000000]) = true := by
-  exact checkedFan28Owner0Part2Checks.1
-
-private theorem checkedFan28Owner0Part1 :
-    fan28Owner0Part1.check (model28.B 0 ++ [step28.q]) 9000000000000
-      (model28.caps 0) 0 1 100 12
-      ([150000000000], [7050000000000]) = true := by
-  exact checkedFan28Owner0Part2Checks.2.1
-
 private theorem checkedFan28Owner0Part2 :
     fan28Owner0Part2.check (model28.B 0 ++ [step28.q]) 9000000000000
       (model28.caps 0) 0 1 100 12
@@ -1563,48 +1503,12 @@ private theorem checkedFan29Owner0Part7Checks :
   exact ⟨checkedTail0, checkedTail1, checkedTail2, checkedTail3, checkedTail4, checkedTail5,
     checkedTail6, checkedTail7⟩
 
-private theorem checkedFan29Owner0Part0 :
-    fan29Owner0Part0.check (model29.B 0 ++ [step29.q]) 9000000000000
-      (model29.caps 0) 0 485 95100 12
-      ([-3900000000000], [9750000000000]) = true := by
-  exact checkedFan29Owner0Part7Checks.1
-
-private theorem checkedFan29Owner0Part1 :
-    fan29Owner0Part1.check (model29.B 0 ++ [step29.q]) 9000000000000
-      (model29.caps 0) 0 485 95100 12
-      ([-45000000000], [4320000000000]) = true := by
-  exact checkedFan29Owner0Part7Checks.2.1
-
-private theorem checkedFan29Owner0Part2 :
-    fan29Owner0Part2.check (model29.B 0 ++ [step29.q]) 9000000000000
-      (model29.caps 0) 0 485 95100 12
-      ([2997000000000, -2520000000000], [2106000000000, 5040000000000]) = true := by
-  exact checkedFan29Owner0Part7Checks.2.2.1
-
 private theorem checkedFan29Owner0Part3 :
     fan29Owner0Part3.check (model29.B 0 ++ [step29.q]) 9000000000000
       (model29.caps 0) 0 485 95100 12
       ([2250000000000], [45000000000]) = true := by
   exact checkedFan29Owner0Part7Checks.2.2.2.1
 
-private theorem checkedFan29Owner0Part4 :
-    fan29Owner0Part4.check (model29.B 0 ++ [step29.q]) 9000000000000
-      (model29.caps 0) 485 951 95100 12
-      ([-3828000000000, -2520000000000], [9756000000000, 5040000000000]) = true := by
-  exact checkedFan29Owner0Part7Checks.2.2.2.2.1
-
-private theorem checkedFan29Owner0Part5 :
-    fan29Owner0Part5.check (model29.B 0 ++ [step29.q]) 9000000000000
-      (model29.caps 0) 485 951 95100 12
-      ([-192000000000, 2520000000000], [6948000000000, 2520000000000]) = true := by
-  exact checkedFan29Owner0Part7Checks.2.2.2.2.2.1
-
-private theorem checkedFan29Owner0Part6 :
-    fan29Owner0Part6.check (model29.B 0 ++ [step29.q]) 9000000000000
-      (model29.caps 0) 485 951 95100 12
-      ([5100000000000], [4200000000000]) = true := by
-  exact checkedFan29Owner0Part7Checks.2.2.2.2.2.2.1
-
 private theorem checkedFan29Owner0Part7 :
     fan29Owner0Part7.check (model29.B 0 ++ [step29.q]) 9000000000000
       (model29.caps 0) 485 951 95100 12
diff --git a/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700001.lean b/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700001.lean
index 0ffd00e137..d189b9b042 100644
--- a/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700001.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700001.lean
@@ -1014,36 +1014,18 @@ private theorem checkedFan15Owner0Part5Checks :
     all_goals decide +kernel
   exact ⟨checkedTail0, checkedTail1, checkedTail2, checkedTail3, checkedTail4, checkedTail5⟩
 
-private theorem checkedFan15Owner0Part0 :
-    fan15Owner0Part0.check (model15.B 0 ++ [step15.q]) 9000000000000
-      (model15.caps 0) 0 740624 318861100 12
-      ([-660000000000], [2100000000000]) = true := by
-  exact checkedFan15Owner0Part5Checks.1
-
 private theorem checkedFan15Owner0Part1 :
     fan15Owner0Part1.check (model15.B 0 ++ [step15.q]) 9000000000000
       (model15.caps 0) 0 740624 318861100 12
       ([2193600000000, -2490000000000], [2329800000000, 4980000000000]) = true := by
   exact checkedFan15Owner0Part5Checks.2.1
 
-private theorem checkedFan15Owner0Part2 :
-    fan15Owner0Part2.check (model15.B 0 ++ [step15.q]) 9000000000000
-      (model15.caps 0) 740624 2083888 318861100 12
-      ([-1533000000000], [4785000000000]) = true := by
-  exact checkedFan15Owner0Part5Checks.2.2.1
-
 private theorem checkedFan15Owner0Part3 :
     fan15Owner0Part3.check (model15.B 0 ++ [step15.q]) 9000000000000
       (model15.caps 0) 740624 2083888 318861100 12
       ([796800000000, 4980000000000], [1041600000000, -2490000000000]) = true := by
   exact checkedFan15Owner0Part5Checks.2.2.2.1
 
-private theorem checkedFan15Owner0Part4 :
-    fan15Owner0Part4.check (model15.B 0 ++ [step15.q]) 9000000000000
-      (model15.caps 0) 2224 3403 340300 12
-      ([-1533000000000], [4785000000000]) = true := by
-  exact checkedFan15Owner0Part5Checks.2.2.2.2.1
-
 private theorem checkedFan15Owner0Part5 :
     fan15Owner0Part5.check (model15.B 0 ++ [step15.q]) 9000000000000
       (model15.caps 0) 2224 3403 340300 12
diff --git a/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700005.lean b/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700005.lean
index 436d012e6e..335e2a5bb4 100644
--- a/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700005.lean
+++ b/LeanPool/ConwaySoifer/Simplified/Certificates/Steps/Aown1600001700005.lean
@@ -782,12 +782,6 @@ private theorem checkedFan42Owner0Part1Checks :
     all_goals decide +kernel
   exact ⟨checkedTail0, checkedTail1⟩
 
-private theorem checkedFan42Owner0Part0 :
-    fan42Owner0Part0.check (model42.B 0 ++ [step42.q]) 9000000000000
-      (model42.caps 0) 0 1 100 12
-      ([-630000000000], [5895000000000]) = true := by
-  exact checkedFan42Owner0Part1Checks.1
-
 private theorem checkedFan42Owner0Part1 :
     fan42Owner0Part1.check (model42.B 0 ++ [step42.q]) 9000000000000
       (model42.caps 0) 0 1 100 12
@@ -948,12 +942,6 @@ private theorem checkedFan43Owner2Part1Checks :
     all_goals decide +kernel
   exact ⟨checkedTail0, checkedTail1⟩
 
-private theorem checkedFan43Owner2Part0 :
-    fan43Owner2Part0.check (model43.B 2 ++ [step43.q]) 9000000000000
-      (model43.caps 2) 0 1 100 12
-      ([0, -9000000000000], [3375000000000]) = true := by
-  exact checkedFan43Owner2Part1Checks.1
-
 private theorem checkedFan43Owner2Part1 :
     fan43Owner2Part1.check (model43.B 2 ++ [step43.q]) 9000000000000
       (model43.caps 2) 0 1 100 12
@@ -1142,48 +1130,24 @@ private theorem checkedFan44Owner2Part7Checks :
   exact ⟨checkedTail0, checkedTail1, checkedTail2, checkedTail3, checkedTail4, checkedTail5,
     checkedTail6, checkedTail7⟩
 
-private theorem checkedFan44Owner2Part0 :
-    fan44Owner2Part0.check (model44.B 2 ++ [step44.q]) 9000000000000
-      (model44.caps 2) 0 4464 2064600 12
-      ([-1440000000000, -9000000000000], [9000000000000, 0]) = true := by
-  exact checkedFan44Owner2Part7Checks.1
-
 private theorem checkedFan44Owner2Part1 :
     fan44Owner2Part1.check (model44.B 2 ++ [step44.q]) 9000000000000
       (model44.caps 2) 0 4464 2064600 12
       ([6165000000000], [2145000000000]) = true := by
   exact checkedFan44Owner2Part7Checks.2.1
 
-private theorem checkedFan44Owner2Part2 :
-    fan44Owner2Part2.check (model44.B 2 ++ [step44.q]) 9000000000000
-      (model44.caps 2) 4464 7533 2064600 12
-      ([-45000000000, -9000000000000], [480000000000, 0]) = true := by
-  exact checkedFan44Owner2Part7Checks.2.2.1
-
 private theorem checkedFan44Owner2Part3 :
     fan44Owner2Part3.check (model44.B 2 ++ [step44.q]) 9000000000000
       (model44.caps 2) 4464 7533 2064600 12
       ([5040000000000], [1395000000000]) = true := by
   exact checkedFan44Owner2Part7Checks.2.2.2.1
 
-private theorem checkedFan44Owner2Part4 :
-    fan44Owner2Part4.check (model44.B 2 ++ [step44.q]) 9000000000000
-      (model44.caps 2) 7533 10619 2064600 12
-      ([-1005000000000, -9000000000000], [8565000000000, 9000000000000]) = true := by
-  exact checkedFan44Owner2Part7Checks.2.2.2.2.1
-
 private theorem checkedFan44Owner2Part5 :
     fan44Owner2Part5.check (model44.B 2 ++ [step44.q]) 9000000000000
       (model44.caps 2) 7533 10619 2064600 12
       ([6165000000000], [2145000000000]) = true := by
   exact checkedFan44Owner2Part7Checks.2.2.2.2.2.1
 
-private theorem checkedFan44Owner2Part6 :
-    fan44Owner2Part6.check (model44.B 2 ++ [step44.q]) 9000000000000
-      (model44.caps 2) 287 558 55800 12
-      ([-210000000000, -9000000000000], [6690000000000, 9000000000000]) = true := by
-  exact checkedFan44Owner2Part7Checks.2.2.2.2.2.2.1
-
 private theorem checkedFan44Owner2Part7 :
     fan44Owner2Part7.check (model44.B 2 ++ [step44.q]) 9000000000000
       (model44.caps 2) 287 558 55800 12
@@ -1340,12 +1304,6 @@ private theorem checkedFan45Owner0Part1Checks :
     all_goals decide +kernel
   exact ⟨checkedTail0, checkedTail1⟩
 
-private theorem checkedFan45Owner0Part0 :
-    fan45Owner0Part0.check (model45.B 0 ++ [step45.q]) 9000000000000
-      (model45.caps 0) 0 1 100 12
-      ([-1185000000000], [8895000000000]) = true := by
-  exact checkedFan45Owner0Part1Checks.1
-
 private theorem checkedFan45Owner0Part1 :
     fan45Owner0Part1.check (model45.B 0 ++ [step45.q]) 9000000000000
       (model45.caps 0) 0 1 100 12
@@ -1501,12 +1459,6 @@ private theorem checkedFan46Owner0Part1Checks :
     all_goals decide +kernel
   exact ⟨checkedTail0, checkedTail1⟩
 
-private theorem checkedFan46Owner0Part0 :
-    fan46Owner0Part0.check (model46.B 0 ++ [step46.q]) 9000000000000
-      (model46.caps 0) 0 1 100 12
-      ([-780000000000], [5625000000000]) = true := by
-  exact checkedFan46Owner0Part1Checks.1
-
 private theorem checkedFan46Owner0Part1 :
     fan46Owner0Part1.check (model46.B 0 ++ [step46.q]) 9000000000000
       (model46.caps 0) 0 1 100 12