diff --git a/Mathlib/Algebra/Group/Equiv/TypeTags.lean b/Mathlib/Algebra/Group/Equiv/TypeTags.lean
index 1e78d7eb404c09..cbdf567ff9460a 100644
--- 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
index 108bf1c486d92d..072a9e2bd6abc8 100644
--- 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
index 65afc647df0f71..d09bb47837ea60 100644
--- 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
index 8dbd1d7363a361..6183607b1e601d 100644
--- 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
index 4326a7841cbedb..061b3afe7dcc3e 100644
--- 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
index c7556abb9e2a6a..2c4849dd7db475 100644
--- 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
index df7c0eacc14bcc..31b39cc88ccb62 100644
--- 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
index bcb41e23e09dcd..1b19a4be0d175a 100644
--- 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
index b05fb5482a5dc0..aa596068908e68 100644
--- 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
index be9a842dfed55f..495314a6aaa8da 100644
--- 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
index c544a39e135f77..2d5c8cb83623ec 100644
--- 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
index 6e0e55b225761c..d7cb077d85b404 100644
--- 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
index 4b6d7d4714dcdf..522f6a1dfb8f83 100644
--- 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
index c86c5366a44953..7e5d645a60e0b1 100644
--- 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
index de4180f04893b0..c674a5d9c62ee8 100644
--- 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
index 8ebb171e0fe17b..186216745a3c94 100644
--- 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
index 299ef742319505..489d58ea52b72a 100644
--- 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
index 99d1fb87681de3..ab8a94a3600285 100644
--- 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
index 79040472922216..a8599318fd3c84 100644
--- 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
index f19b3e05dd76e6..2518fdeb03657e 100644
--- 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
index 0e4a2625c94084..d482581bd2e69f 100644
--- 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
index d699139254f5b9..7b7d1de86cf8f0 100644
--- 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
index 1cdcec671064c7..2010f3bcd3f2b1 100644
--- 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
index 60382f589406c0..ea952326bf85de 100644
--- 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
index ab49a281dea040..978b543af04ab3 100644
--- 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
index 2788a5bdab7abb..23dc38a0baf643 100644
--- 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
index e34f5f072bd6df..6f9494654d6624 100644
--- 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
index 43cc5a6ca83bf2..aa66a935624330 100644
--- 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
index 016c942f92f7ef..04c82ba915e227 100644
--- 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
index c623cb15ab9044..906c83cc2ba427 100644
--- 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
index cb1fc0135b9905..12a3a68f662820 100644
--- 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
index 3d77935764feb3..f209c00259f2e1 100644
--- 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
index 386d60f3676aa9..313b5d4e3c989a 100644
--- 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
index 23e53162d808c7..e02c5609ebd073 100644
--- 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
index e204ee15ea99aa..834c65a0668008 100644
--- 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
index 8b069a7237dfb6..ba3e2595244faf 100644
--- 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
index 712818418e7822..35a899d32cc3f8 100644
--- 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
index cc33b7cd9a758e..df273bf85c8a3c 100644
--- 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
index ab27c7bc76c79d..e46d94cc9c06ea 100644
--- 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
index e2107e53b132b8..b9fb68a74313ff 100644
--- 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
index 4585fb62d56d9a..f0305593d18593 100644
--- 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
index 462ffd61abad46..e8daa23bbb78ad 100644
--- 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
index c63ceacb3acdc0..901158be498e0f 100644
--- 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
diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean
index c5394dffe84e46..c8c354222288a5 100644
--- a/Mathlib/Topology/LocallyFinsupp.lean
+++ b/Mathlib/Topology/LocallyFinsupp.lean
@@ -14,7 +14,6 @@ public import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
 public import Mathlib.Algebra.Order.Pi
 public import Mathlib.Topology.DiscreteSubset
 public import Mathlib.Topology.Separation.Hausdorff
-public import Mathlib.Tactic.Peel
 
 /-!
 # Type of functions with locally finite support
diff --git a/Mathlib/Topology/Order/Cadlag.lean b/Mathlib/Topology/Order/Cadlag.lean
index d3f552481ca7c0..df36a97a2dbac1 100644
--- a/Mathlib/Topology/Order/Cadlag.lean
+++ b/Mathlib/Topology/Order/Cadlag.lean
@@ -5,8 +5,11 @@ Authors: Rémy Degenne, Nick Kuhn, Yongxi Lin, Rohit Manokaran, Etienne Marion,
 -/
 module
 
-public import Mathlib.Analysis.Normed.Group.Continuity
 public import Mathlib.Topology.Order.LeftRightLim
+public import Mathlib.Analysis.Normed.Group.Basic
+public import Mathlib.Data.EReal.Operations
+public import Mathlib.Topology.Algebra.InfiniteSum.Order
+public import Mathlib.Topology.MetricSpace.Bounded
 
 /-! # Càdlàg functions
 
diff --git a/Mathlib/Topology/UniformSpace/Cauchy.lean b/Mathlib/Topology/UniformSpace/Cauchy.lean
index 86640c96b74c3a..a8607a0f824838 100644
--- a/Mathlib/Topology/UniformSpace/Cauchy.lean
+++ b/Mathlib/Topology/UniformSpace/Cauchy.lean
@@ -6,10 +6,10 @@ Authors: Johannes Hölzl, Mario Carneiro
 module
 
 public import Mathlib.Tactic.CrossRefAttribute
-public import Mathlib.Topology.Algebra.Constructions
 public import Mathlib.Topology.Bases
 public import Mathlib.Algebra.Order.Group.Nat
 public import Mathlib.Topology.UniformSpace.DiscreteUniformity
+public import Mathlib.Topology.Compactness.Compact
 
 /-!
 # Theory of Cauchy filters in uniform spaces. Complete uniform spaces. Totally bounded subsets.
diff --git a/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean b/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean
index 8e16641fb31d32..2c4fef855c14be 100644
--- a/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean
+++ b/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean
@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel
 module
 
 public import Mathlib.Topology.UniformSpace.UniformConvergence
+public import Mathlib.Topology.Separation.Hausdorff
 
 /-!
 # Locally uniform convergence
diff --git a/Mathlib/Topology/UniformSpace/UniformConvergence.lean b/Mathlib/Topology/UniformSpace/UniformConvergence.lean
index c211454482223c..64f738d468e7c6 100644
--- a/Mathlib/Topology/UniformSpace/UniformConvergence.lean
+++ b/Mathlib/Topology/UniformSpace/UniformConvergence.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Topology.UniformSpace.Cauchy
+public import Mathlib.Topology.Inseparable
 
 /-!
 # Uniform convergence