chore: lake shake --add-public --keep-implied --keep-prefix --fix

Mathlib/Algebra/Algebra/StrictPositivity.lean

@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
 public import Mathlib.Algebra.Order.Star.Basic
 public import Mathlib.Algebra.Order.Module.Defs
 public import Mathlib.Tactic.ContinuousFunctionalCalculus
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Strictly positive elements of an algebra

Mathlib/Algebra/Algebra/Subalgebra/Rank.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.LinearAlgebra.Dimension.Free
 public import Mathlib.LinearAlgebra.Dimension.Subsingleton
 public import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 

Mathlib/Algebra/Algebra/Unitization.lean

@@ -13,7 +13,6 @@ public import Mathlib.Algebra.Star.NonUnitalSubalgebra
 public import Mathlib.LinearAlgebra.Prod
 public import Mathlib.Tactic.Abel
 public import Mathlib.Algebra.GroupWithZero.Action.TransferInstance
-public import Mathlib.Algebra.Algebra.TransferInstance
 public import Mathlib.Algebra.Module.TransferInstance
 
 /-!

Mathlib/Algebra/Azumaya/Matrix.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Azumaya.Defs
 public import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Matrix algebra is an Azumaya algebra over R

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -7,16 +7,14 @@ module
 
 public import Mathlib.Algebra.BigOperators.Pi
 public import Mathlib.Algebra.FiniteSupport.Defs
-public import Mathlib.Algebra.Group.Indicator
-public import Mathlib.Algebra.Group.Support
 public import Mathlib.Algebra.Module.Torsion.Free
 public import Mathlib.Algebra.Notation.FiniteSupport
 public import Mathlib.Algebra.Order.Ring.Defs
-public import Mathlib.Data.Set.Finite.Lattice
 
 import Mathlib.Algebra.FiniteSupport.Basic
 import Mathlib.Algebra.Module.End
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Finite products and sums over types and sets

Mathlib/Algebra/BigOperators/Group/List/Basic.lean

@@ -16,6 +16,7 @@ public import Mathlib.Algebra.Group.Commute.Defs
 public import Mathlib.Algebra.Group.Nat.Defs
 public import Mathlib.Algebra.Group.Int.Defs
 public import Mathlib.Order.Basic
+public import Mathlib.Data.List.Basic
 
 /-!
 # Sums and products from lists

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
 public import Mathlib.Algebra.Order.Interval.Finset.Basic
 public import Mathlib.Algebra.Order.Sub.Basic
 public import Mathlib.Data.Fintype.BigOperators
+public import Mathlib.Data.Nat.Factorial.Basic
 
 /-!
 # Results about big operators over intervals

Mathlib/Algebra/Category/Ring/Limits.lean

@@ -8,8 +8,8 @@ module
 public import Mathlib.Algebra.Category.Grp.Limits
 public import Mathlib.Algebra.Category.Ring.Basic
 public import Mathlib.Algebra.Ring.Pi
-public import Mathlib.Algebra.Ring.Shrink
 public import Mathlib.Algebra.Ring.Subring.Defs
+public import Mathlib.Algebra.Ring.TransferInstance
 
 /-!
 # The category of (commutative) rings has all limits

Mathlib/Algebra/Category/Ring/Topology.lean

@@ -7,9 +7,9 @@ module
 
 public import Mathlib.Algebra.Category.Ring.Colimits
 public import Mathlib.Algebra.Category.Ring.Constructions
-public import Mathlib.Algebra.MvPolynomial.CommRing
 public import Mathlib.Topology.Algebra.Ring.Basic
 public import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
+public import Mathlib.Algebra.MvPolynomial.Eval
 
 /-!
 # Topology on `Hom(R, S)`

Mathlib/Algebra/CharP/Defs.lean

@@ -10,6 +10,7 @@ public import Mathlib.Data.Nat.Find
 public import Mathlib.Data.Nat.Prime.Defs
 public import Mathlib.Data.Int.Cast.Basic
 public import Mathlib.Order.Lattice
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Characteristic of semirings

