chore: run the new shake tool (leanprover-community#32731)

This is a first candidate run of the [new module-aware Shake](https://github.com/leanprover/lean4/blob/master/script/Shake.lean) on Mathlib. It has been run manually on nightly-testing-green and then rebased onto master as some Lean-side changes to be released in the next RC are needed.

Known limitations:
* If a command `attribute [attr] decl` is imported, the import will be preserved if `decl` is referenced in any way in the file. This is a conservative approximation that avoids having to extend every single attribute implementation with precise tracking but may lead to redundant imports especially if often-used declarations such as `id` are tagged.

Co-authored-by: Kim Morrison <kim@tqft.net>

Author: Kha

Archive/Imo/Imo2024Q5.lean

@@ -7,8 +7,9 @@ import Mathlib.Data.Fin.VecNotation
 import Mathlib.Data.List.ChainOfFn
 import Mathlib.Data.List.TakeWhile
 import Mathlib.Data.Nat.Dist
-import Mathlib.Order.Fin.Basic
+import Mathlib.Data.Fintype.Fin
 import Mathlib.Tactic.IntervalCases
+import Mathlib.Tactic.FinCases
 
 /-!
 # IMO 2024 Q5

Counterexamples/GameMultiplication.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Violeta Hernández Palacios
 -/
 
+import Mathlib.Data.Fintype.Fin
 import Mathlib.SetTheory.Game.Basic
 import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.Linter.DeprecatedModule

Mathlib.lean

@@ -1,4 +1,4 @@
-module
+module  -- shake: keep-all
 
 public import Std
 public import Batteries

Mathlib/Algebra/AffineMonoid/Embedding.lean

@@ -14,6 +14,7 @@ import Mathlib.Algebra.EuclideanDomain.Int
 import Mathlib.GroupTheory.MonoidLocalization.Finite
 import Mathlib.LinearAlgebra.Dimension.Free
 import Mathlib.LinearAlgebra.FreeModule.PID
+public import Mathlib.LinearAlgebra.Dimension.Free
 
 /-!
 # Affine monoids embed into `ℤⁿ`

Mathlib/Algebra/AffineMonoid/Irreducible.lean

@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.Group.Irreducible.Defs
 public import Mathlib.GroupTheory.Finiteness
 
-import Mathlib.Algebra.Group.Submonoid.BigOperators
 
 /-!
 # An affine monoid with no non-trivial unit is generated by its irreducible elements

Mathlib/Algebra/Algebra/Subalgebra/Order.lean

@@ -6,7 +6,6 @@ Authors: Damiano Testa
 module
 
 public import Mathlib.Algebra.Algebra.Subalgebra.Basic
-public import Mathlib.Algebra.Module.Submodule.Order
 public import Mathlib.Algebra.Ring.Subsemiring.Order
 
 /-!

Mathlib/Algebra/ArithmeticGeometric.lean

@@ -1,5 +1,8 @@
 module
 
-public import Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
+public import Mathlib.Algebra.Order.Module.Field
+public import Mathlib.Data.EReal.Inv
+public import Mathlib.Topology.Algebra.InfiniteSum.Order
+public import Mathlib.Topology.MetricSpace.Bounded
 
 deprecated_module (since := "2025-09-17")

Mathlib/Algebra/Azumaya/Basic.lean

@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.Azumaya.Defs
 public import Mathlib.Algebra.Central.End
 public import Mathlib.Algebra.Central.TensorProduct
-public import Mathlib.LinearAlgebra.Matrix.ToLin
 public import Mathlib.RingTheory.Finiteness.Basic
 public import Mathlib.GroupTheory.GroupAction.Hom
 public import Mathlib.RingTheory.TensorProduct.Maps

Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean

@@ -10,6 +10,7 @@ public import Mathlib.Algebra.Group.TypeTags.Basic
 public import Mathlib.Algebra.BigOperators.Group.Multiset.Defs
 public import Mathlib.Data.Fintype.Sets
 public import Mathlib.Data.Multiset.Bind
+public meta import Mathlib.Tactic.ToDual
 
 /-!
 # Big operators

Mathlib/Algebra/BigOperators/Group/Finset/Interval.lean

@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.CharP.Defs
 public import Mathlib.Algebra.Group.EvenFunction
 public import Mathlib.Data.Int.Interval
-public import Mathlib.Tactic.Zify
 
 /-!
 # Sums/products over integer intervals