leanprover-community · mathlib-nolints · Sep 13, 2026 · Sep 13, 2026
diff --git a/Mathlib/Algebra/Group/Equiv/TypeTags.lean b/Mathlib/Algebra/Group/Equiv/TypeTags.lean
@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.Group.TypeTags.Hom
 public import Mathlib.Algebra.Group.Equiv.Defs
 public import Mathlib.Algebra.Notation.Prod
-public import Mathlib.Tactic.Spread
 
 /-!
 # Additive and multiplicative equivalences associated to `Multiplicative` and `Additive`.

diff --git a/Mathlib/Algebra/Regular/Pi.lean b/Mathlib/Algebra/Regular/Pi.lean
@@ -6,7 +6,7 @@ Authors: Eric Wieser
 module
 
 public import Mathlib.Algebra.Regular.SMul
-public import Mathlib.Algebra.Notation.Pi.Basic
+public import Mathlib.Algebra.Notation.Pi.Defs
 
 /-!
 # Results about `IsRegular` and pi types

diff --git a/Mathlib/Algebra/Regular/SMul.lean b/Mathlib/Algebra/Regular/SMul.lean
@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.Group.Units.Defs
 public import Mathlib.Algebra.Group.Action.Defs
 public import Mathlib.Algebra.Group.Basic
-public import Mathlib.Tactic.Convert
 public import Mathlib.Tactic.Push
 
 /-!

diff --git a/Mathlib/Analysis/Asymptotics/TVS.lean b/Mathlib/Analysis/Asymptotics/TVS.lean
@@ -10,7 +10,6 @@ public import Mathlib.Analysis.LocallyConvex.BalancedCoreHull
 public import Mathlib.Analysis.Normed.Module.Seminorm.Basic
 public import Mathlib.Analysis.Asymptotics.Defs
 public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
-import Mathlib.Tactic.Peel
 public import Mathlib.Topology.Instances.ENNReal.Lemmas
 
 /-!

diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unitary.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unitary.lean
@@ -5,7 +5,6 @@ Authors: Jireh Loreaux
 -/
 module
 
-public import Mathlib.Tactic.Peel
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
 public import Mathlib.Analysis.Complex.Basic
 

diff --git a/Mathlib/Analysis/Complex/AbelLimit.lean b/Mathlib/Analysis/Complex/AbelLimit.lean
@@ -7,7 +7,6 @@ module
 
 public import Mathlib.Analysis.Complex.Basic
 public import Mathlib.Analysis.SpecificLimits.Normed
-public import Mathlib.Tactic.Peel
 public import Mathlib.Tactic.Positivity
 
 /-!

diff --git a/Mathlib/Data/Int/Basic.lean b/Mathlib/Data/Int/Basic.lean
@@ -11,6 +11,7 @@ public import Mathlib.Logic.Function.Basic
 public import Mathlib.Tactic.Conv
 public import Mathlib.Tactic.Convert
 public import Mathlib.Tactic.OfNat
+public import Mathlib.Tactic.GCongr
 
 /-!
 # Basic operations on the integers

diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
@@ -12,6 +12,7 @@ public import Mathlib.Tactic.Common
 public import Batteries.Data.List.Lemmas
 public import Mathlib.Data.Subtype
 public import Mathlib.Tactic.Attr.Core
+public import Batteries.Tactic.SeqFocus
 
 /-!
 # Basic properties of lists

diff --git a/Mathlib/Data/Matrix/Cartan.lean b/Mathlib/Data/Matrix/Cartan.lean
@@ -1,5 +1,9 @@
 module
 
-public import Mathlib.LinearAlgebra.Matrix.Cartan.Basic
+public import Mathlib.Algebra.Order.Field.Basic
+public import Mathlib.Data.Nat.Totient
+public import Mathlib.Data.Sym.Sym2
+public import Mathlib.Tactic.ContinuousFunctionalCalculus
+public import Mathlib.Tactic.NormNum.GCD
 
 deprecated_module (since := "2026-06-05")
diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean
@@ -9,7 +9,8 @@ public import Mathlib.Basic.Logic.Basic
 public import Mathlib.Basic.Nontrivial.Defs
 public import Mathlib.Data.Nat.Init
 public import Mathlib.Order.Defs.LinearOrder