Mathlib/Algebra/CubicDiscriminant.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Polynomial.Splits
 public import Mathlib.Tactic.IntervalCases
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Cubics and discriminants

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Jens Wagemaker
 module
 
 public import Mathlib.Algebra.Ring.Associated
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Monoids with normalization functions, `gcd`, and `lcm`

Mathlib/Algebra/Group/Conj.lean

@@ -5,8 +5,11 @@ Authors: Patrick Massot, Chris Hughes, Michael Howes
 -/
 module
 
-public import Mathlib.Algebra.Group.End
 public import Mathlib.Algebra.Group.Semiconj.Units
+public import Mathlib.Algebra.Group.Units.Hom
+public import Mathlib.Data.Set.Operations
+public import Mathlib.Tactic.Common
+public import Mathlib.Tactic.Finiteness.Attr
 
 /-!
 # Conjugacy of group elements

Mathlib/Algebra/Group/Fin/Basic.lean

@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Group.Basic
 public import Mathlib.Algebra.NeZero
 public import Mathlib.Data.Nat.Cast.Defs
 public import Mathlib.Data.Fin.Rev
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Fin is a group

Mathlib/Algebra/Group/Int/Even.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Group.Int.Defs
 public import Mathlib.Algebra.Group.Nat.Even
 public import Mathlib.Data.Int.Sqrt
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Parity of integers

Mathlib/Algebra/Group/Nat/Even.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Group.Even
 public import Mathlib.Algebra.Group.Nat.Defs
 public import Mathlib.Data.Nat.Sqrt
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # `IsSquare` and `Even` for natural numbers

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Group.Conj
 public import Mathlib.Algebra.Group.Pi.Lemmas
 public import Mathlib.Algebra.Group.Subgroup.Ker
 public import Mathlib.Algebra.Group.Torsion
+public import Mathlib.Algebra.Group.End
 
 /-!
 # Basic results on subgroups

Mathlib/Algebra/Group/Subgroup/Ker.lean

@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.Group.Subgroup.Map
 public import Mathlib.Tactic.ApplyFun
 
-import Mathlib.Algebra.Group.Equiv.Basic
 
 /-!
 # Kernel and range of group homomorphisms

Mathlib/Algebra/Group/Submonoid/Support.lean

@@ -5,10 +5,10 @@ Authors: Artie Khovanov
 -/
 module
 
-public import Mathlib.Algebra.Group.Subgroup.Pointwise
 public import Mathlib.Algebra.Group.Subgroup.Lattice
 
 import Mathlib.Tactic.ApplyFun
+public import Mathlib.Algebra.Group.Submonoid.Pointwise
 
 /-!
 # Supports of submonoids

Mathlib/Algebra/Group/UniqueProds/Basic.lean

@@ -12,6 +12,7 @@ public import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 public import Mathlib.Algebra.Group.TypeTags.Basic
 public import Mathlib.Algebra.Group.ULift
 public import Mathlib.Data.DFinsupp.Defs
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Unique products and related notions

Mathlib/Algebra/GroupWithZero/Units/Basic.lean

@@ -13,6 +13,7 @@ public import Mathlib.Tactic.Contrapose
 public import Mathlib.Tactic.Spread
 public import Mathlib.Tactic.Convert
 public import Mathlib.Tactic.Nontriviality
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Lemmas about units in a `MonoidWithZero` or a `GroupWithZero`.

Mathlib/Algebra/Homology/DerivedCategory/Ext/Map.lean

@@ -5,7 +5,6 @@ Authors: Nailin Guan, Jingting Wang
 -/
 module
 
-public import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
 public import Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor

Mathlib/Algebra/Homology/HomologicalComplexAbelian.lean

@@ -7,7 +7,6 @@ module
 
 public import Mathlib.Algebra.Homology.Additive
 public import Mathlib.Algebra.Homology.HomologicalComplexLimits
-public import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
 public import Mathlib.Algebra.Homology.ShortComplex.ShortExact
 
 /-! # THe category of homological complexes is abelian

Mathlib/Algebra/Homology/ModelCategory/Lifting.lean

@@ -5,7 +5,8 @@ Authors: Joël Riou
 -/
 module
 
