Axiomatic-AI · winstonyin-ax · Jul 30, 2026 · Jul 29, 2026 · Jul 29, 2026 · Jul 29, 2026
diff --git a/Archive/Imo/Imo2008Q3.lean b/Archive/Imo/Imo2008Q3.lean
@@ -34,7 +34,7 @@ namespace Imo2008Q3
 
 theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4]) (hp_gt_20 : p > 20) :
     ∃ n : ℕ, p ∣ n ^ 2 + 1 ∧ (p : ℝ) > 2 * n + sqrt (2 * n) := by
-  haveI := Fact.mk hpp
+  have := Fact.mk hpp
   have hp_mod_4_ne_3 : p % 4 ≠ 3 := by linarith [show p % 4 = 1 from hp_mod_4_eq_1]
   obtain ⟨y, hy⟩ := ZMod.exists_sq_eq_neg_one_iff.mpr hp_mod_4_ne_3
   let m := ZMod.valMinAbs y

diff --git a/Archive/Imo/Imo2019Q2.lean b/Archive/Imo/Imo2019Q2.lean
@@ -275,7 +275,7 @@ theorem A₁_ne_B : cfg.A₁ ≠ cfg.B := by
     rw [AffineSubspace.eq_iff_direction_eq_of_mem (left_mem_affineSpan_pair _ _ _)
       hwbtw.mem_affineSpan]
     exact cfg.PQ_parallel_AB.direction_eq
-  haveI := someOrientation V
+  have := someOrientation V
   have haQ : (2 : ℤ) • ∡ cfg.C cfg.B cfg.Q = (2 : ℤ) • ∡ cfg.C cfg.B cfg.A := by
     rw [Collinear.two_zsmul_oangle_eq_right _ cfg.A_ne_B cfg.Q_ne_B]
     rw [Set.pair_comm, Set.insert_comm]
@@ -389,7 +389,7 @@ end Oriented
 
 
 theorem not_collinear_QPA₂ : ¬Collinear ℝ ({cfg.Q, cfg.P, cfg.A₂} : Set Pt) := by
-  haveI := someOrientation V
+  have := someOrientation V
   rw [collinear_iff_of_two_zsmul_oangle_eq cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂, ←
     affineIndependent_iff_not_collinear_set]
   have h : Cospherical ({cfg.B, cfg.A, cfg.A₂} : Set Pt) := by
@@ -515,13 +515,13 @@ end Oriented
 
 
 theorem not_collinear_CA₂A₁ : ¬Collinear ℝ ({cfg.C, cfg.A₂, cfg.A₁} : Set Pt) := by
-  haveI := someOrientation V
+  have := someOrientation V
   rw [collinear_iff_of_two_zsmul_oangle_eq cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA,
     Set.pair_comm, Set.insert_comm, Set.pair_comm]
   exact cfg.not_collinear_ABC
 
 theorem cospherical_A₁Q₁CA₂ : Cospherical ({cfg.A₁, cfg.Q₁, cfg.C, cfg.A₂} : Set Pt) := by
-  haveI := someOrientation V
+  have := someOrientation V
   rw [Set.insert_comm cfg.Q₁, Set.insert_comm cfg.A₁, Set.pair_comm, Set.insert_comm cfg.A₁,
     Set.pair_comm]
   exact cospherical_of_two_zsmul_oangle_eq_of_not_collinear

diff --git a/Archive/Wiedijk100Theorems/BallotProblem.lean b/Archive/Wiedijk100Theorems/BallotProblem.lean
@@ -315,9 +315,9 @@ theorem ballot_problem' :
     rw [div_self]
     exact Nat.cast_add_one_ne_zero p
   · intro q p qp h₁ h₂
-    haveI := isProbabilityMeasure_uniformOn
+    have := isProbabilityMeasure_uniformOn
       (countedSequence_finite p (q + 1)) (countedSequence_nonempty _ _)