-public import Mathlib.Tactic.GCongr
+public import Mathlib.Data.Set.Defs
+public import Mathlib.Tactic.Basic
 
 /-!
 # Basic operations on the natural numbers

diff --git a/Mathlib/Data/Nat/MaxPowDiv.lean b/Mathlib/Data/Nat/MaxPowDiv.lean
@@ -7,6 +7,7 @@ module
 
 
 import Mathlib.Data.Nat.Notation
+public import Mathlib.Data.Nat.Notation
 
 /-!
 # The maximal power of one natural number dividing another

diff --git a/Mathlib/Data/Nat/Sqrt.lean b/Mathlib/Data/Nat/Sqrt.lean
@@ -6,6 +6,7 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 module
 
 public import Mathlib.Data.Nat.Basic
+public import Mathlib.Tactic.GCongr
 
 /-!
 # Properties of the natural number square root function.

diff --git a/Mathlib/GroupTheory/CommutingProbability.lean b/Mathlib/GroupTheory/CommutingProbability.lean
@@ -6,7 +6,6 @@ Authors: Thomas Browning
 module
 
 public import Mathlib.Algebra.BigOperators.Fin
-public import Mathlib.GroupTheory.Abelianization.Finite
 public import Mathlib.GroupTheory.SpecificGroups.Dihedral
 public import Mathlib.Tactic.FieldSimp
 public import Mathlib.Tactic.Qify

diff --git a/Mathlib/GroupTheory/Exponent.lean b/Mathlib/GroupTheory/Exponent.lean
@@ -10,7 +10,6 @@ public import Mathlib.Algebra.GCDMonoid.Nat
 public import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
 public import Mathlib.Data.Nat.Factorization.LCM
 public import Mathlib.GroupTheory.OrderOfElement
-public import Mathlib.Tactic.Peel
 
 /-!
 # Exponent of a group

diff --git a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean
@@ -12,7 +12,6 @@ public import Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
 public import Mathlib.RingTheory.Nilpotent.Basic
 public import Mathlib.RingTheory.Nilpotent.Defs
 public import Mathlib.RingTheory.Nilpotent.Lemmas
-public import Mathlib.Tactic.Peel
 
 /-!
 # Eigenvectors and eigenvalues

diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Count.lean
@@ -5,9 +5,9 @@ Authors: Floris van Doorn
 -/
 module
 
-public import Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
 
 import Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
+public import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 
 /-!
 # `L^p`-seminorms on `count` and `dirac`

diff --git a/Mathlib/MeasureTheory/Integral/MeanInequalities.lean b/Mathlib/MeasureTheory/Integral/MeanInequalities.lean
@@ -8,9 +8,9 @@ module
 public import Mathlib.Analysis.MeanInequalities
 public import Mathlib.Analysis.MeanInequalitiesPow
 public import Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
-public import Mathlib.MeasureTheory.Integral.Lebesgue.Add
 
 import Mathlib.MeasureTheory.Integral.Lebesgue.Markov
+public import Mathlib.MeasureTheory.Integral.Lebesgue.Basic
 
 /-!
 # Mean value inequalities for integrals

diff --git a/Mathlib/NumberTheory/Niven.lean b/Mathlib/NumberTheory/Niven.lean
@@ -9,7 +9,6 @@ public import Mathlib.Analysis.Complex.IsIntegral
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 public import Mathlib.RingTheory.Polynomial.RationalRoot
 public import Mathlib.NumberTheory.Real.Irrational
-public import Mathlib.Tactic.Peel
 public import Mathlib.Tactic.Rify
 public import Mathlib.Tactic.Qify
 

diff --git a/Mathlib/NumberTheory/Padics/PadicNumbers.lean b/Mathlib/NumberTheory/Padics/PadicNumbers.lean
@@ -9,7 +9,6 @@ public import Mathlib.RingTheory.Valuation.Basic
 public import Mathlib.NumberTheory.Padics.PadicNorm
 public import Mathlib.Analysis.Normed.Field.Lemmas
 public import Mathlib.Tactic.CrossRefAttribute
-public import Mathlib.Tactic.Peel
 public import Mathlib.Topology.MetricSpace.Ultra.Basic
 
 /-!

diff --git a/Mathlib/Probability/Independence/Kernel/Indep.lean b/Mathlib/Probability/Independence/Kernel/Indep.lean
@@ -6,7 +6,6 @@ Authors: Rémy Degenne
 module
 
 public import Mathlib.Probability.Kernel.Basic