-public import Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
+public import Mathlib.Algebra.Homology.HomologicalComplexLimits
+public import Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
 
 /-!
 # Lifting properties in cochain complexes

Mathlib/Algebra/LinearRecurrence.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Polynomial.Degree.Operations
 public import Mathlib.Algebra.Polynomial.Eval.Defs
 public import Mathlib.LinearAlgebra.Dimension.Constructions
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Linear recurrence

Mathlib/Algebra/Module/Injective.lean

@@ -10,7 +10,9 @@ public import Mathlib.Algebra.Module.Shrink
 public import Mathlib.LinearAlgebra.LinearPMap
 public import Mathlib.LinearAlgebra.Pi
 public import Mathlib.Logic.Small.Basic
-public import Mathlib.RingTheory.Ideal.Maps
+public import Mathlib.LinearAlgebra.BilinearMap
+public import Mathlib.RingTheory.Ideal.Defs
+public import Mathlib.Tactic.NormNum
 
 /-!
 # Injective modules

Mathlib/Algebra/Module/LinearMap/Polynomial.lean

@@ -11,6 +11,7 @@ public import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 public import Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
 public import Mathlib.RingTheory.TensorProduct.Finite
 public import Mathlib.RingTheory.TensorProduct.Free
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Characteristic polynomials of linear families of endomorphisms

Mathlib/Algebra/Module/SpanRank.lean

@@ -6,7 +6,6 @@ Authors: Wanyi He, Jiedong Jiang, Xuchun Li, Christian Merten, Jingting Wang, An
 module
 
 public import Mathlib.Data.ENat.Lattice
-public import Mathlib.LinearAlgebra.Dimension.Free
 public import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
 public import Mathlib.RingTheory.Finiteness.Ideal
 

Mathlib/Algebra/Module/Submodule/Invariant.lean

@@ -5,7 +5,6 @@ Authors: Oliver Nash
 -/
 module
 
-public import Mathlib.Algebra.Algebra.Defs
 public import Mathlib.Algebra.Module.Equiv.Basic
 public import Mathlib.Algebra.Module.Submodule.Map
 public import Mathlib.LinearAlgebra.Span.Defs

Mathlib/Algebra/Module/Torsion/PrimaryComponent.lean

@@ -6,7 +6,7 @@ Authors: Xavier Généreux, María Inés de Frutos Fernández
 module
 
 public import Mathlib.Algebra.Module.Torsion.Basic
-public import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
+public import Mathlib.Tactic.Positivity
 
 /-!
 # I-Primary Components of modules

Mathlib/Algebra/MonoidAlgebra/Defs.lean

@@ -5,10 +5,10 @@ Authors: Johannes Hölzl, Yury Kudryashov, Kim Morrison
 -/
 module
 
-public import Mathlib.Algebra.GroupWithZero.Action.TransferInstance
 public import Mathlib.Algebra.Module.Defs
 public import Mathlib.Data.Finsupp.Basic
 public import Mathlib.Data.Finsupp.SMulWithZero
+public import Mathlib.Algebra.Group.TransferInstance
 
 /-!
 # Monoid algebras

Mathlib/Algebra/MvPolynomial/Basic.lean

@@ -15,6 +15,7 @@ public import Mathlib.Algebra.Regular.Pow
 public import Mathlib.Data.Finsupp.Antidiagonal
 public import Mathlib.Data.Finsupp.Order
 public import Mathlib.Order.SymmDiff
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Multivariate polynomials

Mathlib/Algebra/MvPolynomial/Cardinal.lean

@@ -6,9 +6,11 @@ Authors: Chris Hughes, Junyan Xu
 module
 
 public import Mathlib.Algebra.MonoidAlgebra.Cardinal
-public import Mathlib.Algebra.MvPolynomial.Equiv
 public import Mathlib.Data.Finsupp.Fintype
 public import Mathlib.SetTheory.Cardinal.Finsupp
+public import Mathlib.Algebra.MvPolynomial.Basic
+public import Mathlib.Tactic.NormNum
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Cardinality of Multivariate Polynomial Ring

