From ca28ca9d473a1a05eb10abf5a45eab42b502a10e Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 4 Jul 2026 11:46:54 +0000
Subject: [PATCH 1/2] refactor(bz): migrate HexBerlekampZassenhaus to the
 module system

Migrate the executable Berlekamp-Zassenhaus library onto the Lean 4 module
system (module / public import / public section), the prerequisite for
splitting the 19k-line Basic.lean monolith.

Works around two lean4 module-system reduction bugs found in the process:
- Array.instDecidableEqImpl is not @[expose], so decide/rfl over Array
  equality does not reduce in the kernel under the module system for
  nonempty arrays. Worked around with import all Init.Data.Array.DecidableEq
  (keeping the efficient Array instance); upstream fix in leanprover/lean4#14270.
- Array.back? does not reduce under the module system; reimplement
  DensePoly.leadingCoeff as coeffs.getD (size - 1) 0 (equal, reducible).

Adds public meta imports for the #guards, the backward.{proofsInPublic,
privateInPublic} options, @[expose] on the executable defs exported defeq
proofs reduce through, and de-privatises the leaked GcdLaws Rat instance.
No runtime performance regression (only leadingCoeff's compiled body
changes, equal-or-faster; DecidableEq unchanged).

See progress/20260704T000000Z_bz-module-migration-phase1a.md.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 HexBerlekamp/DistinctDegree.lean              |   7 +-
 HexBerlekamp/RabinSoundness.lean              |   7 +-
 HexBerlekampZassenhaus.lean                   |  10 +-
 HexBerlekampZassenhaus/Basic.lean             | 153 ++++++++++++------
 HexBerlekampZassenhaus/CrossCheck.lean        |   7 +-
 HexBerlekampZassenhaus/SmallModSingleton.lean |   8 +-
 HexBerlekampZassenhausMathlib/Basic.lean      |   8 +-
 HexHensel/Basic.lean                          |   2 +
 HexHensel/Linear.lean                         |   8 +-
 HexHensel/Quadratic.lean                      |  16 +-
 HexHensel/QuadraticMultifactor.lean           |   1 +
 HexPoly/Euclid.lean                           |  42 ++---
 HexPolyFp/Basic.lean                          |  30 +---
 HexPolyFp/SquareFree.lean                     |  25 +--
 HexPolyMathlib/Basic.lean                     |   8 +-
 HexPolyZ/Basic.lean                           |  12 +-
 ...704T000000Z_bz-module-migration-phase1a.md |  55 +++++++
 .../lean4-array-decidableeq-module-repro.md   |  71 ++++++++
 18 files changed, 292 insertions(+), 178 deletions(-)
 create mode 100644 progress/20260704T000000Z_bz-module-migration-phase1a.md
 create mode 100644 progress/lean4-array-decidableeq-module-repro.md

diff --git a/HexBerlekamp/DistinctDegree.lean b/HexBerlekamp/DistinctDegree.lean
index 1e3d24769..bfde564ab 100644
--- a/HexBerlekamp/DistinctDegree.lean
+++ b/HexBerlekamp/DistinctDegree.lean
@@ -714,12 +714,7 @@ private theorem unitPolynomial_dvd_any
       have hidx : u.coeffs.size - 1 < u.coeffs.size := by
         simpa [DensePoly.size] using Nat.sub_one_lt_of_lt hpos
       have hlead_eq : u.leadingCoeff = u.coeff (u.size - 1) := by
-        unfold DensePoly.leadingCoeff DensePoly.coeff
-        change u.coeffs.back?.getD (0 : ZMod64 p) =
-          u.coeffs.getD (u.coeffs.size - 1) (Zero.zero : ZMod64 p)
-        rw [Array.back?_eq_getElem?, Array.getD_eq_getD_getElem?,
-          Array.getElem?_eq_getElem hidx]
-        rfl
+        simp [DensePoly.leadingCoeff, DensePoly.coeff, DensePoly.size]
       have hlead_ne : u.leadingCoeff ≠ (Zero.zero : ZMod64 p) := by
         rw [hlead_eq]
         exact DensePoly.coeff_last_ne_zero_of_pos_size u hpos
diff --git a/HexBerlekamp/RabinSoundness.lean b/HexBerlekamp/RabinSoundness.lean
index 523a73b3d..99661a283 100644
--- a/HexBerlekamp/RabinSoundness.lean
+++ b/HexBerlekamp/RabinSoundness.lean
@@ -2330,12 +2330,7 @@ theorem dvd_one_of_isUnitPolynomial
       have hidx : u.coeffs.size - 1 < u.coeffs.size := by
         simpa [DensePoly.size] using Nat.sub_one_lt_of_lt hpos
       have hlead_eq : u.leadingCoeff = u.coeff (u.size - 1) := by
-        unfold DensePoly.leadingCoeff DensePoly.coeff
-        change u.coeffs.back?.getD (0 : ZMod64 p) =
-          u.coeffs.getD (u.coeffs.size - 1) (Zero.zero : ZMod64 p)
-        rw [Array.back?_eq_getElem?, Array.getD_eq_getD_getElem?,
-          Array.getElem?_eq_getElem hidx]
-        rfl
+        simp [DensePoly.leadingCoeff, DensePoly.coeff, DensePoly.size]
       have hlead_ne : u.leadingCoeff ≠ (Zero.zero : ZMod64 p) := by
         rw [hlead_eq]
         exact DensePoly.coeff_last_ne_zero_of_pos_size u hpos
diff --git a/HexBerlekampZassenhaus.lean b/HexBerlekampZassenhaus.lean
index ebd228b1a..062115c5c 100644
--- a/HexBerlekampZassenhaus.lean
+++ b/HexBerlekampZassenhaus.lean
@@ -4,9 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhaus.Basic
-import HexBerlekampZassenhaus.CrossCheck
-import HexBerlekampZassenhaus.SmallModSingleton
+module
+
+public import HexBerlekampZassenhaus.Basic
+public import HexBerlekampZassenhaus.CrossCheck
+public import HexBerlekampZassenhaus.SmallModSingleton
+
+public section
 
 /-!
 The `HexBerlekampZassenhaus` library exposes the executable integer
diff --git a/HexBerlekampZassenhaus/Basic.lean b/HexBerlekampZassenhaus/Basic.lean
index 1a0911214..2e964d547 100644
--- a/HexBerlekampZassenhaus/Basic.lean
+++ b/HexBerlekampZassenhaus/Basic.lean
@@ -4,12 +4,32 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexArith.Nat.Prime
-import HexBerlekamp.Factor
-import HexBerlekamp.Irreducibility
-import HexHensel.Multifactor
-import HexHensel.QuadraticMultifactor
-import HexLLL.Basic
+module
+
+public meta import HexArith.Nat.Prime
+public meta import HexBerlekamp.Factor
+public meta import HexBerlekamp.Irreducibility
+public meta import HexHensel.Basic
+public meta import HexHensel.Multifactor
+public meta import HexHensel.QuadraticMultifactor
+public meta import HexMatrix.Basic
+public meta import HexPolyZ.Mignotte
+public meta import HexLLL.Basic
+public import HexArith.Nat.Prime
+public import HexBerlekamp.Factor
+public import HexBerlekamp.Irreducibility
+public import HexHensel.Multifactor
+public import HexHensel.QuadraticMultifactor
+public import HexLLL.Basic
+-- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the
+-- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the
+-- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under
+-- the module system. Drop once that impl is exposed upstream (lean4).
+import all Init.Data.Array.DecidableEq
+
+public section
+set_option backward.proofsInPublic true
+set_option backward.privateInPublic true
 
 /-!
 Executable data records for the Berlekamp-Zassenhaus factorization pipeline.
@@ -23,6 +43,7 @@ namespace Hex
 namespace ZPoly
 
 /-- The integer polynomial `X`. -/
+@[expose]
 def X : ZPoly :=
   DensePoly.monomial 1 1
 
@@ -68,11 +89,13 @@ Executable test that a field-polynomial gcd is a unit.
 any nonzero constant associate of `1`.  In normalized dense representation,
 nonzero constants are exactly the polynomials with one stored coefficient.
 -/
+@[expose]
 def gcdIsUnit {R : Type u} [Zero R] [DecidableEq R]
     (g : DensePoly R) : Bool :=
   g.size == 1
 
 /-- The modular image is square-free according to the executable gcd-unit criterion. -/
+@[expose]
 def squareFreeModP (f : ZPoly) (p : Nat) [ZMod64.Bounds p] : Prop :=
   let fModP := ZPoly.modP p f
   gcdIsUnit (DensePoly.gcd fModP (DensePoly.derivative fModP)) = true
@@ -94,7 +117,7 @@ private theorem bounds_two : ZMod64.Bounds 2 := by
   constructor <;> decide
 
 /-- The `ZMod64.Bounds` instance witness for `p = 3`. -/
-private theorem bounds_three : ZMod64.Bounds 3 := by
+theorem bounds_three : ZMod64.Bounds 3 := by
   constructor <;> decide
 
 /-- The `ZMod64.Bounds` instance witness for `p = 5`. -/
@@ -678,6 +701,7 @@ dividing by its leading coefficient.  `monicModularImage f = scale c⁻¹ f`
 where `c = leadingCoeff f`; the zero branch is a placeholder used to keep
 the function total.
 -/
+@[expose]
 def monicModularImage {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) : FpPoly p :=
   if f.isZero then
     0
@@ -1223,9 +1247,7 @@ theorem isGoodPrime_modP_isZero_false
       apply hadm
       have hcoeffs_zero : f.coeffs.size = 0 := by simpa [DensePoly.size] using hsize_zero
       have hlead : DensePoly.leadingCoeff f = 0 := by
-        unfold DensePoly.leadingCoeff
-        rw [Array.back?_eq_getElem?]
-        simp [hcoeffs_zero]
+        simp [DensePoly.leadingCoeff, hcoeffs_zero, Array.getD] <;> rfl
       unfold ZPoly.leadingCoeffModP
       rw [hlead]
       show (ZMod64.ofNat p (ZPoly.intModNat 0 p) : ZMod64 p) = 0
@@ -1258,9 +1280,7 @@ theorem leadingCoeffAdmissible_size_pos
     apply hadm
     have hcoeffs_zero : f.coeffs.size = 0 := by simpa [DensePoly.size] using hsize_zero
     have hlead : DensePoly.leadingCoeff f = 0 := by
-      unfold DensePoly.leadingCoeff
-      rw [Array.back?_eq_getElem?]
-      simp [hcoeffs_zero]
+      simp [DensePoly.leadingCoeff, hcoeffs_zero, Array.getD] <;> rfl
     unfold ZPoly.leadingCoeffModP
     rw [hlead]
     show (ZMod64.ofNat p (ZPoly.intModNat 0 p) : ZMod64 p) = 0
