perf: adopt modules and reduce Lean Pool build cost

LeanPool.lean

@@ -6237,6 +6237,7 @@ import LeanPool.Sensitivity
 import LeanPool.Sensitivity.Basic
 import LeanPool.Sensitivity.Consequences
 import LeanPool.Sensitivity.Defs
+import LeanPool.Sensitivity.Huang
 import LeanPool.Sensitivity.HuangBridge
 import LeanPool.Sensitivity.Main
 import LeanPool.Sensitivity.Multilinear
@@ -6250,6 +6251,8 @@ import LeanPool.SetTheory.Omega
 import LeanPool.SetTheory.OrderTheory
 import LeanPool.SetTheory.Ordinals
 import LeanPool.SetTheory.Realize
+import LeanPool.SetTheory.RealizeBuilders
+import LeanPool.SetTheory.RealizeCore
 import LeanPool.SetTheory.SimpAttr
 import LeanPool.Shannon1948Formalization
 import LeanPool.Shannon1948Formalization.Entropy

LeanPool/ABCExceptions.lean

@@ -3,10 +3,14 @@ Copyright (c) 2026 Bhavik Mehta, Arend Mellendijk. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Arend Mellendijk
 -/
+module
 
-import LeanPool.ABCExceptions.ForMathlib
-import LeanPool.ABCExceptions.Section2
-import LeanPool.ABCExceptions.Section4
+public import LeanPool.ABCExceptions.ForMathlib
+public import LeanPool.ABCExceptions.Section2
+public import LeanPool.ABCExceptions.Section4
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
+import Mathlib.RingTheory.Radical.NatInt
 
 /-!
 # Exceptional Set in the abc Conjecture
@@ -19,6 +23,8 @@ Tags: number-theory, analytic-number-theory, abc-conjecture
 MSC: 11D75, 11N37
 -/
 
+@[expose] public section
+
 /-!
 ## Mathematical overview
 

LeanPool/ABCExceptions/ForMathlib.lean

@@ -3,13 +3,17 @@ Copyright (c) 2026 Bhavik Mehta, Arend Mellendijk. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Arend Mellendijk
 -/
+module
 
-import LeanPool.ABCExceptions.ForMathlib.Misc
-import LeanPool.ABCExceptions.ForMathlib.RingTheory
+public import LeanPool.ABCExceptions.ForMathlib.Misc
+public import LeanPool.ABCExceptions.ForMathlib.RingTheory
+import Mathlib.RingTheory.Radical.NatInt
 
 /-!
 # Support lemmas for ABC exceptions
 
 Import-only index for Mathlib-adjacent support files used by the ABC exceptions
 development.
 -/
+
+@[expose] public section

LeanPool/ABCExceptions/ForMathlib/Misc.lean

@@ -3,18 +3,23 @@ Copyright (c) 2026 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
+module
 
+public import Mathlib.Order.Interval.Finset.Nat
+public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
+public import Mathlib.Algebra.Order.SuccPred
 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
-import Mathlib.Algebra.Order.Ring.Nat
-import Mathlib.Order.Interval.Finset.Nat
 import Mathlib.Algebra.Order.Interval.Finset.SuccPred
-import Mathlib.Data.Nat.SuccPred
+import Mathlib.Algebra.Order.Ring.Nat
 import Mathlib.Data.Finset.Powerset
+import Mathlib.Data.Nat.SuccPred
 
 /-!
 # LeanPool.ABCExceptions.ForMathlib.Misc
 -/
 
+@[expose] public section
+
 noncomputable section
 
 open Set

LeanPool/ABCExceptions/ForMathlib/RingTheory.lean

@@ -3,12 +3,16 @@ Copyright (c) 2026 Bhavik Mehta, Arend Mellendijk. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Arend Mellendijk
 -/
+module
 
-import LeanPool.ABCExceptions.ForMathlib.RingTheory.Radical
+public import LeanPool.ABCExceptions.ForMathlib.RingTheory.Radical
+import Mathlib.RingTheory.Radical.NatInt
 
 /-!
 # Ring theory support for ABC exceptions
 
 Import-only index for ring-theoretic support files used by the ABC exceptions
 development.
 -/
+
+@[expose] public section

LeanPool/ABCExceptions/ForMathlib/RingTheory/Radical.lean

@@ -3,18 +3,20 @@ Copyright (c) 2026 Bhavik Mehta, Arend Mellendijk. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Arend Mellendijk
 -/
+module
 