-    haveI := isProbabilityMeasure_uniformOn
+    have := isProbabilityMeasure_uniformOn
       (countedSequence_finite (p + 1) q) (countedSequence_nonempty _ _)
     have h₃ : 0 < p + 1 + (q + 1) := Nat.add_pos_left (Nat.succ_pos _) _
     rw [← uniformOn_add_compl_eq {l : List ℤ | l.headI = 1} _ (countedSequence_finite _ _),
@@ -344,7 +344,7 @@ theorem ballot_problem' :
 theorem ballot_problem :
     ∀ q p, q < p → uniformOn (countedSequence p q) staysPositive = (p - q) / (p + q) := by
   intro q p qp
-  haveI :=
+  have :=
     isProbabilityMeasure_uniformOn (countedSequence_finite p q) (countedSequence_nonempty _ _)
   have :
     (uniformOn (countedSequence p q) staysPositive).toReal =

diff --git a/Archive/Wiedijk100Theorems/CubingACube.lean b/Archive/Wiedijk100Theorems/CubingACube.lean
@@ -378,7 +378,7 @@ variable (h v)
   direction will intersect one of the neighbouring cubes on the same boundary as `mi`. -/
 theorem mi_not_onBoundary (j : Fin n) : ¬OnBoundary (mi_mem_bcubes : mi h v ∈ _) j := by
   let i := mi h v; have hi : i ∈ bcubes cs c := mi_mem_bcubes
-  haveI := h.nontrivial_fin
+  have := h.nontrivial_fin
   rcases exists_ne j with ⟨j', hj'⟩
   intro hj
   rcases smallest_onBoundary hj with ⟨x, ⟨hx, h2x⟩, h3x⟩

diff --git a/Archive/Wiedijk100Theorems/FriendshipGraphs.lean b/Archive/Wiedijk100Theorems/FriendshipGraphs.lean
@@ -250,7 +250,7 @@ theorem false_of_three_le_degree (hd : G.IsRegularOfDegree d) (h : 3 ≤ d) : Fa
   have p_dvd_d_pred := (ZMod.natCast_eq_zero_iff _ _).mpr (d - 1).minFac_dvd
   have dpos : 1 ≤ d := by lia
   have d_cast : ↑(d - 1) = (d : ℤ) - 1 := by norm_cast
-  haveI : Fact p.Prime := ⟨Nat.minFac_prime (by lia)⟩
+  have : Fact p.Prime := ⟨Nat.minFac_prime (by lia)⟩
   have hp2 : 2 ≤ p := (Fact.out (p := p.Prime)).two_le
   have dmod : (d : ZMod p) = 1 := by
     rw [← Nat.succ_pred_eq_of_pos dpos, Nat.succ_eq_add_one, Nat.pred_eq_sub_one]

diff --git a/Counterexamples.lean b/Counterexamples.lean
@@ -1,29 +1,31 @@
-import Counterexamples.AharoniKorman
-import Counterexamples.CanonicallyOrderedCommSemiringTwoMul
-import Counterexamples.CharPZeroNeCharZero
-import Counterexamples.CliffordAlgebraNotInjective
-import Counterexamples.Cyclotomic105
-import Counterexamples.DimensionPolynomial
-import Counterexamples.DirectSumIsInternal
-import Counterexamples.DiscreteTopologyNonDiscreteUniformity
-import Counterexamples.EulerSumOfPowers
-import Counterexamples.Girard
-import Counterexamples.HeawoodUnitDistance
-import Counterexamples.HomogeneousPrimeNotPrime
-import Counterexamples.InvertibleModuleNotIdeal
-import Counterexamples.IrrationalPowerOfIrrational
-import Counterexamples.MapFloor
-import Counterexamples.MonicNonRegular
-import Counterexamples.Motzkin
-import Counterexamples.NowhereDifferentiable
-import Counterexamples.OrderedCancelAddCommMonoidWithBounds
-import Counterexamples.PeanoCurve
-import Counterexamples.Phillips
-import Counterexamples.PolynomialIsDomain
-import Counterexamples.Pseudoelement
-import Counterexamples.QuadraticForm
-import Counterexamples.SeminormLatticeNotDistrib
-import Counterexamples.SeparableNotSecondCountable
-import Counterexamples.SorgenfreyLine
-import Counterexamples.TopologistsSineCurve
-import Counterexamples.ZeroDivisorsInAddMonoidAlgebras
+module  -- shake: keep-all --deprecated_module: ignore
+
+public import Counterexamples.AharoniKorman
+public import Counterexamples.CanonicallyOrderedCommSemiringTwoMul
+public import Counterexamples.CharPZeroNeCharZero
+public import Counterexamples.CliffordAlgebraNotInjective
+public import Counterexamples.Cyclotomic105
+public import Counterexamples.DimensionPolynomial
+public import Counterexamples.DirectSumIsInternal
+public import Counterexamples.DiscreteTopologyNonDiscreteUniformity
+public import Counterexamples.EulerSumOfPowers
+public import Counterexamples.Girard
+public import Counterexamples.HeawoodUnitDistance
+public import Counterexamples.HomogeneousPrimeNotPrime
+public import Counterexamples.InvertibleModuleNotIdeal
+public import Counterexamples.IrrationalPowerOfIrrational
+public import Counterexamples.MapFloor
+public import Counterexamples.MonicNonRegular
+public import Counterexamples.Motzkin
+public import Counterexamples.NowhereDifferentiable
+public import Counterexamples.OrderedCancelAddCommMonoidWithBounds
+public import Counterexamples.PeanoCurve
+public import Counterexamples.Phillips
+public import Counterexamples.PolynomialIsDomain
+public import Counterexamples.Pseudoelement
+public import Counterexamples.QuadraticForm
+public import Counterexamples.SeminormLatticeNotDistrib
+public import Counterexamples.SeparableNotSecondCountable
+public import Counterexamples.SorgenfreyLine
+public import Counterexamples.TopologistsSineCurve
+public import Counterexamples.ZeroDivisorsInAddMonoidAlgebras
diff --git a/Counterexamples/AharoniKorman.lean b/Counterexamples/AharoniKorman.lean
@@ -3,12 +3,14 @@ Copyright (c) 2024 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
-import Mathlib.Algebra.Order.Field.Basic
-import Mathlib.Algebra.Order.Field.Rat
-import Mathlib.Data.Setoid.Partition
-import Mathlib.Order.Filter.AtTopBot.Basic
-import Mathlib.Order.Interval.Set.Infinite
-import Mathlib.Order.WellFoundedSet
+module
+
+public import Mathlib.Algebra.Order.Field.Basic
+public import Mathlib.Algebra.Order.Field.Rat
+public import Mathlib.Data.Setoid.Partition
+public import Mathlib.Order.Filter.AtTopBot.Basic
+public import Mathlib.Order.Interval.Set.Infinite
+public import Mathlib.Order.WellFoundedSet
 
 /-!
 # Disproof of the Aharoni–Korman conjecture
@@ -67,6 +69,8 @@ aim of reaching a contradiction (as then, no such partition can exist). We may f
   we have a contradiction (`no_spinalMap`), and therefore show that no spinal map exists.
 -/
 
+@[expose] public section
+
 attribute [aesop 2 simp] Set.subset_def Finset.subset_iff
 
 /-- A type synonym on ℕ³ on which we will construct Hollom's partial order P_5. -/

diff --git a/Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean b/Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean
@@ -3,8 +3,10 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import Mathlib.Algebra.Ring.Subsemiring.Order
-import Mathlib.Data.ZMod.Basic
+module
+
+public import Mathlib.Algebra.Ring.Subsemiring.Order
+public import Mathlib.Data.ZMod.Basic
 
 /-!
 # A canonically ordered commutative semiring where multiplication by 2 is not injective
@@ -24,7 +26,7 @@ Reference:
 https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/canonically_ordered.20pathology
 -/
 
-
+@[expose] public section
 
 namespace Counterexample
 

diff --git a/Counterexamples/CharPZeroNeCharZero.lean b/Counterexamples/CharPZeroNeCharZero.lean
@@ -3,8 +3,10 @@ Copyright (c) 2022 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa, Eric Wieser
 -/
-import Mathlib.Algebra.CharP.Lemmas
-import Mathlib.Algebra.Ring.PUnit
+module
+
+public import Mathlib.Algebra.CharP.Lemmas
+public import Mathlib.Algebra.Ring.PUnit
 
 /-! # `CharP R 0` and `CharZero R` need not coincide for semirings
 
@@ -19,6 +21,7 @@ This file shows that there are semirings `R` for which `CharP R 0` holds and `Ch
 The example is `{0, 1}` with saturating addition.
 -/
 
+@[expose] public section
 
 namespace Counterexample
 

diff --git a/Counterexamples/CliffordAlgebraNotInjective.lean b/Counterexamples/CliffordAlgebraNotInjective.lean
@@ -3,12 +3,14 @@ Copyright (c) 2021 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.Algebra.CharP.Pi
-import Mathlib.Algebra.CharP.Quotient
-import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
-import Mathlib.RingTheory.MvPolynomial.Basic
-import Mathlib.RingTheory.MvPolynomial.Ideal
-import Mathlib.Tactic.Ring.NamePolyVars
+module
+
+public import Mathlib.Algebra.CharP.Pi
+public import Mathlib.Algebra.CharP.Quotient
+public import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
+public import Mathlib.RingTheory.MvPolynomial.Basic
+public import Mathlib.RingTheory.MvPolynomial.Ideal
+public import Mathlib.Tactic.Ring.NamePolyVars
 
 /-! # `algebraMap R (CliffordAlgebra Q)` is not always injective.
 
@@ -30,10 +32,9 @@ As a bonus result, we also show `BilinMap.not_forall_toQuadraticMap_surjective`:
 are quadratic forms that cannot be expressed via even non-symmetric bilinear forms.
 -/
 
-noncomputable section
+@[expose] public noncomputable section
 
-open LinearMap (BilinForm)
-open LinearMap (BilinMap)
+open LinearMap (BilinForm BilinMap)
 
 name_poly_vars X, Y, Z over ZMod 2
 
@@ -154,7 +155,7 @@ theorem sq_map_add_char_two {ι R : Type*} [CommRing R] [CharP R 2] (i : ι) (a
 
 theorem sq_map_sub_char_two {ι R : Type*} [CommRing R] [CharP R 2] (i : ι) (a b : ι → R) :
     sq i (a - b) = sq i a - sq i b := by
-  haveI : Nonempty ι := ⟨i⟩
+  have : Nonempty ι := ⟨i⟩
   rw [CharTwo.sub_eq_add, CharTwo.sub_eq_add, sq_map_add_char_two]
 
 /-- The quadratic form (metric) is just Euclidean -/

diff --git a/Counterexamples/Cyclotomic105.lean b/Counterexamples/Cyclotomic105.lean
@@ -3,8 +3,10 @@ Copyright (c) 2021 Riccardo Brasca. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 -/
-import Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
-import Mathlib.Tactic.NormNum.Prime
+module
+
+public import Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
+public import Mathlib.Tactic.NormNum.Prime
 
 /-!
 # Not all coefficients of cyclotomic polynomials are -1, 0, or 1
@@ -14,9 +16,9 @@ theorem `not_forall_coeff_cyclotomic_neg_one_zero_one`. We prove this with the c
 `coeff_cyclotomic_105 : coeff (cyclotomic 105 ℤ) 7 = -2`.
 -/
 
+@[expose] public section
 
 open Nat (properDivisors)
-
 open Finset
 
 namespace Counterexample

diff --git a/Counterexamples/DimensionPolynomial.lean b/Counterexamples/DimensionPolynomial.lean
@@ -3,10 +3,12 @@ Copyright (c) 2025 Jingting Wang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jingting Wang
 -/
-import Mathlib.RingTheory.KrullDimension.Polynomial
-import Mathlib.RingTheory.KrullDimension.LocalRing
-import Mathlib.FieldTheory.RatFunc.AsPolynomial
-import Mathlib.RingTheory.PowerSeries.Inverse
+module
+
+public import Mathlib.RingTheory.KrullDimension.Polynomial
+public import Mathlib.RingTheory.KrullDimension.LocalRing
+public import Mathlib.FieldTheory.RatFunc.AsPolynomial
+public import Mathlib.RingTheory.PowerSeries.Inverse
 
 /-!
 # Krull dimension of polynomial ring
@@ -22,6 +24,8 @@ We define the commutative ring `A` as `{f ∈ k(t)⟦Y⟧ | f(0) ∈ k}` for a f
 <https://math.stackexchange.com/questions/1267419/examples-of-rings-whose-polynomial-rings-have-large-dimension>
 -/
 
+@[expose] public section
+
 namespace Counterexample
 
 namespace DimensionPolynomial

diff --git a/Counterexamples/DirectSumIsInternal.lean b/Counterexamples/DirectSumIsInternal.lean
@@ -3,10 +3,12 @@ Copyright (c) 2021 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser, Kevin Buzzard
 -/
-import Mathlib.Algebra.DirectSum.Module
-import Mathlib.Algebra.Group.ConjFinite
-import Mathlib.Data.Fintype.Lattice
-import Mathlib.Tactic.FinCases
+module
+
+public import Mathlib.Algebra.DirectSum.Module
+public import Mathlib.Algebra.Group.ConjFinite
+public import Mathlib.Data.Fintype.Lattice
+public import Mathlib.Tactic.FinCases
 
 /-!
 # Not all complementary decompositions of a module over a semiring make up a direct sum
@@ -19,6 +21,8 @@ This file demonstrates why `DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_
 take `Ring R` and not `Semiring R`.
 -/
 
+public section
+
 namespace Counterexample
 
 theorem UnitsInt.one_ne_neg_one : (1 : ℤˣ) ≠ -1 := by decide

diff --git a/Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean b/Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean
@@ -3,7 +3,9 @@ Copyright (c) 2024 Filippo A. E. Nuccio. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Filippo A. E. Nuccio
 -/
-import Mathlib.Analysis.SpecificLimits.Basic
+module
+
+public import Mathlib.Analysis.SpecificLimits.Basic
 
 /-!
 # Discrete uniformities and discrete topology
@@ -75,6 +77,8 @@ inequality) to explicit subsets, many proofs are easily closed by `aesop` or `om
 * [N. Bourbaki, *General Topology*, Chapter II][bourbaki1966]
 -/
 
+@[expose] public section
+
 open Set Function Filter Metric
 
 /- We remove the "usual" instances of (discrete) topological space and of (discrete) uniform space

diff --git a/Counterexamples/EulerSumOfPowers.lean b/Counterexamples/EulerSumOfPowers.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Snir Broshi. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Snir Broshi, Michael Stoll
 -/
-import Mathlib.NumberTheory.FLT.Three
+module
+
+public import Mathlib.NumberTheory.FLT.Three
 
 /-!
 # Euler's sum of powers conjecture
@@ -27,6 +29,7 @@ http://euler.free.fr/
   https://www.ams.org/journals/mcom/1988-51-184/S0025-5718-1988-0930224-9/S0025-5718-1988-0930224-9.pdf
 -/
 
+@[expose] public section
 
 namespace Counterexample
 

diff --git a/Counterexamples/Girard.lean b/Counterexamples/Girard.lean
@@ -3,8 +3,10 @@ Copyright (c) 2021 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Logic.Basic
-import Mathlib.Data.Set.Defs
+module
+
+public import Mathlib.Logic.Basic
+public import Mathlib.Data.Set.Defs
 
 /-!
 # Girard's paradox
@@ -25,6 +27,7 @@ Based on Watkins' LF implementation of Hurkens' simplification of Girard's parad
 * `girard`: there are no Girard universes.
 -/
 
+@[expose] public section
 
 namespace Counterexample