-public import Mathlib.Tactic.Peel
 public import Mathlib.Analysis.Normed.Group.Basic
 
 /-!

diff --git a/Mathlib/Tactic/CongrExclamation.lean b/Mathlib/Tactic/CongrExclamation.lean
@@ -10,9 +10,9 @@ public meta import Lean.Elab.Tactic.RCases
 public meta import Lean.Meta.Tactic.Assumption
 
 public import Mathlib.Lean.Meta.CongrTheorems
-public import Mathlib.Tactic.Relation.Rfl
 public import Lean.Elab.ConfigEval
 public import Mathlib.Basic.Logic.Basic
+public meta import Lean.Meta.Tactic.Rfl
 
 /-!
 # The `congr!` tactic

diff --git a/Mathlib/Tactic/GCongr/Core.lean b/Mathlib/Tactic/GCongr/Core.lean
@@ -13,6 +13,7 @@ public import Mathlib.Order.Defs.Unbundled
 public import Mathlib.Tactic.Core
 public import Mathlib.Tactic.GCongr.ForwardAttr
 public meta import Mathlib.Tactic.GCongr.ForwardAttr
+public import Lean.Elab.Tactic.RCases
 
 /-!
 # The `gcongr` ("generalized congruence") tactic

diff --git a/Mathlib/Tactic/GCongr/CoreAttrs.lean b/Mathlib/Tactic/GCongr/CoreAttrs.lean
@@ -5,6 +5,6 @@ Authors: Yury Kudryashov, Jovan Gerbscheid
 -/
 module
 
-public import Mathlib.Tactic.GCongr.Core
+public import Mathlib.Init
 
 deprecated_module "use Mathlib.Tactic.GCongr instead" (since := "2026-09-09")
diff --git a/Mathlib/Tactic/GRewrite.lean b/Mathlib/Tactic/GRewrite.lean
@@ -5,8 +5,8 @@ Authors: Sebastian Zimmer, Mario Carneiro, Heather Macbeth, Jovan Gerbscheid
 -/
 module
 
-public import Mathlib.Tactic.GCongr
 public import Mathlib.Tactic.GRewrite.Elab
+public import Mathlib.Tactic.Basic
 
 /-!
 

diff --git a/Mathlib/Tactic/GRewrite/Core.lean b/Mathlib/Tactic/GRewrite/Core.lean
@@ -9,6 +9,7 @@ public meta import Lean.Meta.Tactic.Rewrite
 public import Mathlib.Tactic.GCongr.Core
 public import Lean.Meta.Tactic.Rewrite
 meta import Mathlib.Tactic.GCongr.Core
+public meta import Mathlib.Tactic.GCongr.Core
 
 /-!
 # The generalized rewriting tactic

diff --git a/Mathlib/Tactic/Inclusion/Core/Core.lean b/Mathlib/Tactic/Inclusion/Core/Core.lean
@@ -5,8 +5,9 @@ Authors: David Ledvinka
 -/
 module
 
-public meta import Mathlib.Tactic.Inclusion.Core.Inclusion
 public meta import Lean.Meta.Native
+public import Mathlib.Tactic.Inclusion.Core.Inclusion
+public meta import Mathlib.Tactic.Inclusion.Core.ToSet
 
 /-!
 # Core implementation of the `inclusion` tactic

diff --git a/Mathlib/Tactic/Inclusion/Core/DiscrTreeExt.lean b/Mathlib/Tactic/Inclusion/Core/DiscrTreeExt.lean
@@ -6,7 +6,6 @@ Authors: David Ledvinka
 module
 
 public import Mathlib.Init
-public meta import Lean.Meta.DiscrTree
 
 /-!
 # Discrimination-tree-indexed environment extensions

diff --git a/Mathlib/Tactic/Inclusion/Core/Elab.lean b/Mathlib/Tactic/Inclusion/Core/Elab.lean
@@ -6,6 +6,7 @@ Authors: David Ledvinka
 module
 
 public meta import Mathlib.Tactic.Inclusion.Core.Core
+public import Mathlib.Tactic.Inclusion.Core.Core
 
 /-!
 # The `inclusion` tactic

diff --git a/Mathlib/Tactic/Inclusion/Core/Expr.lean b/Mathlib/Tactic/Inclusion/Core/Expr.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Tactic.Inclusion.Core.ToSet
 public meta import Mathlib.Tactic.Inclusion.Core.Types