-import Mathlib.Algebra.GCDMonoid.Nat
-import Mathlib.Algebra.Squarefree.Basic
-import Mathlib.Data.Nat.PrimeFin
-import Mathlib.RingTheory.Coprime.Lemmas
+public import Mathlib.RingTheory.Radical.Basic
+
+public meta import Aesop.BuiltinRules
+public import Mathlib.Tactic.Positivity.Core
 import Mathlib.RingTheory.Radical.NatInt
-import Mathlib.RingTheory.UniqueFactorizationDomain.Nat
 
 /-!
 # LeanPool.ABCExceptions.ForMathlib.RingTheory.Radical
 -/
 
+@[expose] public section
+
 namespace UniqueFactorizationMonoid
 
 open Qq Lean Mathlib.Meta Finset
@@ -25,7 +27,7 @@ open Positivity
 attribute [local instance] monadLiftOptionMetaM in
 /-- Positivity extension for radical. Proves radicals are nonzero. -/
 @[positivity UniqueFactorizationMonoid.radical _]
-def evalRadical : PositivityExt where eval {u α} _ _ e := do
+meta def evalRadical : PositivityExt where eval {u α} _ _ e := do
   match e with
   | ~q(@radical _ $inst $inst' $inst'' $n) =>
     have _ := ← synthInstanceQ q(Nontrivial $α)

LeanPool/ABCExceptions/Section2.lean

@@ -3,21 +3,26 @@ Copyright (c) 2026 Bhavik Mehta, Arend Mellendijk. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Arend Mellendijk
 -/
+module
 
-import Mathlib.Analysis.SpecialFunctions.Log.Base
-import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
-import Mathlib.Algebra.Order.Floor.Semifield
-import Mathlib.Data.Nat.GCD.BigOperators
-import Mathlib.Data.Nat.Squarefree
-import Mathlib.Algebra.Order.Star.Real
-import Mathlib.Order.CompletePartialOrder
+public import Mathlib.Analysis.SpecialFunctions.Log.Base
+public import Mathlib.Order.CompletePartialOrder
 
+public import Mathlib.RingTheory.Radical.Basic
+public import Mathlib.RingTheory.UniqueFactorizationDomain.Nat
 import LeanPool.ABCExceptions.ForMathlib.RingTheory.Radical
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Algebra.Order.Star.Real
+import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
+import Mathlib.Data.Nat.GCD.BigOperators
+import Mathlib.RingTheory.Radical.NatInt
 
 /-!
 # LeanPool.ABCExceptions.Section2
 -/
 
+@[expose] public section
+
 open Finset UniqueFactorizationMonoid
 
 section
@@ -52,9 +57,8 @@ theorem Finset.mem_abcExceptionsBelow (ε : ℝ) (X : ℕ) (a b c : ℕ) :
 @[gcongr]
 lemma Finset.abcExceptionsBelow_mono_right {ε : ℝ} {X Y : ℕ} (hXY : X ≤ Y) :
     abcExceptionsBelow ε X ⊆ abcExceptionsBelow ε Y := by
-  rintro ⟨a, b, c⟩
-  simp +contextual
-  omega
+  exact Finset.filter_subset_filter _
+    (Finset.Icc_subset_Icc le_rfl ⟨hXY, hXY, hXY⟩)
 
 @[gcongr]
 lemma Finset.abcExceptionsBelow_mono_left {ε₁ ε₂ : ℝ} {X : ℕ} (hε : ε₁ ≤ ε₂) :
@@ -344,7 +348,7 @@ This is $$S^*_{α,β,γ}(X)$$ in the paper and blueprint.
 noncomputable def refinedCountTriplesStar (α β γ : ℝ) (X : ℕ) : ℕ := #(dyadicPoints α β γ X)
 
 /-- The set over which we take the supremum in lemma 2.2. -/
-private noncomputable def indexSet (ε : ℝ) (X : ℕ) : Finset (ℕ × ℕ × ℕ × ℕ) :=
+noncomputable def indexSet (ε : ℝ) (X : ℕ) : Finset (ℕ × ℕ × ℕ × ℕ) :=
   (Finset.Icc 0 (Nat.log 2 X)) ×ˢ (Finset.Icc 0 (Nat.log 2 X)) ×ˢ
   (Finset.Icc 0 (Nat.log 2 X)) ×ˢ (Finset.Icc 1 (Nat.log 2 X+1)) |>.filter fun ⟨i, j, k, n⟩ ↦
     i + j + k ≤ (1 - ε) * n
@@ -711,7 +715,7 @@ private theorem hd_pos : 0 < d := by
   rw [hd, Nat.floor_pos]
   nlinarith only [two_lt_eps_inv]
 
-private instance hd_ne_zero : NeZero d := by
+instance hd_ne_zero : NeZero d := by
   simp_rw [neZero_iff]
   apply ne_of_gt hd_pos
 
@@ -907,7 +911,8 @@ private theorem c_le_X_pow : c ≤ (X : ℝ) ^ ε := calc
     · norm_cast
       linarith
 
-private noncomputable def KIndex : Fin d := Fin.ofNat d (K - 1)
+/-- The distinguished index `K - 1`, viewed in `Fin d`. -/
+noncomputable def KIndex : Fin d := Fin.ofNat d (K - 1)
 
 @[simp]
 private theorem KIndex_val_add_one : KIndex.val + 1 = K := by
@@ -1177,12 +1182,12 @@ theorem exists_nice_factorization'
     · exact c_le_pow
     gcongr
     · norm_cast
-    · linarith [sq_nonneg ε]
+    · linarith only [sq_nonneg ε]
   · rw [Nat.le_floor_iff]
     · apply c_le_pow.trans
       gcongr _ ^ ?_
       · norm_cast
-      · nlinarith
+      · nlinarith only [hε, hε_pos]
     positivity
   · rw [sub_eq_add_neg, Real.rpow_add, Real.rpow_neg, mul_inv_le_iff₀]
     · apply hsim.1.trans (rad_n_le.trans _)
@@ -1359,7 +1364,7 @@ theorem B_to_triple_surjOn {α β γ : ℝ} (x : ℕ) (ε : ℝ)
           · simp only [Real.rpow_one]
             trans 2 * (c₂ *(∏ i, (w i : ℝ) ^ (i.val + 1)))
             · norm_cast
-              simp_all
+              rwa [← c_eq_c_mul_prod]
             · rw [← mul_assoc, mul_comm 2, mul_assoc]
               gcongr
           · apply Real.rpow_pos_of_pos
@@ -1405,7 +1410,7 @@ theorem B_to_triple_surjOn {α β γ : ℝ} (x : ℕ) (ε : ℝ)
     · apply fun i ↦ (similar_pow_log (hu_pos i))
     · apply fun i ↦ (similar_pow_log (hv_pos i))
     · apply fun i ↦ (similar_pow_log (hw_pos i))
-    · simp_all
+    · rwa [← a_eq_c_mul_prod, ← b_eq_c_mul_prod, ← c_eq_c_mul_prod]
     · apply coprime_mul_prod_aux _ _ (a_eq_c_mul_prod ▸ b_eq_c_mul_prod ▸ hab) <;> omega
     · apply coprime_mul_prod_aux _ _ (a_eq_c_mul_prod ▸ c_eq_c_mul_prod ▸ hac) <;> omega
     · apply coprime_mul_prod_aux _ _ (b_eq_c_mul_prod ▸ c_eq_c_mul_prod ▸ hbc) <;> omega

LeanPool/ABCExceptions/Section4.lean

@@ -3,11 +3,20 @@ Copyright (c) 2026 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
+module
 
-import Mathlib.Analysis.RCLike.Basic
+public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
+public import Mathlib.Algebra.Order.Archimedean.Real.Basic
+public import Mathlib.Order.Interval.Finset.Nat
+meta import Lean.Meta.Tactic.NormCast
+import LeanPool.ABCExceptions.ForMathlib.Misc
+import Mathlib.Algebra.BigOperators.Fin
+import Mathlib.Algebra.CharP.Defs
+import Mathlib.Algebra.Order.BigOperators.Expect
 import Mathlib.Algebra.Order.Star.Real
+import Mathlib.Analysis.Normed.Group.Basic
+import Mathlib.Tactic.LinearCombination
 import Mathlib.Tactic.NormNum.BigOperators
-import LeanPool.ABCExceptions.ForMathlib.Misc
 
 /-!
 # Section 4
@@ -18,6 +27,8 @@ parts of the paper.
 
 -/
 
+@[expose] public section
+
 noncomputable section
 
 open Finset
@@ -1010,7 +1021,7 @@ lemma bound_4_point_24 (hd : 6 ≤ d) (hba : b 3 ≤ a 3) :
       have h4 : 0 ≤ min (a 4) (b 4) := le_min (ha.nonneg _) (hb.nonneg _)
       have h5 : 0 ≤ min (a 5) (b 5) := le_min (ha.nonneg _) (hb.nonneg _)
       have h6 : 0 ≤ min (a 6) (b 6) := le_min (ha.nonneg _) (hb.nonneg _)
-      norm_num [- min_add_max, ha.zero, hb.zero, hba]
+      simp [-min_add_max, ha.zero, hb.zero, hba]
       linear_combination 2 * h4 + 3 * h5 + 4 * h6
 
 include ha hb h44 htab hg in
@@ -1118,7 +1129,8 @@ lemma GeometryBound.s21_application_basic
   have h₁₂₃ : {1, 2, 3} ⊆ Finset.Icc 1 d := by simp [Finset.insert_subset_iff]; omega
   have h₁₂₄ : {1, 2, 4} ⊆ Finset.Icc 1 d := by simp [Finset.insert_subset_iff]; omega
   have h₁₂₃₄ : {1, 2, 3, 4} ⊆ Finset.Icc 1 d := by simp [Finset.insert_subset_iff]; omega
-  have : ν < ε + a 3 + b 3 + c 4 + ∑ i ∈ Icc 5 d, (b i + c i) + 0 ⊔ (∑ x ∈ Icc 1 d, x * a x +
+  have hbounds :
+      ν < ε + a 3 + b 3 + c 4 + ∑ i ∈ Icc 5 d, (b i + c i) + 0 ⊔ (∑ x ∈ Icc 1 d, x * a x +
           (b 1 + c 1) + 2 * (b 2 + c 2) - 3 * (a 3 - c 3) + (4 * b 4) - 1) ∧
          ν < ε + a 3 + b 3 + b 4 + ∑ i ∈ Icc 5 d, (b i + c i) + 0 ⊔ (∑ x ∈ Icc 1 d, x * a x +
           (b 1 + c 1) + 2 * (b 2 + c 2) - 3 * (a 3 - c 3) + (4 * c 4) - 1) := by
@@ -1136,10 +1148,10 @@ lemma GeometryBound.s21_application_basic
     simp only [Finset.sum_add_distrib]
     simp [sum_range, Fin.sum_univ_five, hb.zero, hc.zero] at h₁ h₂
     ring_nf at h₁ h₂ ⊢
-    simp_all
+    exact ⟨h₁, h₂⟩
   obtain h4 | h4 := le_total (b 4) (c 4)
-  · simp_all
-  · simp_all
+  · simpa only [min_eq_left h4, max_eq_right h4] using hbounds.2
+  · simpa only [min_eq_right h4, max_eq_left h4] using hbounds.1
 
 lemma min_le_half_add {x y : ℝ} : min x y ≤ (x + y) / 2 := by
   linarith [min_le_left x y, min_le_right x y]

LeanPool/AFormalizationOfBorelDeterminacyInLean.lean

@@ -3,9 +3,13 @@ Copyright (c) 2026 Sven Manthe. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sven Manthe
 -/
+module
 
-import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications
-import LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Undetermined
+public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.BorelDeterminacy
+
+public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications
+public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Undetermined
+import Mathlib.CategoryTheory.Category.Init
 
 /-!
 # A formalization of Borel determinacy in Lean
@@ -18,6 +22,8 @@ Tags: descriptive-set-theory, game-theory, determinacy
 MSC: 03E15, 54H05, 91A44
 -/
 
+@[expose] public section
+
 /-!
 ## Mathematical overview
 

LeanPool/AFormalizationOfBorelDeterminacyInLean/Applications.lean

@@ -3,15 +3,19 @@ Copyright (c) 2026 Sven Manthe. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sven Manthe
 -/
+module
 
-import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.Choquet
-import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.General
-import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.Meager
-import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.RegularOpen
+public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.Choquet
+public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.General
+public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.Meager
+public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.RegularOpen
+import Mathlib.CategoryTheory.Category.Init
 
 /-!
 # Applications index
 
 Import-only index for the application modules in the Borel determinacy
 formalization.
 -/
+
+@[expose] public section

LeanPool/AFormalizationOfBorelDeterminacyInLean/Applications/Choquet.lean

@@ -3,16 +3,25 @@ Copyright (c) 2026 Sven Manthe. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sven Manthe
 -/
+module
 
-import LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.Meager
-import LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.BorelDeterminacy
+public import LeanPool.AFormalizationOfBorelDeterminacyInLean.Game.Games
+import LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.Meta
+import Mathlib.Algebra.Order.Module.Field
+import Mathlib.CategoryTheory.Category.Init
+import Mathlib.Data.EReal.Inv
+import Mathlib.Tactic.Measurability.Init
+import Mathlib.Topology.Algebra.InfiniteSum.Order
+import Mathlib.Topology.MetricSpace.Bounded
 
 /-!
 # LeanPool.AFormalizationOfBorelDeterminacyInLean.Applications.Choquet
 
 Auxiliary declarations for the Borel determinacy formalization.
 -/
 
+@[expose] public section
+
 
 open GaleStewartGame
 open Descriptive