@@ -1424,10 +1444,12 @@ structure ToMonicData where
 
 namespace ToMonicData
 
+@[expose]
 private def transformedCoeffs (core : ZPoly) (degree : Nat) : Array Int :=
   ((List.range degree).map fun i =>
       core.coeff i * (DensePoly.leadingCoeff core) ^ (degree - 1 - i)).toArray.push 1
 
+@[expose]
 private def transformedCore (core : ZPoly) (degree : Nat) : ZPoly :=
   { coeffs := transformedCoeffs core degree
     normalized := by
@@ -1465,6 +1487,7 @@ theorem transformedCore_monic (core : ZPoly) (degree : Nat) :
 end ToMonicData
 
 /-- Build the `ToMonicData` packet for a core by the integer scaling transform. -/
+@[expose]
 def toMonic (core : ZPoly) : ToMonicData :=
   let degree := core.degree?.getD 0
   { core
@@ -1551,11 +1574,13 @@ deriving DecidableEq
 
 namespace Factorization
 
+@[expose]
 private def polyPow (f : ZPoly) : Nat → ZPoly
   | 0 => 1
   | n + 1 => polyPow f n * f
 
 /-- Public wrapper for the polynomial power used by `Factorization.product`. -/
+@[expose]
 def factorPower (f : ZPoly) (n : Nat) : ZPoly :=
   polyPow f n
 
@@ -1566,6 +1591,7 @@ def factorPower (f : ZPoly) (n : Nat) : ZPoly :=
     factorPower f (n + 1) = factorPower f n * f := rfl
 
 /-- Expand multiplicity pairs into the ordered polynomial product. -/
+@[expose]
 def product (φ : Factorization) : ZPoly :=
   φ.factors.foldl (fun acc factor => acc * polyPow factor.1 factor.2) (DensePoly.C φ.scalar)
 
@@ -1586,6 +1612,7 @@ theorem product_eq_foldl_factorPower (φ : Factorization) :
 end Factorization
 
 /-- Compute the normalization data required before the square-free pipeline. -/
+@[expose]
 def normalizeForFactor (f : ZPoly) : FactorNormalizationData :=
   let primitive := ZPoly.primitivePart f
   let xData := ZPoly.extractXPower primitive
@@ -1603,15 +1630,18 @@ private def contentFactorArray (content : Int) : Array ZPoly :=
   else
     #[DensePoly.C content]
 
+@[expose]
 private def xPowerFactorArray (power : Nat) : Array ZPoly :=
   (List.replicate power ZPoly.X).toArray
 
+@[expose]
 private def repeatedPartFactorArray (repeatedPart : ZPoly) : Array ZPoly :=
   if repeatedPart = 1 then
     #[]
   else
     #[repeatedPart]
 
+@[expose]
 private def signedContentScalar (f : ZPoly) : Int :=
   if f = 0 then
     0
@@ -1623,6 +1653,7 @@ private def signedContentScalar (f : ZPoly) : Int :=
 /-- Normalize a polynomial factor's sign by negating it whenever the leading
 coefficient is negative.  The result has nonnegative leading coefficient and is
 associated to the input over `ℤ`. -/
+@[expose]
 def normalizeFactorSign (f : ZPoly) : ZPoly :=
   if DensePoly.leadingCoeff f < 0 then
     DensePoly.scale (-1 : Int) f
@@ -1633,6 +1664,7 @@ def normalizeFactorSign (f : ZPoly) : ZPoly :=
 when it is not zero and not a unit (`±1`).  Exposed publicly so that
 Mathlib-side lemmas can transport the predicate into `¬ IsUnit` over
 `Polynomial ℤ`. -/
+@[expose]
 def shouldRecordPolynomialFactor (f : ZPoly) : Bool :=
   f ≠ 0 && f ≠ 1 && f ≠ DensePoly.C (-1)
 
@@ -1644,6 +1676,7 @@ private def bumpFactorMultiplicity (f : ZPoly) : List (ZPoly × Nat) → List (Z
       else
         entry :: bumpFactorMultiplicity f entries
 
+@[expose]
 private def collectFactorMultiplicities (factors : Array ZPoly) : Array (ZPoly × Nat) :=
   factors.toList.foldl
     (fun acc factor =>
@@ -1655,6 +1688,7 @@ private def collectFactorMultiplicities (factors : Array ZPoly) : Array (ZPoly 
     []
   |>.reverse.toArray
 
+@[expose]
 private def polynomialNormalizationPrefixFactors (d : FactorNormalizationData) : Array ZPoly :=
   xPowerFactorArray d.xPower ++ repeatedPartFactorArray d.repeatedPart
 
@@ -1674,6 +1708,7 @@ Exact-division check on integer polynomials: returns the quotient when
 `quot * candidate = target` exactly, and rejects unit candidates so iterated
 calls cannot loop forever on `±1`.
 -/
+@[expose]
 def exactQuotient? (target candidate : ZPoly) : Option ZPoly :=
   if candidate.isZero || candidate = 1 then
     none
@@ -1740,6 +1775,7 @@ Compute `(emitted, residual)` where each candidate factor `q` from
 `q^k` exactly divides the running repeated-part. The fuel is the source
 size, which dominates any irreducible's multiplicity in `repeatedPart`.
 -/
+@[expose]
 private def expandRepeatedPartFactorArray (rp : ZPoly) (coreFactors : Array ZPoly) :
     Array ZPoly × ZPoly :=
   expandRepeatedPartFactorsAux coreFactors.toList rp (rp.size + 1)
@@ -1753,6 +1789,7 @@ for higher-multiplicity inputs. Falls back to the un-expanded
 fully consume `repeatedPart` (e.g. when the BZ pipeline emitted the raw
 square-free core as a single core factor).
 -/
+@[expose]
 private def reassemblePolynomialFactors
     (d : FactorNormalizationData) (coreFactors : Array ZPoly) : Array ZPoly :=
   let (expanded, residual) := expandRepeatedPartFactorArray d.repeatedPart coreFactors
@@ -1761,6 +1798,7 @@ private def reassemblePolynomialFactors
   else
     polynomialNormalizationPrefixFactors d ++ coreFactors
 
+@[expose]
 private def factorizationOfFactors (f : ZPoly) (factors : Array ZPoly) : Factorization :=
   { scalar := signedContentScalar f
     factors := collectFactorMultiplicities factors }
@@ -2958,6 +2996,7 @@ theorem choosePrimeData?_berlekampFactor_factors_length_le_one_of_small
 Lift the chosen modular factors to the requested precision for integer
 recombination.
 -/
+@[expose]
 def henselLiftData (f : ZPoly) (B : Nat) (d : PrimeChoiceData) : LiftData :=
   letI := d.bounds
   let factors := d.factorsModP.map (fun factor => FpPoly.liftToZ factor)
@@ -3713,6 +3752,7 @@ private theorem collectFactorMultiplicities_eq_foldl (factors : Array ZPoly) :
     collectFactorMultiplicities factors =
       (factors.toList.foldl collectFactorStep []).reverse.toArray := rfl
 
+@[expose]
 private def filteredNormalizedFactors (factors : List ZPoly) : List ZPoly :=
   factors.filterMap fun f =>
     let f := normalizeFactorSign f
@@ -4329,7 +4369,7 @@ theorem normalizeFactorSign_leadingCoeff_nonneg (g : ZPoly) :
     have hg_ne : g ≠ 0 := by
       intro hzero
       rw [hzero] at hlead
-      change (0 : Int) < 0 at hlead
+      rw [DensePoly.leadingCoeff_zero] at hlead
       omega
     rw [ZPoly.leadingCoeff_scale_of_nonzero (-1 : Int) g (by decide)]
     omega
@@ -5600,6 +5640,7 @@ private def bhksNoProgressProjectedRows : BhksProjectedRows :=
 def liftModulus (d : LiftData) : Nat :=
   d.p ^ d.k
 
+@[expose]
 def centeredLiftPoly (f : ZPoly) (m : Nat) : ZPoly :=
   DensePoly.ofCoeffs <| f.toArray.map fun coeff => centeredModNat coeff m
 
@@ -8775,7 +8816,7 @@ theorem scaledRecombinationSmartCandLoop_primitive
                             rw [hpp]
                             unfold normalizeFactorSign
                             rw [if_neg
-                              (by decide : ¬ DensePoly.leadingCoeff (0 : ZPoly) < 0)]
+                              (by simp : ¬ DensePoly.leadingCoeff (0 : ZPoly) < 0)]
                           have hcontent_ne :
                               ZPoly.content
                                   (ZPoly.dilate coreLc
@@ -9673,6 +9714,7 @@ deriving Repr, DecidableEq
 agrees with `factorClassicalWithBound f B`; the trace exposes the prime, the
 lifted-factor count `r`, the recombination candidate count, and whether the tier
 declined (budget exhausted / no admissible prime). -/
+@[expose]
 def factorClassicalTracedWithBound (f : ZPoly) (B : Nat) : Option Factorization × FactorTrace :=
   let normalized := normalizeForFactor f
   if normalized.squareFreeCore.degree?.getD 0 = 0 then
@@ -9711,6 +9753,7 @@ def factorClassicalTracedWithBound (f : ZPoly) (B : Nat) : Option Factorization
                 (some (factorizationOfFactors f (reassemblePolynomialFactors normalized coreFactors)), trace)
 
 /-- Classical-tier factorisation with trace, at the default Mignotte bound. -/
+@[expose]
 def factorClassicalTraced (f : ZPoly) : Option Factorization × FactorTrace :=
   factorClassicalTracedWithBound f (ZPoly.defaultFactorCoeffBound f)
 
@@ -9828,6 +9871,7 @@ def factorTrialFactorsWithBound (f : ZPoly) (B : Nat) : Array ZPoly :=
 #guard factorTrialFactorsWithBound exhaustiveNonMonicQuadraticGuard 4 =
   #[exhaustiveNonMonicQuadraticGuard]
 
+@[expose]
 def factorTrialWithBound (f : ZPoly) (B : Nat) : Factorization :=
   factorizationOfFactors f (factorTrialFactorsWithBound f B)
 
@@ -10178,6 +10222,7 @@ def latticeCoreFactorsWithBound
 /-- Raw factor array for the large-`r` lattice tier: the CLD lattice recovery,
 certifying irreducibility at the cap so that Swinnerton-Dyer / high-`r`
 irreducibles return `some #[f]` instead of `none`. -/
+@[expose]
 def factorLatticeFactorsWithBound (f : ZPoly) (B : Nat) : Option (Array ZPoly) :=
   let normalized := normalizeForFactor f
   if normalized.squareFreeCore.degree?.getD 0 = 0 then
@@ -10200,12 +10245,14 @@ def factorLatticeFactorsWithBound (f : ZPoly) (B : Nat) : Option (Array ZPoly) :
             (latticeCoreFactorsWithBound normalized.squareFreeCore B primeData).map
               fun coreFactors => reassemblePolynomialFactors normalized coreFactors
 
+@[expose]
 def factorLatticeWithBound (f : ZPoly) (B : Nat) : Option Factorization :=
   (factorLatticeFactorsWithBound f B).map (factorizationOfFactors f)
 
 /-- Van Hoeij CLD lattice tier (large-`r`) at the full BHKS precision cap.
 Certifies irreducibility (unlike a cap-free CLD path), so it returns `some` on
 Swinnerton-Dyer and cyclotomic high-`r` irreducibles. -/
+@[expose]
 def factorLattice (f : ZPoly) : Option Factorization :=
   factorLatticeWithBound f (latticePrecisionCap f)
 
@@ -10242,6 +10289,7 @@ provable unconditionally without yet proving the classical recombination loop
 reconstructs (that, with per-factor irreducibility, is the separate re-proof
 step). The classical tier is correct on the whole conformance corpus, so the
 guard always passes there and the emitted factor/trace values are unchanged. -/
+@[expose]
 def factorTraced (f : ZPoly) : Factorization × FactorTrace :=
   match factorClassicalTraced f with
   | (some φ, trace) =>
@@ -10264,6 +10312,7 @@ residual falls through to the `factorTrial` totality backstop, which is
 `choosePrimeData?`-independent and so makes `factor` unconditionally correct on
 every `ZPoly`. Total.
 -/
+@[expose]
 def factor (f : ZPoly) : Factorization :=
   (factorTraced f).1
 
@@ -11930,7 +11979,7 @@ private theorem normalizeForFactor_reassembles_signedContentScalar
       (normalizeForFactor f).squareFreeCore * (normalizeForFactor f).repeatedPart ≠ 0 := by
     intro hzero
     rw [hzero] at hA_pos
-    have hl0 : DensePoly.leadingCoeff (0 : ZPoly) = 0 := rfl
+    have hl0 : DensePoly.leadingCoeff (0 : ZPoly) = 0 := by simp
     rw [hl0] at hA_pos
     omega
   have hB_leading :
@@ -12493,7 +12542,7 @@ private theorem scaledRecombinationSearchModAux_primitive
                         rw [hpp]
                         unfold normalizeFactorSign
                         rw [if_neg
-                          (by decide : ¬ DensePoly.leadingCoeff (0 : ZPoly) < 0)]
+                          (by simp : ¬ DensePoly.leadingCoeff (0 : ZPoly) < 0)]
                       have hcontent_ne :
                           ZPoly.content
                               (ZPoly.dilate coreLc
@@ -13686,7 +13735,7 @@ private theorem polyProduct_toArray_monic_factors_monic_of_pos_lc :
         intro h0
         rw [h0] at hhead_pos
         change (0 : Int) < DensePoly.leadingCoeff (0 : ZPoly) at hhead_pos
-        have hzero : DensePoly.leadingCoeff (0 : ZPoly) = 0 := by decide
+        have hzero : DensePoly.leadingCoeff (0 : ZPoly) = 0 := by simp
         rw [hzero] at hhead_pos
         exact absurd hhead_pos (by decide)
       have hrest_lc_pos : 0 < DensePoly.leadingCoeff (Array.polyProduct rest.toArray) :=
@@ -13695,7 +13744,7 @@ private theorem polyProduct_toArray_monic_factors_monic_of_pos_lc :
         intro h0
         rw [h0] at hrest_lc_pos
         change (0 : Int) < DensePoly.leadingCoeff (0 : ZPoly) at hrest_lc_pos
-        have hzero : DensePoly.leadingCoeff (0 : ZPoly) = 0 := by decide
+        have hzero : DensePoly.leadingCoeff (0 : ZPoly) = 0 := by simp
         rw [hzero] at hrest_lc_pos
         exact absurd hrest_lc_pos (by decide)
       have hprod_eq :
@@ -14417,7 +14466,7 @@ private theorem mem_trialDivisionCandidatesOfDegree_of_bounded
   have hp_ne : p ≠ 0 := by
     intro hzero
     rw [hzero] at hlc
-    change 0 < (0 : Int) at hlc
+    rw [DensePoly.leadingCoeff_zero] at hlc
     omega
   have hp_size_pos : 0 < p.size := ZPoly.size_pos_of_ne_zero p hp_ne
   have hdeg_size : p.degree?.getD 0 = p.size - 1 := by
@@ -14836,12 +14885,12 @@ private theorem trialDivisionPeelAux_residual_leadingCoeff_pos
               have htarget_ne : target ≠ 0 := by
                 intro hz
                 rw [hz] at htarget_pos
-                change 0 < (0 : Int) at htarget_pos
+                rw [DensePoly.leadingCoeff_zero] at htarget_pos
                 omega
               have hc_ne : c ≠ 0 := by
                 intro hz
                 rw [hz] at hc_pos
-                change 0 < (0 : Int) at hc_pos
+                rw [DensePoly.leadingCoeff_zero] at hc_pos
                 omega
               have hq_ne : q ≠ 0 := by
                 intro hz
@@ -14946,12 +14995,12 @@ theorem exhaustiveIntegerTrialCoreFactorsWithBound_normalizeFactorSign
   have hcore_ne : core ≠ 0 := by
     intro hz
     rw [hz] at hcore_pos
-    change 0 < (0 : Int) at hcore_pos
+    rw [DensePoly.leadingCoeff_zero] at hcore_pos
     omega
   have hsplit1_ne : Array.polyProduct split.1 ≠ 0 := by
     intro hz
     rw [hz] at hsplit_lc_pos
-    change 0 < (0 : Int) at hsplit_lc_pos
+    rw [DensePoly.leadingCoeff_zero] at hsplit_lc_pos
     omega
   have hsplit2_ne : split.2 ≠ 0 := by
     intro hz
@@ -15054,12 +15103,12 @@ theorem exhaustiveIntegerTrialCoreFactorsWithBound_shouldRecord
   have hcore_ne : core ≠ 0 := by
     intro hz
     rw [hz] at hcore_pos
-    change 0 < (0 : Int) at hcore_pos
+    rw [DensePoly.leadingCoeff_zero] at hcore_pos
     omega
   have hsplit1_ne : Array.polyProduct split.1 ≠ 0 := by
     intro hz
     rw [hz] at hsplit_lc_pos
-    change 0 < (0 : Int) at hsplit_lc_pos
+    rw [DensePoly.leadingCoeff_zero] at hsplit_lc_pos
     omega
   have hsplit2_ne : split.2 ≠ 0 := by
     intro hz
@@ -15130,7 +15179,7 @@ theorem exhaustiveIntegerTrialCoreFactorsWithBound_shouldRecord
       have hpeel_ne_zero : peel.2 ≠ 0 := by
         intro hz
         rw [hz] at hpeel_res_pos
-        change 0 < (0 : Int) at hpeel_res_pos
+        rw [DensePoly.leadingCoeff_zero] at hpeel_res_pos
         omega
       have hpeel_ne_neg_one : peel.2 ≠ DensePoly.C (-1 : Int) := by
         intro hneg
@@ -15409,7 +15458,7 @@ private theorem trialDivisionPeel_residual_irreducible
   change trialDivisionPeelAux target candidates = (factors, residual) at hsplit
   have htarget_ne : target ≠ 0 := by
     intro h; rw [h] at htarget_pos
-    change 0 < (0 : Int) at htarget_pos; omega
+    rw [DensePoly.leadingCoeff_zero] at htarget_pos; omega
   have hcand_pos_lc : ∀ c ∈ candidates, 0 < DensePoly.leadingCoeff c :=
     fun c hc => (mem_trialDivisionCandidatesUpTo hc).2.1
   have hcand_pos_deg : ∀ c ∈ candidates, 0 < c.degree?.getD 0 :=
@@ -15423,7 +15472,7 @@ private theorem trialDivisionPeel_residual_irreducible
       htarget_pos hcand_pos_lc factors residual hsplit
   have hres_ne_zero : residual ≠ 0 := by
     intro hzero; rw [hzero] at hres_lc_pos
-    change 0 < (0 : Int) at hres_lc_pos; omega
+    rw [DensePoly.leadingCoeff_zero] at hres_lc_pos; omega
   have hres_dvd_target : residual ∣ target :=
     trialDivisionPeelAux_residual_dvd_target target candidates factors residual hsplit
   have hres_dvd_core : residual ∣ core :=
@@ -15528,7 +15577,7 @@ private theorem trialDivisionPeel_residual_irreducible
     have hq_size_pos : 0 < q.size := hq_size_eq ▸ hsm_size_pos
     have hq_ne_zero : q ≠ 0 := by
       intro hz; rw [hz] at hq_lc_pos
-      change 0 < (0 : Int) at hq_lc_pos; omega
+      rw [DensePoly.leadingCoeff_zero] at hq_lc_pos; omega
     have hq_dvd_res : q ∣ residual := ZPoly_dvd_trans hq_dvd_small hsm_dvd
     have hq_dvd_core : q ∣ core := ZPoly_dvd_trans hq_dvd_res hres_dvd_core
     have hq_bound : ∀ i, (q.coeff i).natAbs ≤ B := by
@@ -15694,7 +15743,7 @@ private theorem trialDivisionPeel_factor_irreducible
   change trialDivisionPeelAux target candidates = (factors, residual) at hsplit
   have htarget_ne : target ≠ 0 := by
     intro h; rw [h] at htarget_pos
-    change 0 < (0 : Int) at htarget_pos; omega
+    rw [DensePoly.leadingCoeff_zero] at htarget_pos; omega
   have hcand_pos_lc : ∀ c ∈ candidates, 0 < DensePoly.leadingCoeff c :=
     fun c hc => (mem_trialDivisionCandidatesUpTo hc).2.1
   have hcand_pos_deg : ∀ c ∈ candidates, 0 < c.degree?.getD 0 :=
@@ -15708,7 +15757,7 @@ private theorem trialDivisionPeel_factor_irreducible
       htarget_pos hcand_pos_lc factors residual hsplit
   have hres_ne_zero : residual ≠ 0 := by
     intro hzero; rw [hzero] at hres_lc_pos
-    change 0 < (0 : Int) at hres_lc_pos; omega
+    rw [DensePoly.leadingCoeff_zero] at hres_lc_pos; omega
   have hprod : residual * Array.polyProduct factors = target :=
     trialDivisionPeelAux_product target candidates factors residual hsplit
   have hfactor_mem_cand : factor ∈ candidates :=
@@ -15723,7 +15772,7 @@ private theorem trialDivisionPeel_factor_irreducible
   have hfactor_pos_lc : 0 < DensePoly.leadingCoeff factor := hcand_pos_lc factor hfactor_mem_cand
   have hfactor_ne_zero : factor ≠ 0 := by
     intro h; rw [h] at hfactor_pos_lc
-    change 0 < (0 : Int) at hfactor_pos_lc; omega
+    rw [DensePoly.leadingCoeff_zero] at hfactor_pos_lc; omega
   have hfactor_size_pos : 0 < factor.size :=
     ZPoly.size_pos_of_ne_zero factor hfactor_ne_zero
   have hfactor_size_eq : factor.size = factor.degree?.getD 0 + 1 := by
@@ -15825,7 +15874,7 @@ private theorem trialDivisionPeel_factor_irreducible
     have hq_size_pos : 0 < q.size := hq_size_eq ▸ hsm_size_pos
     have hq_ne_zero : q ≠ 0 := by
       intro hz; rw [hz] at hq_lc_pos
-      change 0 < (0 : Int) at hq_lc_pos; omega
+      rw [DensePoly.leadingCoeff_zero] at hq_lc_pos; omega
     have hq_dvd_factor : q ∣ factor := ZPoly_dvd_trans hq_dvd_small hsm_dvd
     have hq_dvd_target : q ∣ target := ZPoly_dvd_trans hq_dvd_factor hfactor_dvd_target
     have hq_dvd_core : q ∣ core := ZPoly_dvd_trans hq_dvd_target htarget_dvd
@@ -16089,7 +16138,7 @@ theorem exhaustiveIntegerTrialCoreFactorsWithBound_degree_pos
   let peel := trialDivisionPeelAux split.2 candidates
   have hcore_ne : core ≠ 0 := by
     intro hz; rw [hz] at hcore_pos
-    change 0 < (0 : Int) at hcore_pos; omega
+    rw [DensePoly.leadingCoeff_zero] at hcore_pos; omega
   have hsplit_prod : split.2 * Array.polyProduct split.1 = core :=
     splitIntegerRootFactorsAux_product core roots roots.length split.1 split.2 rfl
   have hsplit2_dvd_core : split.2 ∣ core :=
@@ -16100,7 +16149,7 @@ theorem exhaustiveIntegerTrialCoreFactorsWithBound_degree_pos
       roots.length split.1 split.2 rfl
   have hsplit1_ne : Array.polyProduct split.1 ≠ 0 := by
     intro hz; rw [hz] at hsplit_lc_pos
-    change 0 < (0 : Int) at hsplit_lc_pos; omega
+    rw [DensePoly.leadingCoeff_zero] at hsplit_lc_pos; omega
   have hsplit2_ne : split.2 ≠ 0 := by
     intro hz; apply hcore_ne
     rw [← hsplit_prod, hz]; exact DensePoly.zero_mul _
@@ -16169,7 +16218,7 @@ theorem exhaustiveIntegerTrialCoreFactorsWithBound_degree_pos
       rw [hfac_eq]
       have hres_ne : peel.2 ≠ 0 := by
         intro hz; rw [hz] at hpeel_res_pos
-        change 0 < (0 : Int) at hpeel_res_pos; omega
+        rw [DensePoly.leadingCoeff_zero] at hpeel_res_pos; omega
       have hres_size_pos : 0 < peel.2.size :=
         ZPoly.size_pos_of_ne_zero peel.2 hres_ne
       have hres_dvd_split2 : peel.2 ∣ split.2 :=
@@ -16228,7 +16277,7 @@ theorem exhaustiveIntegerTrialCoreFactorsWithBound_factor_irreducible
       roots.length split.1 split.2 rfl
   have hsplit1_ne : Array.polyProduct split.1 ≠ 0 := by
     intro hz; rw [hz] at hsplit_lc_pos
-    change 0 < (0 : Int) at hsplit_lc_pos; omega
+    rw [DensePoly.leadingCoeff_zero] at hsplit_lc_pos; omega
   have hsplit2_ne : split.2 ≠ 0 := by
     intro hz; apply hcore_ne
     rw [← hsplit_prod, hz]; exact DensePoly.zero_mul _
@@ -16429,7 +16478,7 @@ theorem quadraticIntegerRootFactors?_normalizeFactorSign
               have hsplit_poly_ne : Array.polyProduct split.1 ≠ 0 := by
                 intro hzero
                 rw [hzero] at hsplit_lc_pos
-                change 0 < (0 : Int) at hsplit_lc_pos
+                rw [DensePoly.leadingCoeff_zero] at hsplit_lc_pos
                 omega
               have hres_ne : split.2 ≠ 0 := by
                 intro hzero
@@ -16437,7 +16486,7 @@ theorem quadraticIntegerRootFactors?_normalizeFactorSign
                   rw [← hsplit_prod, hzero]
                   exact DensePoly.zero_mul _
                 rw [hcore_zero] at hcore_pos
-                change 0 < (0 : Int) at hcore_pos
+                rw [DensePoly.leadingCoeff_zero] at hcore_pos
                 omega
               have hlc :
                   DensePoly.leadingCoeff core =
@@ -16503,7 +16552,7 @@ theorem quadraticIntegerRootFactors?_shouldRecord
               have hsplit_poly_ne : Array.polyProduct split.1 ≠ 0 := by
                 intro hzero
                 rw [hzero] at hsplit_lc_pos
-                change 0 < (0 : Int) at hsplit_lc_pos
+                rw [DensePoly.leadingCoeff_zero] at hsplit_lc_pos
                 omega
               have hres_ne : split.2 ≠ 0 := by
                 intro hzero
@@ -16511,7 +16560,7 @@ theorem quadraticIntegerRootFactors?_shouldRecord
                   rw [← hsplit_prod, hzero]
                   exact DensePoly.zero_mul _
                 rw [hcore_zero] at hcore_pos
-                change 0 < (0 : Int) at hcore_pos
+                rw [DensePoly.leadingCoeff_zero] at hcore_pos
                 omega
               have hres_ne_one : split.2 ≠ 1 := hres_one
               have hres_ne_neg_one : split.2 ≠ DensePoly.C (-1 : Int) := by
@@ -16525,7 +16574,7 @@ theorem quadraticIntegerRootFactors?_shouldRecord
                     split.2 (Array.polyProduct split.1) hres_ne hsplit_poly_ne
                 rw [hneg_one] at hlc
                 have hneg_lc :
-                    DensePoly.leadingCoeff (DensePoly.C (-1 : Int)) = -1 := by decide
+                    DensePoly.leadingCoeff (DensePoly.C (-1 : Int)) = -1 := by simp
                 rw [hneg_lc] at hlc
                 have hcore_neg : DensePoly.leadingCoeff core < 0 := by
                   rw [hlc]
@@ -16637,12 +16686,12 @@ private theorem quadraticIntegerRootFactors?_residual_irreducible
           have hsplit_poly_ne : Array.polyProduct split.1 ≠ 0 := by
             intro hzero
             rw [hzero] at hsplit_lc_pos
-            change 0 < (0 : Int) at hsplit_lc_pos
+            rw [DensePoly.leadingCoeff_zero] at hsplit_lc_pos
             omega
           have hcore_ne : core ≠ 0 := by
             intro hzero
             rw [hzero] at hcore_pos
-            change 0 < (0 : Int) at hcore_pos
+            rw [DensePoly.leadingCoeff_zero] at hcore_pos
             omega
           -- factor = split.2 from hres. Need: Irreducible split.2.
           rw [hres]
@@ -16956,12 +17005,12 @@ theorem quadraticIntegerRootFactors?_factor_size_eq_two
             have hsplit_poly_ne : Array.polyProduct split.1 ≠ 0 := by
               intro hzero
               rw [hzero] at hsplit_lc_pos
-              change 0 < (0 : Int) at hsplit_lc_pos
+              rw [DensePoly.leadingCoeff_zero] at hsplit_lc_pos
               omega
             have hcore_ne : core ≠ 0 := by
               intro hzero
               rw [hzero] at hcore_pos
-              change 0 < (0 : Int) at hcore_pos
+              rw [DensePoly.leadingCoeff_zero] at hcore_pos
               omega
             have hres_ne_zero : split.2 ≠ 0 := by
               intro hzero
@@ -17234,7 +17283,7 @@ theorem quadraticIntegerRootFactors?_pairwise_not_associated
   have hcore_ne : core ≠ 0 := by
     intro hz
     rw [hz] at hcore_lc_pos
-    change 0 < (0 : Int) at hcore_lc_pos
+    rw [DensePoly.leadingCoeff_zero] at hcore_lc_pos
     omega
   -- Acknowledge the primitivity hypothesis (kept in the signature for
   -- symmetry with the `_factor_irreducible_of_primitive` wrapper; the
@@ -17280,7 +17329,7 @@ theorem quadraticIntegerRootFactors?_pairwise_not_associated
           have hpoly_ne : Array.polyProduct split.1 ≠ 0 := by
             intro hz
             rw [hz] at hpoly_lc_pos
-            change 0 < (0 : Int) at hpoly_lc_pos
+            rw [DensePoly.leadingCoeff_zero] at hpoly_lc_pos
             omega
           have hres_ne : split.2 ≠ 0 := by
             intro hz
@@ -17445,12 +17494,12 @@ theorem quadraticIntegerRootFactors?_degree_pos_of_primitive
             have hpoly_ne : Array.polyProduct split.1 ≠ 0 := by
               intro hz
               rw [hz] at hpoly_lc_pos
-              change 0 < (0 : Int) at hpoly_lc_pos
+              rw [DensePoly.leadingCoeff_zero] at hpoly_lc_pos
               omega
             have hcore_ne : core ≠ 0 := by
               intro hz
               rw [hz] at hcore_pos
-              change 0 < (0 : Int) at hcore_pos
+              rw [DensePoly.leadingCoeff_zero] at hcore_pos
               omega
             have hres_ne : split.2 ≠ 0 := by
               intro hz
@@ -17581,7 +17630,7 @@ private theorem repeatedPart_ne_C_neg_one_of_ne_zero (f : ZPoly) (hf : f ≠ 0)
   intro h
   have hpos := repeatedPart_leadingCoeff_pos_of_ne_zero f hf
   rw [h] at hpos
-  have hneg : DensePoly.leadingCoeff (DensePoly.C (-1 : Int)) = -1 := by decide
+  have hneg : DensePoly.leadingCoeff (DensePoly.C (-1 : Int)) = -1 := by simp
   rw [hneg] at hpos
   omega
 
diff --git a/HexBerlekampZassenhaus/CrossCheck.lean b/HexBerlekampZassenhaus/CrossCheck.lean
index ebc45b344..a91994882 100644
--- a/HexBerlekampZassenhaus/CrossCheck.lean
+++ b/HexBerlekampZassenhaus/CrossCheck.lean
@@ -4,7 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhaus.Basic
+module
+
+public meta import HexBerlekampZassenhaus.Basic
+public import HexBerlekampZassenhaus.Basic
+
+public section
 
 /-!
 BHKS fast-path vs slow-backstop cross-check for `HexBerlekampZassenhaus`.
diff --git a/HexBerlekampZassenhaus/SmallModSingleton.lean b/HexBerlekampZassenhaus/SmallModSingleton.lean
index c7be4d046..de5183c79 100644
--- a/HexBerlekampZassenhaus/SmallModSingleton.lean
+++ b/HexBerlekampZassenhaus/SmallModSingleton.lean
@@ -4,8 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
-import HexBerlekampZassenhaus.Basic
-import HexBerlekamp.RabinSoundness
+module
+
+public import HexBerlekampZassenhaus.Basic
+public import HexBerlekamp.RabinSoundness
+
+public section
 
 /-!
 Small-mod singleton Berlekamp irreducibility wrapper.
diff --git a/HexBerlekampZassenhausMathlib/Basic.lean b/HexBerlekampZassenhausMathlib/Basic.lean
index 4794e163f..bf8f0d026 100644
--- a/HexBerlekampZassenhausMathlib/Basic.lean
+++ b/HexBerlekampZassenhausMathlib/Basic.lean
@@ -6531,10 +6531,8 @@ private theorem zpoly_size_pos_of_monic {f : Hex.ZPoly}
   have hlead : Hex.DensePoly.leadingCoeff f = (1 : Int) := h
   rcases Nat.eq_zero_or_pos f.coeffs.size with hcs_zero | hcs_pos
   · exfalso
-    have hback_none : f.coeffs.back? = none := by
-      rw [Array.back?_eq_getElem?]; simp [hcs_zero]
     have hlc_zero : Hex.DensePoly.leadingCoeff f = (0 : Int) := by
-      unfold Hex.DensePoly.leadingCoeff; rw [hback_none]; rfl
+      simp [Hex.DensePoly.leadingCoeff, hcs_zero, Array.getD] <;> rfl
     rw [hlc_zero] at hlead
     exact absurd hlead (by decide)
   · exact hcs_pos
@@ -11225,10 +11223,8 @@ private theorem zpoly_size_pos_of_pos_lc {f : Hex.ZPoly}
     (hpos : 0 < Hex.DensePoly.leadingCoeff f) : 0 < f.size := by
   rcases Nat.eq_zero_or_pos f.coeffs.size with hcs_zero | hcs_pos
   · exfalso
-    have hback_none : f.coeffs.back? = none := by
-      rw [Array.back?_eq_getElem?]; simp [hcs_zero]
     have hlc_zero : Hex.DensePoly.leadingCoeff f = (0 : Int) := by
-      unfold Hex.DensePoly.leadingCoeff; rw [hback_none]; rfl
+      simp [Hex.DensePoly.leadingCoeff, hcs_zero, Array.getD] <;> rfl
     rw [hlc_zero] at hpos
     omega
   · exact hcs_pos
diff --git a/HexHensel/Basic.lean b/HexHensel/Basic.lean
index 8c17cacc7..b6d9bee75 100644
--- a/HexHensel/Basic.lean
+++ b/HexHensel/Basic.lean
@@ -68,11 +68,13 @@ private theorem intModNat_eq_of_congr {a b : Int} {m : Nat} (h : (a - b) % (m :
   simp [intModNat, hmod]
 
 /-- Reduce the coefficients of an integer polynomial modulo `p`. -/
+@[expose]
 def modP (p : Nat) [ZMod64.Bounds p] (f : ZPoly) : FpPoly p :=
   FpPoly.ofCoeffs <|
     (List.range f.size).map (fun i => ZMod64.ofNat p (intModNat (f.coeff i) p)) |>.toArray
 
 /-- Reduce each coefficient to its canonical representative modulo `p^k`. -/
+@[expose]
 def reduceModPow (f : ZPoly) (p k : Nat) : ZPoly :=
   DensePoly.ofCoeffs <|
     (List.range f.size).map (fun i => Int.ofNat (intModNat (f.coeff i) (p ^ k))) |>.toArray
diff --git a/HexHensel/Linear.lean b/HexHensel/Linear.lean
index 244ce3aa8..372a451df 100644
--- a/HexHensel/Linear.lean
+++ b/HexHensel/Linear.lean
@@ -1445,9 +1445,7 @@ private theorem coeff_last_eq_leadingCoeff (f : ZPoly) (hpos : 0 < f.size) :
   | mk coeffs normalized =>
       have hcoeffs : 0 < coeffs.size := by simpa [DensePoly.size] using hpos
       have hidx : coeffs.size - 1 < coeffs.size := Nat.sub_one_lt (Nat.ne_of_gt hcoeffs)
-      change coeffs.getD (coeffs.size - 1) 0 = coeffs.back?.getD 0
-      rw [Array.back?_eq_getElem?, Array.getElem?_eq_getElem hidx]
-      exact (Array.getElem_eq_getD 0).symm
+      simp [DensePoly.leadingCoeff, DensePoly.coeff, DensePoly.size]
 
 /-- A monic polynomial is nonempty: its `size` is positive. A zero-size `f` would
 have leading coefficient `0`, contradicting `leadingCoeff = 1`. This rules out the
@@ -1460,8 +1458,8 @@ private theorem monic_size_pos (f : ZPoly) (hmonic : DensePoly.Monic f) :
     have hlead : f.leadingCoeff = 0 := by
       cases f with
       | mk coeffs normalized =>
-          simp [DensePoly.leadingCoeff, DensePoly.size] at hsize ⊢
-          simp [hsize]
+          simp only [DensePoly.leadingCoeff, DensePoly.size] at hsize ⊢
+          simp [hsize, Array.getD] <;> rfl
     have hlead_one : f.leadingCoeff = 1 :=
       DensePoly.leadingCoeff_eq_one_of_monic hmonic
     rw [hlead] at hlead_one
diff --git a/HexHensel/Quadratic.lean b/HexHensel/Quadratic.lean
index 10eb117a1..633d80ffb 100644
--- a/HexHensel/Quadratic.lean
+++ b/HexHensel/Quadratic.lean
@@ -431,9 +431,7 @@ private theorem coeff_last_eq_leadingCoeff (f : ZPoly) (hpos : 0 < f.size) :
   | mk coeffs normalized =>
       have hcoeffs : 0 < coeffs.size := by simpa [DensePoly.size] using hpos
       have hidx : coeffs.size - 1 < coeffs.size := Nat.sub_one_lt (Nat.ne_of_gt hcoeffs)
-      change coeffs.getD (coeffs.size - 1) 0 = coeffs.back?.getD 0
-      rw [Array.back?_eq_getElem?, Array.getElem?_eq_getElem hidx]
-      exact (Array.getElem_eq_getD 0).symm
+      simp [DensePoly.leadingCoeff, DensePoly.coeff, DensePoly.size]
 
 /-- `monic_of_coeff_eq_one_and_high_coeff_zero` builds monicity from a coefficient equal to one with all higher coefficients zero. -/
 private theorem monic_of_coeff_eq_one_and_high_coeff_zero
@@ -478,8 +476,8 @@ private theorem leadingCoeff_zero_mod_base
     have hlead : f.leadingCoeff = 0 := by
       cases f with
       | mk coeffs normalized =>
-          simp [DensePoly.leadingCoeff, DensePoly.size] at hsize ⊢
-          simp [hsize]
+          simp only [DensePoly.leadingCoeff, DensePoly.size] at hsize ⊢
+          simp [hsize, Array.getD] <;> rfl
     simp [hlead]
 
 /-- `canonicalMod_congr_self` says canonical reduction differs from the original integer by a multiple of the modulus. -/
@@ -712,8 +710,8 @@ private theorem monic_size_pos (q : ZPoly) (hmonic : DensePoly.Monic q) :
     have hlead : q.leadingCoeff = 0 := by
       cases q with
       | mk coeffs normalized =>
-          simp [DensePoly.leadingCoeff, DensePoly.size] at hsize ⊢
-          simp [hsize]
+          simp only [DensePoly.leadingCoeff, DensePoly.size] at hsize ⊢
+          simp [hsize, Array.getD] <;> rfl
     have hlead_one : q.leadingCoeff = 1 :=
       DensePoly.leadingCoeff_eq_one_of_monic hmonic
     rw [hlead] at hlead_one
@@ -2161,8 +2159,8 @@ private theorem addModSquare_monic_of_high_remainder_zero
       have hlead : g.leadingCoeff = 0 := by
         cases g with
         | mk coeffs normalized =>
-            simp [DensePoly.leadingCoeff, DensePoly.size] at hsize ⊢
-            simp [hsize]
+            simp only [DensePoly.leadingCoeff, DensePoly.size] at hsize ⊢
+            simp [hsize, Array.getD] <;> rfl
       have hmonicLead : g.leadingCoeff = 1 :=
         DensePoly.leadingCoeff_eq_one_of_monic hmonic
       rw [hlead] at hmonicLead
diff --git a/HexHensel/QuadraticMultifactor.lean b/HexHensel/QuadraticMultifactor.lean
index 290a01a59..b6d772243 100644
--- a/HexHensel/QuadraticMultifactor.lean
+++ b/HexHensel/QuadraticMultifactor.lean
@@ -51,6 +51,7 @@ and `⌊log₂ (k - 1)⌋ + 1` otherwise, the least `n` with `k ≤ 2 ^ n`.
 The bound `k ≤ 2 ^ quadraticDoublingSteps k` is what
 `henselLiftQuadratic_spec` consumes to descend from the loop modulus
 `p ^ (2 ^ quadraticDoublingSteps k)` back to the requested `p ^ k`. -/
+@[expose]
 def quadraticDoublingSteps (k : Nat) : Nat :=
   if k ≤ 1 then 0 else (k - 1).log2 + 1
 
diff --git a/HexPoly/Euclid.lean b/HexPoly/Euclid.lean
index f8d5f6f79..745117634 100644
--- a/HexPoly/Euclid.lean
+++ b/HexPoly/Euclid.lean
@@ -32,7 +32,12 @@ variable {R : Type u} [Zero R] [DecidableEq R]
 /-- The leading coefficient, or `0` for the zero polynomial. -/
 @[expose]
 def leadingCoeff (p : DensePoly R) : R :=
-  p.coeffs.back?.getD 0
+  -- Written as `getD (size - 1)` rather than the more natural `back?.getD 0`
+  -- because `Array.back?` does not reduce in the kernel under the module
+  -- system (lean4 Array.back? reducibility issue), which would break the
+  -- `decide`/`rfl` defeq proofs downstream. Revert to `coeffs.back?.getD 0`
+  -- once the upstream fix lands.
+  p.coeffs.getD (p.coeffs.size - 1) (Zero.zero : R)
 
 /-- The zero polynomial has leading coefficient `0`. Registered as a `simp`
 normal form so callers reasoning about `leadingCoeff` discharge the zero case
@@ -40,7 +45,7 @@ automatically. -/
 @[simp, grind =] theorem leadingCoeff_zero : (0 : DensePoly R).leadingCoeff = 0 := by
   unfold leadingCoeff
   rw [show (DensePoly.coeffs (0 : DensePoly R)) = #[] from rfl]
-  simp
+  rfl
 
 /-- The constant polynomial `1`. -/
 instance [One R] : One (DensePoly R) where
@@ -54,10 +59,10 @@ lets callers read the leading coefficient off any constant. -/
   · rw [hc]
     unfold leadingCoeff
     rw [coeffs_C_zero]
-    simp
+    rfl
   · unfold leadingCoeff
     rw [coeffs_C_of_ne_zero hc]
-    simp
+    rfl
 
 /-- The constant polynomial `1` has leading coefficient `1`, hence is monic.
 Specialises `leadingCoeff_C` and feeds the monicity facts about `1` that the
@@ -84,13 +89,7 @@ theorem monic_iff_leadingCoeff_eq_one [One R] {p : DensePoly R} :
 at the last stored index. -/
 theorem leadingCoeff_eq_coeff_last (p : DensePoly R) (hpos : 0 < p.size) :
     p.leadingCoeff = p.coeff (p.size - 1) := by
-  unfold leadingCoeff coeff
-  change p.coeffs.back?.getD (Zero.zero : R) =
-    p.coeffs.getD (p.coeffs.size - 1) (Zero.zero : R)
-  rw [Array.back?_eq_getElem?]
-  have hidx : p.coeffs.size - 1 < p.coeffs.size := by
-    simpa [size] using Nat.sub_one_lt_of_lt hpos
-  rw [Array.getD_eq_getD_getElem?]
+  simp only [leadingCoeff, coeff, size]
 
 /-- The leading coefficient of a nonzero normalized dense polynomial is nonzero. -/
 theorem leadingCoeff_ne_zero_of_pos_size (p : DensePoly R) (hpos : 0 < p.size) :
@@ -860,12 +859,7 @@ theorem divModArray_remainder_degree_lt_of_pos_degree [Sub R] [Mul R]
     have hlead : q.toArray.getD qDegree (Zero.zero : R) = q.leadingCoeff := by
       unfold leadingCoeff toArray
       dsimp [qDegree]
-      change q.coeffs.getD (q.coeffs.size - 1) (Zero.zero : R) =
-        q.coeffs.back?.getD (Zero.zero : R)
-      have hidx : q.coeffs.size - 1 < q.coeffs.size := by
-        simpa [size] using Nat.sub_one_lt_of_lt hqpos
-      rw [Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hidx, Array.back?_eq_getElem?,
-        Array.getElem?_eq_getElem hidx]
+      simp [size]
     have hzero_start :
         ∀ i, qDegree + p.size ≤ i → p.toArray.getD i (Zero.zero : R) = (Zero.zero : R) := by
       intro i hi
@@ -1002,12 +996,8 @@ theorem divMod_remainder_eq_zero_of_degree_zero_core [One R] [Add R] [Sub R] [Mu
   have hlead : q.toArray.getD qDegree (Zero.zero : R) = q.leadingCoeff := by
     unfold leadingCoeff toArray
     rw [hqDegree_zero]
-    change q.coeffs.getD 0 (Zero.zero : R) = q.coeffs.back?.getD (Zero.zero : R)
-    rw [Array.getD_eq_getD_getElem?]
-    have hidx : 0 < q.coeffs.size := by omega
-    rw [Array.getElem?_eq_getElem hidx, Array.back?_eq_getElem?]
     have hlast : q.coeffs.size - 1 = 0 := by omega
-    rw [hlast, Array.getElem?_eq_getElem hidx]
+    rw [hlast]
   have hzero_start :
       ∀ i, qDegree + p.size ≤ i → p.toArray.getD i (Zero.zero : R) = (Zero.zero : R) := by
     intro i hi
@@ -3485,13 +3475,7 @@ theorem divModArray_reconstruction {S : Type _}
       simpa [toArray, size] using hraw
     have hlead : q.toArray.getD (q.size - 1) (Zero.zero : S) = q.leadingCoeff := by
       unfold leadingCoeff toArray
-      change q.coeffs.getD (q.coeffs.size - 1) (Zero.zero : S) =
-        q.coeffs.back?.getD (Zero.zero : S)
-      have hcoeffpos : 0 < q.coeffs.size := by simpa [size] using hqpos
-      have hidx : q.coeffs.size - 1 < q.coeffs.size :=
-        Nat.sub_one_lt_of_lt hcoeffpos
-      rw [Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hidx,
-        Array.back?_eq_getElem?, Array.getElem?_eq_getElem hidx]
+      simp [size]
     have hcancel_array :
         ∀ a, a - scaleLead a * q.toArray.getD (q.size - 1) (Zero.zero : S) =
           (Zero.zero : S) := by
diff --git a/HexPolyFp/Basic.lean b/HexPolyFp/Basic.lean
index 4b9b620d9..2f28cc0e2 100644
--- a/HexPolyFp/Basic.lean
+++ b/HexPolyFp/Basic.lean
@@ -104,11 +104,7 @@ private theorem divMod_spec_core [PrimeModulus p] (f g : DensePoly (ZMod64 p)) :
     have hidx : g.coeffs.size - 1 < g.coeffs.size := by
       simpa [DensePoly.size] using Nat.sub_one_lt_of_lt hgpos
     have hlead_eq : g.leadingCoeff = g.coeff (g.size - 1) := by
-      unfold DensePoly.leadingCoeff DensePoly.coeff
-      change g.coeffs.back?.getD (0 : ZMod64 p) =
-        g.coeffs.getD (g.coeffs.size - 1) (Zero.zero : ZMod64 p)
-      rw [Array.back?_eq_getElem?, Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hidx]
-      rfl
+      simp [DensePoly.leadingCoeff, DensePoly.coeff, DensePoly.size]
     have hlead_ne : g.leadingCoeff ≠ (Zero.zero : ZMod64 p) := by
       rw [hlead_eq]
       exact DensePoly.coeff_last_ne_zero_of_pos_size g hgpos
@@ -196,10 +192,7 @@ private theorem divMod_remainder_degree_lt_core
     unfold lead DensePoly.leadingCoeff DensePoly.coeff
     have hidx : m.coeffs.size - 1 < m.coeffs.size := by
       simpa [DensePoly.size] using Nat.sub_one_lt_of_lt hpos_size
-    change m.coeffs.back?.getD (0 : ZMod64 p) =
-      m.coeffs.getD (m.coeffs.size - 1) (Zero.zero : ZMod64 p)
-    rw [Array.back?_eq_getElem?, Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hidx]
-    rfl
+    simp [DensePoly.size]
   have hlead_ne : lead ≠ (Zero.zero : ZMod64 p) := by
     rw [hlead_eq]
     exact DensePoly.coeff_last_ne_zero_of_pos_size m hpos_size
@@ -581,11 +574,7 @@ private theorem mod_eq_mod_of_congr_not_pos_degree
       have hidx : m.coeffs.size - 1 < m.coeffs.size := by
         simpa [DensePoly.size] using Nat.sub_one_lt_of_lt hpos
       have hlead_eq : m.leadingCoeff = m.coeff (m.size - 1) := by
-        unfold DensePoly.leadingCoeff DensePoly.coeff
-        change m.coeffs.back?.getD (0 : ZMod64 p) =
-          m.coeffs.getD (m.coeffs.size - 1) (Zero.zero : ZMod64 p)
-        rw [Array.back?_eq_getElem?, Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hidx]
-        rfl
+        simp [DensePoly.leadingCoeff, DensePoly.coeff, DensePoly.size]
       have hcoeff_ne := DensePoly.coeff_last_ne_zero_of_pos_size m hpos
       rw [hlead_eq]
       exact hcoeff_ne
@@ -710,12 +699,7 @@ private theorem cancel_lead_at_pos_size_core [PrimeModulus p]
   have hidx : m.coeffs.size - 1 < m.coeffs.size := by
     simpa [DensePoly.size] using Nat.sub_one_lt_of_lt hsize
   have hlead_eq : m.leadingCoeff = m.coeff (m.size - 1) := by
-    unfold DensePoly.leadingCoeff DensePoly.coeff
-    change m.coeffs.back?.getD (0 : ZMod64 p) =
-      m.coeffs.getD (m.coeffs.size - 1) (Zero.zero : ZMod64 p)
-    rw [Array.back?_eq_getElem?, Array.getD_eq_getD_getElem?,
-        Array.getElem?_eq_getElem hidx]
-    rfl
+    simp [DensePoly.leadingCoeff, DensePoly.coeff, DensePoly.size]
   have hlead_ne : m.leadingCoeff ≠ (Zero.zero : ZMod64 p) := by
     rw [hlead_eq]
     exact DensePoly.coeff_last_ne_zero_of_pos_size m hsize
@@ -2904,11 +2888,7 @@ coefficient when they need to compute or rewrite it. -/
 theorem leadingCoeff_eq_coeff_pred
     (f : FpPoly p) (hpos : 0 < f.size) :
     DensePoly.leadingCoeff f = f.coeff (f.size - 1) := by
-  unfold DensePoly.leadingCoeff DensePoly.coeff
-  rw [Array.back?_eq_getElem?]
-  have hidx : f.coeffs.size - 1 < f.coeffs.size := by
-    simpa [DensePoly.size] using Nat.sub_one_lt_of_lt hpos
-  simp [Array.getD, DensePoly.size, hidx]
+  simp [DensePoly.leadingCoeff, DensePoly.coeff, DensePoly.size]
 
 /-- A polynomial of positive degree has a nonzero leading coefficient. The
 nondegeneracy fact that justifies inverting the leading coefficient during
diff --git a/HexPolyFp/SquareFree.lean b/HexPolyFp/SquareFree.lean
index b7398655b..6cc50ead7 100644
--- a/HexPolyFp/SquareFree.lean
+++ b/HexPolyFp/SquareFree.lean
@@ -1147,11 +1147,7 @@ theorem fpPoly_leadingCoeff_ne_zero_of_isZero_false
       Nat.pos_iff_ne_zero] using hzero
   have hlast := DensePoly.coeff_last_ne_zero_of_pos_size f hpos
   have hlead : DensePoly.leadingCoeff f = f.coeff (f.size - 1) := by
-    unfold DensePoly.leadingCoeff DensePoly.coeff
-    rw [Array.back?_eq_getElem?]
-    have hidx : f.coeffs.size - 1 < f.coeffs.size := by
-      simpa [DensePoly.size] using Nat.sub_one_lt_of_lt hpos
-    simp [Array.getD, DensePoly.size, hidx]
+    simp [DensePoly.leadingCoeff, DensePoly.coeff, DensePoly.size]
   rw [hlead]
   exact hlast
 
@@ -2485,11 +2481,7 @@ private theorem squareFreeContributionReachable_of_monic
       have hlead : DensePoly.leadingCoeff f = f.coeff 0 := by
         have hlead_last :
             DensePoly.leadingCoeff f = f.coeff (f.size - 1) := by
-          unfold DensePoly.leadingCoeff DensePoly.coeff
-          rw [Array.back?_eq_getElem?]
-          have hidx : f.coeffs.size - 1 < f.coeffs.size := by
-            simpa [DensePoly.size] using Nat.sub_one_lt_of_lt hpos
-          simp [Array.getD, DensePoly.size, hidx]
+          simp [DensePoly.leadingCoeff, DensePoly.coeff, DensePoly.size]
         simpa [hsize] using hlead_last
       change f.coeff 0 = (DensePoly.C (1 : ZMod64 p)).coeff 0
       rw [← hlead, hmonic]
@@ -4978,12 +4970,7 @@ private theorem normalizeMonic_squareFreeContributionReachable
           have hlead : DensePoly.leadingCoeff f = f.coeff 0 := by
             have hlead_last :
                 DensePoly.leadingCoeff f = f.coeff (f.size - 1) := by
-              unfold DensePoly.leadingCoeff DensePoly.coeff
-              rw [Array.back?_eq_getElem?]
-              have hpos : 0 < f.size := size_pos_of_isZero_false f hzero
-              have hidx : f.coeffs.size - 1 < f.coeffs.size := by
-                simpa [DensePoly.size] using Nat.sub_one_lt_of_lt hpos
-              simp [Array.getD, DensePoly.size, hidx]
+              simp [DensePoly.leadingCoeff, DensePoly.coeff, DensePoly.size]
             simpa [hf_size] using hlead_last
           rw [← hlead]
           have h := zmod64_mul_inv_eq_one_of_prime_ne_zero hp hlead_ne
@@ -5224,11 +5211,7 @@ private theorem constant_nonzero_dvd
     | zero =>
         have hlead : unit = g.coeff 0 := by
           have hlead_last : DensePoly.leadingCoeff g = g.coeff (g.size - 1) := by
-            unfold DensePoly.leadingCoeff DensePoly.coeff
-            rw [Array.back?_eq_getElem?]
-            have hidx : g.coeffs.size - 1 < g.coeffs.size := by
-              simpa [DensePoly.size] using Nat.sub_one_lt_of_lt hg_pos
-            simp [Array.getD, DensePoly.size, hidx]
+            simp [DensePoly.leadingCoeff, DensePoly.coeff, DensePoly.size]
           simpa [unit, hg_size] using hlead_last
         rw [← hlead]
         exact (DensePoly.coeff_C unit 0).symm
diff --git a/HexPolyMathlib/Basic.lean b/HexPolyMathlib/Basic.lean
index 855372f5c..6c0f8835b 100644
--- a/HexPolyMathlib/Basic.lean
+++ b/HexPolyMathlib/Basic.lean
@@ -527,13 +527,7 @@ theorem leadingCoeff_toPolynomial [Semiring R] [DecidableEq R]
       simp [Hex.DensePoly.degree?, hsize]
     rw [hdegree_some, Option.getD_some]
     show p.coeff (p.size - 1) = p.leadingCoeff
-    unfold Hex.DensePoly.coeff Hex.DensePoly.leadingCoeff
-    have hidx : p.coeffs.size - 1 < p.coeffs.size := by
-      have hs : p.size = p.coeffs.size := rfl
-      omega
-    rw [Array.back?_eq_getElem?, Array.getElem?_eq_getElem hidx, Option.getD_some,
-      show p.size = p.coeffs.size from rfl]
-    exact (Array.getElem_eq_getD (Zero.zero : R)).symm
+    simp [Hex.DensePoly.leadingCoeff, Hex.DensePoly.coeff, Hex.DensePoly.size]
 
 /-- `toPolynomial` preserves divisibility: a divisibility in the executable
 representation transfers to the corresponding Mathlib polynomials. -/
diff --git a/HexPolyZ/Basic.lean b/HexPolyZ/Basic.lean
index 03370fc22..b4bea4119 100644
--- a/HexPolyZ/Basic.lean
+++ b/HexPolyZ/Basic.lean
@@ -73,6 +73,7 @@ def content (f : ZPoly) : Int :=
   DensePoly.content f
 
 /-- Divide every coefficient by the content to obtain a primitive polynomial. -/
+@[expose]
 def primitivePart (f : ZPoly) : ZPoly :=
   DensePoly.primitivePart f
 
@@ -85,6 +86,7 @@ monic factor `g` of the transform to `g(c · X)`, an integer multiple of the
 corresponding factor of `core`. Composing with `primitivePart` recovers the
 primitive integer factor of `core`. This is *not* the same as `DensePoly.scale`,
 which multiplies the whole polynomial by a constant. -/
+@[expose]
 def dilate (c : Int) (p : ZPoly) : ZPoly :=
   DensePoly.ofCoeffs <| ((List.range p.size).map fun i => c ^ i * p.coeff i).toArray
 
@@ -601,6 +603,7 @@ structure PrimitiveSquareFreeDecomposition where
   repeatedPart : ZPoly
 
 /-- Square-free over `Rat[x]`, up to the executable rational gcd's unit factor. -/
+@[expose]
 def SquareFreeRat (f : ZPoly) : Prop :=
   (DensePoly.gcd (toRatPoly f) (DensePoly.derivative (toRatPoly f))).size ≤ 1
 
@@ -608,6 +611,7 @@ def SquareFreeRat (f : ZPoly) : Prop :=
 Compute the primitive square-free normalization data needed by the integer
 factorization pipeline.
 -/
+@[expose]
 def primitiveSquareFreeDecomposition (f : ZPoly) : PrimitiveSquareFreeDecomposition :=
   let primitive := primitivePart f
   if primitive.isZero then
@@ -1986,11 +1990,7 @@ private theorem rat_leadingCoeff_ne_zero_of_pos_size (p : DensePoly Rat) (hpos :
   have hidx : p.coeffs.size - 1 < p.coeffs.size := by
     simpa [DensePoly.size] using Nat.sub_one_lt_of_lt hpos
   have hlead_eq : p.leadingCoeff = p.coeff (p.size - 1) := by
-    unfold DensePoly.leadingCoeff DensePoly.coeff
-    change p.coeffs.back?.getD (0 : Rat) =
-      p.coeffs.getD (p.coeffs.size - 1) (Zero.zero : Rat)
-    rw [Array.back?_eq_getElem?, Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hidx]
-    rfl
+    simp [DensePoly.leadingCoeff, DensePoly.coeff, DensePoly.size]
   rw [hlead_eq]
   exact DensePoly.coeff_last_ne_zero_of_pos_size p hpos
 
@@ -2716,7 +2716,7 @@ private instance ratDivModLaws : DensePoly.DivModLaws Rat where
       have hq' : q % m = q + m * rq := rat_eq_add_mul_of_sub_eq_mul hq
       exact rat_mul_left_remainder_delta p q m rp rq hp' hq'⟩
 
-private instance ratGcdLaws : DensePoly.GcdLaws Rat where
+instance ratGcdLaws : DensePoly.GcdLaws Rat where
   gcd_dvd_left := by
     intro f g
     exact DensePoly.gcd_dvd_left_of_divModLaws
diff --git a/progress/20260704T000000Z_bz-module-migration-phase1a.md b/progress/20260704T000000Z_bz-module-migration-phase1a.md
new file mode 100644
index 000000000..1718987eb
--- /dev/null
+++ b/progress/20260704T000000Z_bz-module-migration-phase1a.md
@@ -0,0 +1,55 @@
+# BZ module-system migration — Phase 1a (executable library)
+
+## Accomplished
+Migrated the executable `HexBerlekampZassenhaus` library onto the Lean 4
+module system (`module` / `public import` / `public section`), as the
+prerequisite step before splitting the 19k-line `Basic.lean` monolith.
+Whole project builds green (`lake build`, 4088 jobs); `check_dag.py`
+passes; no new `sorry`/`axiom`.
+
+The migration surfaced **two genuine lean4 module-system reduction bugs**,
+both diagnosed to root and worked around locally:
+
+1. **`Array.instDecidableEqImpl` is not `@[expose]`**, so `decide`/`rfl`
+   over `Array` equality does not reduce in the kernel under `module` for
+   two nonempty arrays (`instDecidableEq` inlines the empty cases but
+   delegates the nonempty case to the opaque impl). Repro + analysis in
+   [progress/lean4-array-decidableeq-module-repro.md](lean4-array-decidableeq-module-repro.md).
+   - Draft lean4 PR: https://github.com/leanprover/lean4/pull/14270
+     (adds `@[expose]`, with a `tests/elab/` regression test).
+   - In-tree workaround: `import all Init.Data.Array.DecidableEq` in
+     `HexBerlekampZassenhaus/Basic.lean`. The efficient `Array` DecidableEq
+     is retained (no switch to a slower `List`-based instance).
+2. **`Array.back?` does not reduce under `module`** — reimplemented
+   `HexPoly.Euclid.leadingCoeff` as `coeffs.getD (size - 1) 0` instead of
+   `coeffs.back?.getD 0` (equal, kernel-reducible, no `Option` alloc).
+   Both workarounds carry `-- revert once upstream lands` comments.
+
+Other mechanics: `public meta import`s for the 117 `#guard`s;
+`backward.{proofsInPublic,privateInPublic}` for private-in-public;
+`@[expose]` on the executable defs that exported `decide`/`rfl`/`unfold`
+proofs reduce through (incl. the shallow `factor 0` constant-branch
+closure); de-privatised the leaked `GcdLaws Rat` instance; exposed
+`SquareFreeRat`. The `leadingCoeff` reimplementation rippled into ~12
+`leadingCoeff = coeff (size-1)` re-proofs across HexPoly/HexHensel/
+HexBerlekamp/HexPolyFp/HexPolyZ/HexPolyMathlib/HexBZMathlib — all fixed to
+`simp [leadingCoeff, coeff, size]` form.
+
+**No runtime performance regression:** the only change to compiled code is
+`leadingCoeff` (equal-or-faster); DecidableEq is unchanged (original
+efficient instance kept); everything else is compile/elaboration-time.
+
+## Current frontier
+Phase 1a green and committable. `HexBerlekampZassenhausMathlib` is still
+legacy (only its two `leadingCoeff`-consuming proofs were touched, forced
+by the def change).
+
+## Next step
+- Phase 1b: migrate `HexBerlekampZassenhausMathlib` (22k, CI-gated) to the
+  module system — expect a larger `@[expose]`/private-in-public pass.
+- Phase 2: split both `Basic.lean` monoliths into dependency-ordered
+  leaves and delete `Basic.lean` (repoint importers to the umbrella).
+
+## Blockers
+None. Upstream lean4 PR #14270 pending; the `import all` and `getD`
+workarounds keep us green in the meantime.
diff --git a/progress/lean4-array-decidableeq-module-repro.md b/progress/lean4-array-decidableeq-module-repro.md
new file mode 100644
index 000000000..a84cee6d2
--- /dev/null
+++ b/progress/lean4-array-decidableeq-module-repro.md
@@ -0,0 +1,71 @@
+# lean4 bug: `Array.instDecidableEq` does not reduce under the module system (nonempty arrays)
+
+Toolchain: `leanprover/lean4:v4.32.0-rc1` (also present on nightlies through 2026-07-03).
+
+## Minimal repro
+
+```lean
+module
+example : (#[0, 1] : Array Nat) ≠ #[1] := by decide
+```
+
+fails:
+
+```
+error: Tactic `decide` failed for proposition
+  #[0, 1] ≠ #[1]
+because its `Decidable` instance `instDecidableNot` did not reduce to `isTrue` or `isFalse`.
+After unfolding the instances `instDecidableNot` and `Array.instDecidableEq`, reduction got
+stuck at the `Decidable` instance
+  { toList := [0, 1] }.instDecidableEqImpl { toList := [1] }
+```
+
+The identical statement **without** `module` succeeds. `decide` also succeeds under
+`module` whenever at least one array is empty (`#[] = #[]`, `#[] = #[1]`, `#[0,1] = #[]`),
+and for `List` (`[0,1] ≠ [1]`).
+
+## Root cause
+
+In `Init/Data/Array/DecidableEq.lean`:
+
+```lean
+def instDecidableEqImpl [DecidableEq α] : DecidableEq (Array α) := fun xs ys =>
+  match h : isEqv xs ys (fun a b => a = b) with
+  | true  => isTrue (eq_of_isEqv xs ys h)
+  | false => isFalse (by subst ·; rw [isEqv_self] at h; contradiction)
+
+instance instDecidableEq [DecidableEq α] : DecidableEq (Array α) := fun xs ys =>
+  match xs with
+  | ⟨[]⟩ => match ys with | ⟨[]⟩ => isTrue rfl | ⟨_ :: _⟩ => isFalse …
+  | ⟨a :: as⟩ => match ys with
+    | ⟨[]⟩ => isFalse …
+    | ⟨b :: bs⟩ => instDecidableEqImpl ⟨a :: as⟩ ⟨b :: bs⟩   -- delegates to the impl
+```
+
+`instDecidableEq` is exposed (`@[implicit_reducible, expose]`) and its empty/empty and
+empty/nonempty cases are inlined, so they reduce. The nonempty/nonempty case delegates to
+`instDecidableEqImpl`, which is a **plain `def` with no `@[expose]`**. Under the module
+system a public non-`@[expose]` `def` exports only its signature, so `instDecidableEqImpl`'s
+body is unavailable to the kernel downstream — `#print Array.instDecidableEqImpl` reports
+`<not imported>` — and reduction stalls for every pair of nonempty arrays.
+
+## Proposed fix
+
+Add `@[expose]` to `Array.instDecidableEqImpl` (and verify its reduction closure,
+`Array.isEqv` / `Array.isEqvAux`, is likewise exposed). That restores kernel reduction of
+`decide`/`rfl` over `Array` equality under `module`.
+
+## Consumer-side workarounds (no toolchain change)
+
+- `import all Init.Data.Array.DecidableEq` in the module performing the `decide` — pulls the
+  impl body in and reduces (verified).
+- Route a wrapper type's `DecidableEq` through `List` instead of `Array`, e.g.
+  `decidable_of_iff (a.toList = b.toList) …`; `List.instDecidableEq` is fully exposed.
+  (This is what `HexPoly.Dense`'s `DecidableEq (DensePoly R)` now does.)
+
+## Related
+
+The sibling `Array.back?` non-reduction under `module` (worked around in
+`HexPoly.Euclid.leadingCoeff` by using `coeffs.getD (size - 1)` instead of
+`coeffs.back?.getD 0`) is the same class of issue: a core `Array` helper whose body is not
+available to the kernel downstream under the module system.

From 9b33ffe2211330dc2fa2ce0f5cf78b6d75e8b253 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 4 Jul 2026 12:30:52 +0000
Subject: [PATCH 2/2] fix(bench): repair leadingCoeff Monic proofs in
 bench/conformance drivers

The DensePoly.leadingCoeff reimplementation (coeffs.getD (size-1) 0 instead
of coeffs.back?.getD 0) broke the monic-witness proofs in the bench exe and
emit-fixture drivers, which the module-migration commit missed because a
plain `lake build` does not build the bench/conformance sub-projects (CI
does). Rewrite the `change ...back?.getD 0 = 1` proofs to close the
getD form via Array.getElem_push.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---
 bench/HexBerlekamp/Bench.lean              | 4 +---
 bench/HexPoly/Bench.lean                   | 2 +-
 bench/HexPolyFp/Bench.lean                 | 9 ++++-----
 conformance/HexBerlekamp/EmitFixtures.lean | 6 +-----
 conformance/HexPolyFp/EmitFixtures.lean    | 3 +--
 5 files changed, 8 insertions(+), 16 deletions(-)

diff --git a/bench/HexBerlekamp/Bench.lean b/bench/HexBerlekamp/Bench.lean
index b159b3b49..201901c0d 100644
--- a/bench/HexBerlekamp/Bench.lean
+++ b/bench/HexBerlekamp/Bench.lean
@@ -95,9 +95,7 @@ def monicPoly (degree salt : Nat) : FpPoly 5 :=
 /-- Generated monic polynomials have leading coefficient one. -/
 theorem monicPoly_monic (degree salt : Nat) : DensePoly.Monic (monicPoly degree salt) := by
   unfold monicPoly DensePoly.Monic DensePoly.leadingCoeff
-  change (((Array.range degree).map fun i => coeffValue degree i salt).push
-    (1 : ZMod64 5)).back?.getD 0 = 1
-  simp
+  simp [Array.getElem_push] <;> rfl
 
 /-- Stable checksum for polynomial-valued benchmark results. -/
 def checksumPoly (f : FpPoly 5) : UInt64 :=
diff --git a/bench/HexPoly/Bench.lean b/bench/HexPoly/Bench.lean
index c66c10649..2417bb59c 100644
--- a/bench/HexPoly/Bench.lean
+++ b/bench/HexPoly/Bench.lean
@@ -199,7 +199,7 @@ def monicDivisor (degree : Nat) : DensePoly F7 :=
 
 /-- Generated monomial divisors are monic by construction. -/
 theorem monicDivisor_monic (degree : Nat) : DensePoly.Monic (monicDivisor degree) := by
-  simp [monicDivisor, DensePoly.Monic, DensePoly.leadingCoeff]
+  simp [monicDivisor, DensePoly.Monic, DensePoly.leadingCoeff, Array.getElem_push] <;> rfl
 
 /-- Stable bounded observable for polynomial-valued benchmark results. -/
 def checksum [Hashable R] [Zero R] [DecidableEq R] (p : DensePoly R) : UInt64 :=
diff --git a/bench/HexPolyFp/Bench.lean b/bench/HexPolyFp/Bench.lean
index 2e0eb5ec7..082d683e0 100644
--- a/bench/HexPolyFp/Bench.lean
+++ b/bench/HexPolyFp/Bench.lean
@@ -141,8 +141,9 @@ theorem monicModulusFive_monic (degree : Nat) : DensePoly.Monic (monicModulusFiv
   unfold monicModulusFive DensePoly.Monic DensePoly.leadingCoeff DensePoly.monomial
   by_cases h : (1 : ZMod64 5) = 0
   · exact False.elim (one_ne_zero_five h)
-  · change ((Array.replicate degree (0 : ZMod64 5)).push 1).back?.getD 0 = 1
-    simp
+  · have h' : ¬ ((1 : ZMod64 5) = Zero.zero) := h
+    simp only [dif_neg h']
+    simp [Array.getElem_push] <;> rfl
 
 /-- Deterministic monic modulus of degree `degree` over the large benchmark prime. -/
 def monicModulusLarge (degree : Nat) : FpPoly 65537 :=
@@ -161,9 +162,7 @@ def monicModulusLarge (degree : Nat) : FpPoly 65537 :=
 theorem monicModulusLarge_monic (degree : Nat) :
     DensePoly.Monic (monicModulusLarge degree) := by
   unfold monicModulusLarge DensePoly.Monic DensePoly.leadingCoeff
-  change (((Array.range degree).map fun i => coeffValueLarge degree i 503).push
-    (1 : ZMod64 65537)).back?.getD 0 = 1
-  simp
+  simp [Array.getElem_push] <;> rfl
 
 /-- Deterministic linear square-free factor. -/
 def linearFactor (i : Nat) : FpPoly 5 :=
diff --git a/conformance/HexBerlekamp/EmitFixtures.lean b/conformance/HexBerlekamp/EmitFixtures.lean
index 748314d56..4496b0e59 100644
--- a/conformance/HexBerlekamp/EmitFixtures.lean
+++ b/conformance/HexBerlekamp/EmitFixtures.lean
@@ -249,11 +249,7 @@ private def mkMonicAux {p : Nat} [ZMod64.Bounds p]
         exact h1ne0 (Option.some.inj hback) }
   ⟨f, by
     show f.leadingCoeff = 1
-    show f.coeffs.back?.getD 0 = 1
-    have hlast : f.coeffs.back? = some 1 := by
-      simp [f, coeffs]
-    rw [hlast]
-    rfl⟩
+    simp [DensePoly.leadingCoeff, f, coeffs, Array.getElem_push] <;> rfl⟩
 
 /-- Wrap a list of `Nat` coefficients as a monic `FpPoly p`. -/
 private def mkMonic {p : Nat} [ZMod64.Bounds p]
diff --git a/conformance/HexPolyFp/EmitFixtures.lean b/conformance/HexPolyFp/EmitFixtures.lean
index f5ee76852..d4ef9383c 100644
--- a/conformance/HexPolyFp/EmitFixtures.lean
+++ b/conformance/HexPolyFp/EmitFixtures.lean
@@ -113,8 +113,7 @@ private theorem randomMonicPoly_monic
     (p : Nat) [ZMod64.Bounds p] (h : 2 ≤ p) (seed deg : Nat) :
     DensePoly.Monic (randomMonicPoly p h seed deg) := by
   unfold DensePoly.Monic DensePoly.leadingCoeff randomMonicPoly
-  simp [monicArray_back?]
-  rfl
+  simp [monicArray, Array.getElem_push] <;> rfl
 
 /-! ## Coefficient ↔ Int conversion -/