From c2694d30f04a9e5c028efd04efd1e1cc94696e85 Mon Sep 17 00:00:00 2001 From: Batixx Date: Fri, 24 Jul 2026 16:15:35 +0200 Subject: [PATCH 1/3] chore: no newline between public imports --- Mathlib/Algebra/Group/End.lean | 1 - Mathlib/AlgebraicGeometry/Sites/EtalePoint.lean | 1 - Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean | 1 - Mathlib/Logic/Basic.lean | 1 - Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean | 1 - Mathlib/RingTheory/SimpleModule/Basic.lean | 1 - Mathlib/RingTheory/Valuation/Extension.lean | 1 - Mathlib/Tactic/Common.lean | 1 - Mathlib/Tactic/NormNum/Result.lean | 1 - Mathlib/Topology/Algebra/Valued/ValuationTopology.lean | 1 - Mathlib/Topology/Defs/Basic.lean | 1 - 11 files changed, 11 deletions(-) diff --git a/Mathlib/Algebra/Group/End.lean b/Mathlib/Algebra/Group/End.lean index d097f727d007bf..f2ad7a65fbacbf 100644 --- a/Mathlib/Algebra/Group/End.lean +++ b/Mathlib/Algebra/Group/End.lean @@ -11,7 +11,6 @@ public import Mathlib.Algebra.Group.Prod public import Mathlib.Algebra.Group.Units.Equiv public import Mathlib.Data.Set.Basic public import Mathlib.Tactic.Common - public import Mathlib.Tactic.Attr.Register /-! diff --git a/Mathlib/AlgebraicGeometry/Sites/EtalePoint.lean b/Mathlib/AlgebraicGeometry/Sites/EtalePoint.lean index 080431e447073f..0bbd1ed50c603b 100644 --- a/Mathlib/AlgebraicGeometry/Sites/EtalePoint.lean +++ b/Mathlib/AlgebraicGeometry/Sites/EtalePoint.lean @@ -10,7 +10,6 @@ public import Mathlib.AlgebraicGeometry.Sites.AffineEtale public import Mathlib.CategoryTheory.Functor.TypeValuedFlat public import Mathlib.CategoryTheory.Limits.Elements public import Mathlib.CategoryTheory.Sites.Point.Conservative - public import Mathlib.FieldTheory.SeparableClosure /-! diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean index 8aa500bba2a819..199ab8efa6025d 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean @@ -7,7 +7,6 @@ module public import Mathlib.LinearAlgebra.AffineSpace.AffineEquiv public import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs - public import Mathlib.Algebra.NoZeroSMulDivisors.Basic /-! diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean index ebcd43198e0ad1..ddf2c7599e4a50 100644 --- a/Mathlib/Logic/Basic.lean +++ b/Mathlib/Logic/Basic.lean @@ -8,7 +8,6 @@ module public import Mathlib.Lean.Meta.Simp public import Batteries.Logic public import Batteries.Util.LibraryNote - public import Mathlib.Tactic.Attr.Register /-! diff --git a/Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean b/Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean index 37d55774ebae66..4621f8f399acff 100644 --- a/Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean +++ b/Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean @@ -7,7 +7,6 @@ module public import Mathlib.Analysis.Normed.Ring.Basic public import Mathlib.RingTheory.MvPowerSeries.Basic - public import Mathlib.Algebra.Order.Ring.IsNonarchimedean /-! diff --git a/Mathlib/RingTheory/SimpleModule/Basic.lean b/Mathlib/RingTheory/SimpleModule/Basic.lean index d959b463994b1b..9d011b5a840eda 100644 --- a/Mathlib/RingTheory/SimpleModule/Basic.lean +++ b/Mathlib/RingTheory/SimpleModule/Basic.lean @@ -16,7 +16,6 @@ public import Mathlib.Order.JordanHolder public import Mathlib.RingTheory.Ideal.Colon public import Mathlib.RingTheory.Noetherian.Defs public import Mathlib.SetTheory.Cardinal.NatCard - public import Mathlib.Algebra.NoZeroSMulDivisors.Basic /-! diff --git a/Mathlib/RingTheory/Valuation/Extension.lean b/Mathlib/RingTheory/Valuation/Extension.lean index 2cd3a3fc4c5405..71f15d7604fca8 100644 --- a/Mathlib/RingTheory/Valuation/Extension.lean +++ b/Mathlib/RingTheory/Valuation/Extension.lean @@ -6,7 +6,6 @@ Authors: Jiedong Jiang, Bichang Lei, María Inés de Frutos-Fernández, Filippo module public import Mathlib.RingTheory.Valuation.ValuationSubring - public import Mathlib.Algebra.NoZeroSMulDivisors.Basic /-! diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean index 01fa2cdc218664..77101da34d58a4 100644 --- a/Mathlib/Tactic/Common.lean +++ b/Mathlib/Tactic/Common.lean @@ -122,7 +122,6 @@ public import Mathlib.Util.CountHeartbeats public import Mathlib.Util.PrintSorries public import Mathlib.Util.TransImports public import Mathlib.Util.WhatsNew - public import Lean.Elab.Tactic.Try /-! diff --git a/Mathlib/Tactic/NormNum/Result.lean b/Mathlib/Tactic/NormNum/Result.lean index 8583027f5b8b9d..1a326aa22980e0 100644 --- a/Mathlib/Tactic/NormNum/Result.lean +++ b/Mathlib/Tactic/NormNum/Result.lean @@ -10,7 +10,6 @@ public import Mathlib.Algebra.GroupWithZero.Invertible public import Mathlib.Algebra.Ring.Nat public import Mathlib.Data.Int.Cast.Basic public import Qq.MetaM - public meta import Mathlib.Data.Sigma.Basic -- for the `Inhabited (Sigma β)` instance /-! diff --git a/Mathlib/Topology/Algebra/Valued/ValuationTopology.lean b/Mathlib/Topology/Algebra/Valued/ValuationTopology.lean index 2eeaf86c8b915a..8cce79014c391e 100644 --- a/Mathlib/Topology/Algebra/Valued/ValuationTopology.lean +++ b/Mathlib/Topology/Algebra/Valued/ValuationTopology.lean @@ -9,7 +9,6 @@ public import Mathlib.Algebra.Order.Group.Units public import Mathlib.Topology.Algebra.Nonarchimedean.Bases public import Mathlib.Topology.Algebra.UniformFilterBasis public import Mathlib.RingTheory.Valuation.ValuationSubring - public import Mathlib.Algebra.Order.GroupWithZero.Range /-! diff --git a/Mathlib/Topology/Defs/Basic.lean b/Mathlib/Topology/Defs/Basic.lean index 25731ef39ec5b2..0928608045054f 100644 --- a/Mathlib/Topology/Defs/Basic.lean +++ b/Mathlib/Topology/Defs/Basic.lean @@ -11,7 +11,6 @@ public import Mathlib.Tactic.CrossRefAttribute public import Mathlib.Tactic.FunProp public import Mathlib.Tactic.MkIffOfInductiveProp public import Mathlib.Data.Nat.Notation - public meta import Mathlib.Util.DelabNonCanonical /-! From 08eaff2e6c64efe964705d45f490abd93d914d56 Mon Sep 17 00:00:00 2001 From: Felix Pernegger Date: Fri, 24 Jul 2026 20:42:41 +0200 Subject: [PATCH 2/3] Update Result.lean --- Mathlib/Tactic/NormNum/Result.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Tactic/NormNum/Result.lean b/Mathlib/Tactic/NormNum/Result.lean index 1a326aa22980e0..8583027f5b8b9d 100644 --- a/Mathlib/Tactic/NormNum/Result.lean +++ b/Mathlib/Tactic/NormNum/Result.lean @@ -10,6 +10,7 @@ public import Mathlib.Algebra.GroupWithZero.Invertible public import Mathlib.Algebra.Ring.Nat public import Mathlib.Data.Int.Cast.Basic public import Qq.MetaM + public meta import Mathlib.Data.Sigma.Basic -- for the `Inhabited (Sigma β)` instance /-! From 815258f10e1e972d2a2ce7a3e676a7bc953598ad Mon Sep 17 00:00:00 2001 From: Felix Pernegger Date: Fri, 24 Jul 2026 20:43:01 +0200 Subject: [PATCH 3/3] Add import for DelabNonCanonical utility --- Mathlib/Topology/Defs/Basic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Topology/Defs/Basic.lean b/Mathlib/Topology/Defs/Basic.lean index 0928608045054f..25731ef39ec5b2 100644 --- a/Mathlib/Topology/Defs/Basic.lean +++ b/Mathlib/Topology/Defs/Basic.lean @@ -11,6 +11,7 @@ public import Mathlib.Tactic.CrossRefAttribute public import Mathlib.Tactic.FunProp public import Mathlib.Tactic.MkIffOfInductiveProp public import Mathlib.Data.Nat.Notation + public meta import Mathlib.Util.DelabNonCanonical /-!