Narrow ConwaySoifer imports and stage certificate checks

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

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)

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

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

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

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. -/

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

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

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. -/

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. -/
 

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`

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`

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

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.

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`

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

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

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

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,

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

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

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`

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

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

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

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

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. -/
 

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. -/
 

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. -/
 

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

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

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

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

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