+public import Mathlib.Tactic.Inclusion.Core.Types
 
 /-!
 # Expr helpers for the `inclusion` tactic

diff --git a/Mathlib/Tactic/Inclusion/Core/Extensions.lean b/Mathlib/Tactic/Inclusion/Core/Extensions.lean
@@ -5,8 +5,8 @@ Authors: David Ledvinka
 -/
 module
 
-public meta import Mathlib.Tactic.Inclusion.Core.DiscrTreeExt
-public meta import Mathlib.Tactic.Inclusion.Core.Types
+public import Mathlib.Tactic.Inclusion.Core.DiscrTreeExt
+public import Mathlib.Tactic.Inclusion.Core.Types
 
 /-!
 # Environment extensions for the `inclusion` tactic

diff --git a/Mathlib/Tactic/Inclusion/Core/Inclusion.lean b/Mathlib/Tactic/Inclusion/Core/Inclusion.lean
@@ -5,8 +5,13 @@ Authors: David Ledvinka
 -/
 module
 
-public meta import Mathlib.Tactic.Inclusion.Core.Expr
 public meta import Mathlib.Tactic.Inclusion.Core.Extensions
+public meta import Aesop
+public meta import Mathlib.Tactic.Basic
+public import Mathlib.Tactic.Inclusion.Core.Expr
+public import Mathlib.Tactic.Inclusion.Core.Extensions
+public meta import Mathlib.Tactic.Simps
+public meta import Mathlib.Tactic.ToDual
 
 /-!
 # Constructing inclusions

diff --git a/Mathlib/Tactic/Inclusion/Extension/Core/Core.lean b/Mathlib/Tactic/Inclusion/Extension/Core/Core.lean
@@ -5,8 +5,8 @@ Authors: David Ledvinka
 -/
 module
 
-public meta import Mathlib.Tactic.Inclusion.Extension.Core.Init
-public meta import Mathlib.Tactic.Inclusion.ExtensionAPI.Attr
+public meta import Mathlib.Tactic.Inclusion.Extension.Core.Init  -- shake: keep (registers `core`)
+public import Mathlib.Tactic.Inclusion.ExtensionAPI.Attr
 
 /-!
 # Core extensions for the `inclusion` tactic

diff --git a/Mathlib/Tactic/Inclusion/Extension/Core/Init.lean b/Mathlib/Tactic/Inclusion/Extension/Core/Init.lean
@@ -5,7 +5,7 @@ Authors: David Ledvinka
 -/
 module
 
-public meta import Mathlib.Tactic.Inclusion.Core.Extensions
+public import Mathlib.Tactic.Inclusion.Core.Extensions
 
 /-!
 # Core extension family for the `inclusion` tactic

diff --git a/Mathlib/Tactic/Inclusion/Extension/IntervalDyadicReal/BinarySplit.lean b/Mathlib/Tactic/Inclusion/Extension/IntervalDyadicReal/BinarySplit.lean
@@ -6,7 +6,7 @@ Authors: David Ledvinka
 module
 
 public import Mathlib.Tactic.Inclusion.Extension.IntervalDyadicReal.Init
-public meta import Mathlib.Tactic.Inclusion.ExtensionAPI.Attr
+public import Mathlib.Tactic.Inclusion.ExtensionAPI.Attr
 
 /-!
 # Binary splitting of dyadic real intervals

diff --git a/Mathlib/Tactic/Inclusion/Extension/IntervalDyadicReal/Hypotheses.lean b/Mathlib/Tactic/Inclusion/Extension/IntervalDyadicReal/Hypotheses.lean
@@ -5,8 +5,8 @@ Authors: David Ledvinka
 -/
 module
 
-public meta import Mathlib.Tactic.Inclusion.ExtensionAPI.Attr
 public import Mathlib.Tactic.Inclusion.Extension.IntervalDyadicReal.Init
+public import Mathlib.Tactic.Inclusion.ExtensionAPI.Attr
 
 /-!
 # Hypothesis operations for dyadic real intervals

diff --git a/Mathlib/Tactic/Inclusion/Extension/IntervalDyadicReal/Init.lean b/Mathlib/Tactic/Inclusion/Extension/IntervalDyadicReal/Init.lean
@@ -6,8 +6,8 @@ Authors: David Ledvinka
 module
 
 public import Mathlib.Data.Dyadic