Mathlib/Algebra/MvPolynomial/Division.lean

@@ -6,8 +6,9 @@ Authors: Eric Wieser
 module
 
 public import Mathlib.Algebra.MonoidAlgebra.Division
-public import Mathlib.Algebra.MvPolynomial.CommRing
 public import Mathlib.Data.Finsupp.Weight
+public import Mathlib.Algebra.MvPolynomial.Basic
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Division of `MvPolynomial` by monomials

Mathlib/Algebra/MvPolynomial/Equiv.lean

@@ -10,7 +10,6 @@ public import Mathlib.Algebra.MvPolynomial.Degrees
 public import Mathlib.Algebra.MvPolynomial.Rename
 public import Mathlib.Algebra.Polynomial.AlgebraMap
 public import Mathlib.Algebra.MonoidAlgebra.Basic
-public import Mathlib.Algebra.Polynomial.Degree.Lemmas
 public import Mathlib.Data.Finsupp.Option
 public import Mathlib.Logic.Equiv.Fin.Basic
 

Mathlib/Algebra/MvPolynomial/Funext.lean

@@ -7,7 +7,6 @@ module
 
 public import Mathlib.Algebra.Polynomial.RingDivision
 public import Mathlib.Algebra.Polynomial.Roots
-public import Mathlib.Algebra.MvPolynomial.CommRing
 public import Mathlib.Algebra.MvPolynomial.Polynomial
 public import Mathlib.Algebra.MvPolynomial.Rename
 

Mathlib/Algebra/MvPolynomial/Nilpotent.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.RingTheory.MvPolynomial.Homogeneous
 public import Mathlib.RingTheory.Polynomial.Nilpotent
+public import Mathlib.Algebra.MvPolynomial.CommRing
 
 /-!
 # Nilpotents and units in multivariate polynomial rings

Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean

@@ -9,6 +9,7 @@ public import Mathlib.Algebra.MvPolynomial.Variables
 public import Mathlib.Algebra.MvPolynomial.Equiv
 public import Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex
 public import Mathlib.Algebra.MvPolynomial.Division
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Multivariate polynomials over integral domains

Mathlib/Algebra/Order/Archimedean/Basic.lean

@@ -11,6 +11,7 @@ public import Mathlib.Algebra.Order.Ring.Pow
 public import Mathlib.Data.Int.LeastGreatest
 public import Mathlib.Data.Rat.Floor
 import Mathlib.Algebra.Order.Group.Basic
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Archimedean groups and fields.

Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.lean

@@ -7,7 +7,8 @@ module
 
 public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 public import Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
-public import Mathlib.Tactic.Ring
+public import Mathlib.Tactic.NormNum.Inv
+public import Mathlib.Tactic.NormNum.Pow
 
 /-!
 # Big operators on a finset in groups with zero involving order

Mathlib/Algebra/Order/BigOperators/Ring/List.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Order.Ring.Canonical
 public import Batteries.Data.List.Lemmas
+public import Batteries.Data.List
 
 /-!
 # Big operators on a list in ordered rings

Mathlib/Algebra/Order/Field/Power.lean

@@ -10,6 +10,7 @@ public import Mathlib.Algebra.Order.Ring.Abs
 public import Mathlib.Algebra.Order.Ring.Pow
 public import Mathlib.Algebra.Ring.CharZero
 public import Mathlib.Tactic.Positivity.Core
+meta import Mathlib.Tactic.Attr.Register
 
 /-!
 # Lemmas about powers in ordered fields.

Mathlib/Algebra/Order/Group/Indicator.lean

@@ -6,10 +6,11 @@ Authors: Yury Kudryashov
 module
 
 public import Mathlib.Algebra.Group.Indicator
-public import Mathlib.Order.ConditionallyCompleteLattice.Indexed
 public import Mathlib.Algebra.Order.Group.Synonym
 public import Mathlib.Algebra.Order.Group.Unbundled.Abs
 public import Mathlib.Algebra.Order.Monoid.Canonical.Defs
+public import Mathlib.Order.ConditionallyCompleteLattice.Basic
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
 
 /-!
 # Support of a function in an order