-public meta import Mathlib.Tactic.Inclusion.Core.Extensions
 public import Mathlib.Tactic.Inclusion.Extension.Interval
+public import Mathlib.Tactic.Inclusion.Core.Extensions
 
 /-!
 # Initialization for the dyadic real interval extension family

diff --git a/Mathlib/Tactic/Inclusion/Extension/IntervalDyadicReal/Tactic.lean b/Mathlib/Tactic/Inclusion/Extension/IntervalDyadicReal/Tactic.lean
@@ -5,10 +5,11 @@ Authors: David Ledvinka
 -/
 module
 
-public meta import Mathlib.Tactic.Inclusion.Core.Elab
-public meta import Mathlib.Tactic.Inclusion.Extension.Core.Core
-public import Mathlib.Tactic.Inclusion.Extension.IntervalDyadicReal.Rational
-public meta import Mathlib.Tactic.Inclusion.Extension.IntervalDyadicReal.Hypotheses
+public import Mathlib.Algebra.Order.AbsoluteValue.Basic
+public import Mathlib.Algebra.Order.Field.Basic
+public import Mathlib.Data.Rat.Cast.Order
+public import Mathlib.Tactic.Inclusion.Core.Elab
+public meta import Mathlib.Tactic.ToAdditive
 
 /-!
 # The `dyadic_interval` tactic

diff --git a/Mathlib/Tactic/Inclusion/ExtensionAPI/Attr.lean b/Mathlib/Tactic/Inclusion/ExtensionAPI/Attr.lean
@@ -5,7 +5,7 @@ Authors: David Ledvinka
 -/
 module
 
-public meta import Mathlib.Tactic.Inclusion.ExtensionAPI.Basic
+public import Mathlib.Tactic.Inclusion.ExtensionAPI.Basic
 
 /-!
 # Attributes for `inclusion` extensions

diff --git a/Mathlib/Tactic/Inclusion/ExtensionAPI/Basic.lean b/Mathlib/Tactic/Inclusion/ExtensionAPI/Basic.lean
@@ -6,7 +6,7 @@ Authors: David Ledvinka
 module
 
 public meta import Mathlib.Lean.Meta.Basic
-public meta import Mathlib.Tactic.Inclusion.Core.Inclusion
+public import Mathlib.Tactic.Inclusion.Core.Inclusion
 
 /-!
 # Basic API for `inclusion` extensions

diff --git a/Mathlib/Testing/Plausible/Sampleable.lean b/Mathlib/Testing/Plausible/Sampleable.lean
@@ -13,6 +13,7 @@ public import Plausible.Arbitrary
 public import Plausible.Gen
 public import Plausible.Random
 public meta import Plausible.Sampleable
+public import Mathlib.Tactic.Basic
 
 /-!
 This module contains `Plausible.Shrinkable` and `Plausible.SampleableExt` instances for mathlib

diff --git a/Mathlib/Topology/CantorBendixson.lean b/Mathlib/Topology/CantorBendixson.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.SetTheory.Ordinal.FixedPointApproximants
 public import Mathlib.Topology.DerivedSet
+public meta import Mathlib.Tactic.ToAdditive
 
 /-!
 # Cantor-Bendixson derivatives and perfect kernel

diff --git a/Mathlib/Topology/Compactness/NhdsKer.lean b/Mathlib/Topology/Compactness/NhdsKer.lean
@@ -5,7 +5,6 @@ Authors: Yury Kudryashov
 -/
 module
 
-public import Mathlib.Tactic.Peel
 public import Mathlib.Topology.Compactness.Compact
 public import Mathlib.Topology.NhdsKer
 

diff --git a/Mathlib/Topology/DerivedSet.lean b/Mathlib/Topology/DerivedSet.lean
@@ -6,7 +6,6 @@ Authors: Daniel Weber
 module
 
 public import Mathlib.Topology.Perfect
-public import Mathlib.Tactic.Peel
 
 /-!
 # Derived set
-Original file line number
+Diff line change
@@ Expand Up / @@ -5,7 +5,6 @@ Authors: Jireh Loreaux @@
     -/
     module
-    public import Mathlib.Tactic.Peel
     public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
     public import Mathlib.Analysis.Complex.Basic
@@ Expand Down @@