diff --git a/Mathlib/Algebra/AddConstMap/Basic.lean b/Mathlib/Algebra/AddConstMap/Basic.lean
index 9bed6eb4e7ecd..9a4bbb7a01085 100644
--- a/Mathlib/Algebra/AddConstMap/Basic.lean
+++ b/Mathlib/Algebra/AddConstMap/Basic.lean
@@ -9,6 +9,7 @@ import Mathlib.Algebra.Module.Defs
 import Mathlib.Algebra.Order.Archimedean.Basic
 import Mathlib.Algebra.Order.Group.Instances
 import Mathlib.Logic.Function.Iterate
+import Mathlib.Tactic.WLOG
 
 /-!
 # Maps (semi)conjugating a shift to a shift
diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean
index 33329a6e81269..180e41ca8fe55 100644
--- a/Mathlib/Algebra/BigOperators/Finprod.lean
+++ b/Mathlib/Algebra/BigOperators/Finprod.lean
@@ -9,6 +9,7 @@ import Mathlib.Algebra.NoZeroSMulDivisors.Basic
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Data.Set.Subsingleton
+import Mathlib.Tactic.IrreducibleDef
 
 /-!
 # Finite products and sums over types and sets
diff --git a/Mathlib/Algebra/CharP/Basic.lean b/Mathlib/Algebra/CharP/Basic.lean
index bb0db6f85c58a..8be5c8727afce 100644
--- a/Mathlib/Algebra/CharP/Basic.lean
+++ b/Mathlib/Algebra/CharP/Basic.lean
@@ -12,8 +12,9 @@ import Mathlib.Data.Nat.Cast.Prod
 import Mathlib.Data.Nat.Find
 import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.Data.ULift
-import Mathlib.Tactic.NormNum.Basic
 import Mathlib.Order.Interval.Set.Basic
+import Mathlib.Tactic.TermCongr
+import Mathlib.Tactic.NormNum.Basic
 
 /-!
 # Characteristic of semirings
diff --git a/Mathlib/Algebra/CharP/Defs.lean b/Mathlib/Algebra/CharP/Defs.lean
index 9c41f5a2b3741..0fb3ede762cd6 100644
--- a/Mathlib/Algebra/CharP/Defs.lean
+++ b/Mathlib/Algebra/CharP/Defs.lean
@@ -8,6 +8,7 @@ import Mathlib.Data.Nat.Cast.Defs
 import Mathlib.Data.Nat.Find
 import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.Tactic.NormNum.Basic
+import Mathlib.Tactic.WLOG
 
 /-!
 # Characteristic of semirings
diff --git a/Mathlib/Algebra/ContinuedFractions/Basic.lean b/Mathlib/Algebra/ContinuedFractions/Basic.lean
index 6a34dbcebe789..6a54fd3bca107 100644
--- a/Mathlib/Algebra/ContinuedFractions/Basic.lean
+++ b/Mathlib/Algebra/ContinuedFractions/Basic.lean
@@ -3,8 +3,9 @@ Copyright (c) 2019 Kevin Kappelmann. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 -/
-import Mathlib.Data.Seq.Seq
 import Mathlib.Algebra.Field.Defs
+import Mathlib.Data.Seq.Seq
+import Mathlib.Tactic.Coe
 
 /-!
 # Basic Definitions/Theorems for Continued Fractions
diff --git a/Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean b/Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
index fa5e59f20d0ad..a3268105424cc 100644
--- a/Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
+++ b/Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
 import Mathlib.Algebra.ContinuedFractions.TerminatedStable
 import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Set
 import Mathlib.Tactic.Ring
 
 /-!
diff --git a/Mathlib/Algebra/ContinuedFractions/Determinant.lean b/Mathlib/Algebra/ContinuedFractions/Determinant.lean
index fc47ab611ad63..b74116407b703 100644
--- a/Mathlib/Algebra/ContinuedFractions/Determinant.lean
+++ b/Mathlib/Algebra/ContinuedFractions/Determinant.lean
@@ -6,6 +6,7 @@ Authors: Kevin Kappelmann
 import Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
 import Mathlib.Algebra.ContinuedFractions.TerminatedStable
 import Mathlib.Tactic.Ring
+import Mathlib.Tactic.Set
 
 /-!
 # Determinant Formula for Simple Continued Fraction
diff --git a/Mathlib/Algebra/Divisibility/Basic.lean b/Mathlib/Algebra/Divisibility/Basic.lean
index 7e62a5bd031dc..c5c63d33fcdce 100644
--- a/Mathlib/Algebra/Divisibility/Basic.lean
+++ b/Mathlib/Algebra/Divisibility/Basic.lean
@@ -6,7 +6,7 @@ Neil Strickland, Aaron Anderson
 -/
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Hom.Defs
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.Use
 
 /-!
 # Divisibility
diff --git a/Mathlib/Algebra/Divisibility/Prod.lean b/Mathlib/Algebra/Divisibility/Prod.lean
index 355b2cfd6033d..a68aafac49275 100644
--- a/Mathlib/Algebra/Divisibility/Prod.lean
+++ b/Mathlib/Algebra/Divisibility/Prod.lean
@@ -5,7 +5,7 @@ Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Group.Prod
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.Choose
 
 /-!
 # Lemmas about the divisibility relation in product (semi)groups
diff --git a/Mathlib/Algebra/Field/IsField.lean b/Mathlib/Algebra/Field/IsField.lean
index e9b67d20db248..abaf404ab50f3 100644
--- a/Mathlib/Algebra/Field/IsField.lean
+++ b/Mathlib/Algebra/Field/IsField.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Field.Defs
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.Convert
 
 /-!
 # `IsField` predicate
diff --git a/Mathlib/Algebra/GCDMonoid/Basic.lean b/Mathlib/Algebra/GCDMonoid/Basic.lean
index 1eb6be1251a77..a560692b8f2e8 100644
--- a/Mathlib/Algebra/GCDMonoid/Basic.lean
+++ b/Mathlib/Algebra/GCDMonoid/Basic.lean
@@ -5,6 +5,8 @@ Authors: Johannes Hölzl, Jens Wagemaker
 -/
 import Mathlib.Algebra.Associated.Basic
 import Mathlib.Algebra.Ring.Regular
+import Mathlib.Tactic.DefEqTransformations
+import Mathlib.Tactic.Set
 
 /-!
 # Monoids with normalization functions, `gcd`, and `lcm`
diff --git a/Mathlib/Algebra/Group/Int.lean b/Mathlib/Algebra/Group/Int.lean
index d0d47342d4add..c9867785c4b61 100644
--- a/Mathlib/Algebra/Group/Int.lean
+++ b/Mathlib/Algebra/Group/Int.lean
@@ -6,6 +6,8 @@ Authors: Jeremy Avigad
 import Mathlib.Algebra.Group.Nat
 import Mathlib.Algebra.Group.Units.Basic
 import Mathlib.Data.Int.Sqrt
+import Mathlib.Tactic.Cases
+import Mathlib.Tactic.Tauto
 
 /-!
 # The integers form a group
diff --git a/Mathlib/Algebra/Group/Subgroup/Defs.lean b/Mathlib/Algebra/Group/Subgroup/Defs.lean
index 2bbdaa180486f..4b48a8f2f61c7 100644
--- a/Mathlib/Algebra/Group/Subgroup/Defs.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Defs.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kexing Ying
 -/
 import Mathlib.Algebra.Group.Submonoid.Defs
-import Mathlib.Tactic.Common
 
 /-!
 # Subgroups
diff --git a/Mathlib/Algebra/Group/WithOne/Defs.lean b/Mathlib/Algebra/Group/WithOne/Defs.lean
index 39ed722267c5d..6772577b77473 100644
--- a/Mathlib/Algebra/Group/WithOne/Defs.lean
+++ b/Mathlib/Algebra/Group/WithOne/Defs.lean
@@ -6,7 +6,10 @@ Authors: Mario Carneiro, Johan Commelin
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Data.Option.Defs
 import Mathlib.Logic.Nontrivial.Basic
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.Coe
+import Mathlib.Tactic.Lift
+import Mathlib.Tactic.SimpRw
+import Mathlib.Tactic.Spread
 
 /-!
 # Adjoining a zero/one to semigroups and related algebraic structures
diff --git a/Mathlib/Algebra/GroupPower/IterateHom.lean b/Mathlib/Algebra/GroupPower/IterateHom.lean
index 50ac0d58a372a..8d1f831f60e7b 100644
--- a/Mathlib/Algebra/GroupPower/IterateHom.lean
+++ b/Mathlib/Algebra/GroupPower/IterateHom.lean
@@ -7,7 +7,7 @@ import Mathlib.Algebra.Group.Action.Opposite
 import Mathlib.Algebra.Group.Int
 import Mathlib.Algebra.Group.Nat
 import Mathlib.Logic.Function.Iterate
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.DefEqTransformations
 
 /-!
 # Iterates of monoid homomorphisms
diff --git a/Mathlib/Algebra/GroupWithZero/Action/Pi.lean b/Mathlib/Algebra/GroupWithZero/Action/Pi.lean
index f465f4b4caa56..497cbbedbd1c5 100644
--- a/Mathlib/Algebra/GroupWithZero/Action/Pi.lean
+++ b/Mathlib/Algebra/GroupWithZero/Action/Pi.lean
@@ -6,7 +6,6 @@ Authors: Simon Hudon, Patrick Massot
 import Mathlib.Algebra.Group.Action.Pi
 import Mathlib.Algebra.GroupWithZero.Action.Defs
 import Mathlib.Algebra.GroupWithZero.Defs
-import Mathlib.Tactic.Common
 
 /-!
 # Pi instances for multiplicative actions with zero
diff --git a/Mathlib/Algebra/Homology/LocalCohomology.lean b/Mathlib/Algebra/Homology/LocalCohomology.lean
index f8d4b17460856..372da9aa5fffc 100644
--- a/Mathlib/Algebra/Homology/LocalCohomology.lean
+++ b/Mathlib/Algebra/Homology/LocalCohomology.lean
@@ -3,13 +3,14 @@ Copyright (c) 2023 Emily Witt. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Emily Witt, Kim Morrison, Jake Levinson, Sam van Gool
 -/
-import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.Algebra.Category.ModuleCat.Colimits
 import Mathlib.Algebra.Category.ModuleCat.Projective
 import Mathlib.CategoryTheory.Abelian.Ext
-import Mathlib.RingTheory.Finiteness
 import Mathlib.CategoryTheory.Limits.Final
+import Mathlib.RingTheory.Finiteness
+import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.RingTheory.Noetherian
+import Mathlib.Tactic.ApplyWith
 
 /-!
 # Local cohomology.
diff --git a/Mathlib/Algebra/Module/Defs.lean b/Mathlib/Algebra/Module/Defs.lean
index 394dd7a778e54..9f62d433ee1cf 100644
--- a/Mathlib/Algebra/Module/Defs.lean
+++ b/Mathlib/Algebra/Module/Defs.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.GroupWithZero.Action.End
 import Mathlib.Algebra.GroupWithZero.Action.Units
 import Mathlib.Algebra.SMulWithZero
 import Mathlib.Data.Int.Cast.Lemmas
+import Mathlib.Tactic.NthRewrite
 
 /-!
 # Modules over a ring
diff --git a/Mathlib/Algebra/Order/Archimedean/Hom.lean b/Mathlib/Algebra/Order/Archimedean/Hom.lean
index c4e7b11c89739..9340044369edb 100644
--- a/Mathlib/Algebra/Order/Archimedean/Hom.lean
+++ b/Mathlib/Algebra/Order/Archimedean/Hom.lean
@@ -5,6 +5,7 @@ Authors: Alex J. Best, Yaël Dillies
 -/
 import Mathlib.Algebra.Order.Archimedean.Basic
 import Mathlib.Algebra.Order.Hom.Ring
+import Mathlib.Tactic.WLOG
 
 /-!
 ### Uniqueness of ring homomorphisms to archimedean fields.
diff --git a/Mathlib/Algebra/Order/CauSeq/Basic.lean b/Mathlib/Algebra/Order/CauSeq/Basic.lean
index 380eb60f96e79..3abe2edd463ef 100644
--- a/Mathlib/Algebra/Order/CauSeq/Basic.lean
+++ b/Mathlib/Algebra/Order/CauSeq/Basic.lean
@@ -11,6 +11,7 @@ import Mathlib.Algebra.Ring.Pi
 import Mathlib.Data.Setoid.Basic
 import Mathlib.GroupTheory.GroupAction.Ring
 import Mathlib.Tactic.GCongr
+import Mathlib.Tactic.Set
 
 /-!
 # Cauchy sequences
diff --git a/Mathlib/Algebra/Order/GroupWithZero/Action/Synonym.lean b/Mathlib/Algebra/Order/GroupWithZero/Action/Synonym.lean
index bd2d126a778f8..cfc4ed69ed2ed 100644
--- a/Mathlib/Algebra/Order/GroupWithZero/Action/Synonym.lean
+++ b/Mathlib/Algebra/Order/GroupWithZero/Action/Synonym.lean
@@ -5,7 +5,6 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.Order.GroupWithZero.Synonym
 import Mathlib.Algebra.SMulWithZero
-import Mathlib.Tactic.Common
 
 /-!
 # Actions by and on order synonyms
diff --git a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
index 798ea261934d2..e1cf863300bf8 100644
--- a/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
+++ b/Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
@@ -13,6 +13,8 @@ import Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import Mathlib.Algebra.Order.Monoid.Basic
 import Mathlib.Algebra.Order.Monoid.OrderDual
 import Mathlib.Algebra.Order.Monoid.TypeTags
+import Mathlib.Tactic.ByContra
+import Mathlib.Tactic.Cases
 
 /-!
 # Linearly ordered commutative groups and monoids with a zero element adjoined
diff --git a/Mathlib/Algebra/Prime/Defs.lean b/Mathlib/Algebra/Prime/Defs.lean
index 90165b72d0050..90bed3c2a3318 100644
--- a/Mathlib/Algebra/Prime/Defs.lean
+++ b/Mathlib/Algebra/Prime/Defs.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jens Wagemaker
 -/
 import Mathlib.Algebra.GroupWithZero.Divisibility
+import Mathlib.Tactic.Says
 
 /-!
 # Prime and irreducible elements.
diff --git a/Mathlib/Algebra/Quotient.lean b/Mathlib/Algebra/Quotient.lean
index ea7436110634b..29bd4c24ebcbf 100644
--- a/Mathlib/Algebra/Quotient.lean
+++ b/Mathlib/Algebra/Quotient.lean
@@ -3,7 +3,6 @@ Copyright (c) 2021 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
-import Mathlib.Tactic.Common
 
 /-!
 # Algebraic quotients
diff --git a/Mathlib/Algebra/Ring/Parity.lean b/Mathlib/Algebra/Ring/Parity.lean
index 72fdec393def4..f721cf50e9211 100644
--- a/Mathlib/Algebra/Ring/Parity.lean
+++ b/Mathlib/Algebra/Ring/Parity.lean
@@ -7,6 +7,7 @@ import Mathlib.Data.Nat.Cast.Basic
 import Mathlib.Data.Nat.Cast.Commute
 import Mathlib.Data.Set.Operations
 import Mathlib.Logic.Function.Iterate
+import Mathlib.Tactic.Cases
 
 /-!
 # Even and odd elements in rings
diff --git a/Mathlib/Algebra/Ring/Subring/Basic.lean b/Mathlib/Algebra/Ring/Subring/Basic.lean
index 35a508fb82fb3..59e2c25a530da 100644
--- a/Mathlib/Algebra/Ring/Subring/Basic.lean
+++ b/Mathlib/Algebra/Ring/Subring/Basic.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.Group.Subgroup.Basic
 import Mathlib.Algebra.Ring.Subsemiring.Basic
 import Mathlib.RingTheory.NonUnitalSubring.Basic
+import Mathlib.Tactic.RSuffices
 
 /-!
 # Subrings
diff --git a/Mathlib/Algebra/Ring/WithZero.lean b/Mathlib/Algebra/Ring/WithZero.lean
index 6c68ee84556bc..6e906d512cb8f 100644
--- a/Mathlib/Algebra/Ring/WithZero.lean
+++ b/Mathlib/Algebra/Ring/WithZero.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Johan Commelin
 -/
 import Mathlib.Algebra.GroupWithZero.WithZero
 import Mathlib.Algebra.Ring.Defs
+import Mathlib.Tactic.Cases
 
 /-!
 # Adjoining a zero to a semiring
diff --git a/Mathlib/Algebra/RingQuot.lean b/Mathlib/Algebra/RingQuot.lean
index fb0556615bab7..99895882b14ae 100644
--- a/Mathlib/Algebra/RingQuot.lean
+++ b/Mathlib/Algebra/RingQuot.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Algebra.Hom
 import Mathlib.RingTheory.Congruence.Basic
 import Mathlib.RingTheory.Ideal.Quotient.Defs
 import Mathlib.RingTheory.Ideal.Span
+import Mathlib.Tactic.IrreducibleDef
 
 /-!
 # Quotients of non-commutative rings
diff --git a/Mathlib/Algebra/Star/SelfAdjoint.lean b/Mathlib/Algebra/Star/SelfAdjoint.lean
index f2e5c48eb5513..669147661090f 100644
--- a/Mathlib/Algebra/Star/SelfAdjoint.lean
+++ b/Mathlib/Algebra/Star/SelfAdjoint.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.Algebra.Module.Defs
 import Mathlib.Algebra.Star.Pi
 import Mathlib.Algebra.Star.Rat
+import Mathlib.Tactic.TermCongr
 
 /-!
 # Self-adjoint, skew-adjoint and normal elements of a star additive group
diff --git a/Mathlib/Analysis/Analytic/RadiusLiminf.lean b/Mathlib/Analysis/Analytic/RadiusLiminf.lean
index 6aefcab0e900e..c8e1e823c3a11 100644
--- a/Mathlib/Analysis/Analytic/RadiusLiminf.lean
+++ b/Mathlib/Analysis/Analytic/RadiusLiminf.lean
@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Analysis.Analytic.Basic
 import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
+import Mathlib.Tactic.InferParam
 
 /-!
 # Representation of `FormalMultilinearSeries.radius` as a `liminf`
diff --git a/Mathlib/Analysis/Convex/Combination.lean b/Mathlib/Analysis/Convex/Combination.lean
index 6fe599b4f51f7..dd9326458c738 100644
--- a/Mathlib/Analysis/Convex/Combination.lean
+++ b/Mathlib/Analysis/Convex/Combination.lean
@@ -6,6 +6,7 @@ Authors: Yury Kudryashov
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 import Mathlib.Analysis.Convex.Hull
 import Mathlib.LinearAlgebra.AffineSpace.Basis
+import Mathlib.Tactic.SimpIntro
 
 /-!
 # Convex combinations
diff --git a/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean b/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean
index 1473b0ef27413..3f5e7a520f1a1 100644
--- a/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean
+++ b/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean
@@ -3,10 +3,11 @@ Copyright (c) 2022 Jujian Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang, Kim Morrison
 -/
-import Mathlib.CategoryTheory.Preadditive.InjectiveResolution
 import Mathlib.Algebra.Homology.HomotopyCategory
+import Mathlib.CategoryTheory.Preadditive.InjectiveResolution
 import Mathlib.Data.Set.Subsingleton
 import Mathlib.Tactic.AdaptationNote
+import Mathlib.Tactic.IrreducibleDef
 
 /-!
 # Abelian categories with enough injectives have injective resolutions
diff --git a/Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean b/Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean
index b46ed6087d1b3..84c7ff72d226f 100644
--- a/Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean
+++ b/Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean
@@ -5,6 +5,7 @@ Authors: Markus Himmel, Kim Morrison, Jakob von Raumer, Joël Riou
 -/
 import Mathlib.CategoryTheory.Preadditive.ProjectiveResolution
 import Mathlib.Algebra.Homology.HomotopyCategory
+import Mathlib.Tactic.IrreducibleDef
 import Mathlib.Tactic.SuppressCompilation
 
 /-!
diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
index d314808670795..ddb1545cc4f8c 100644
--- a/Mathlib/CategoryTheory/Category/Basic.lean
+++ b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -6,7 +6,7 @@ Authors: Stephen Morgan, Kim Morrison, Johannes Hölzl, Reid Barton
 import Mathlib.CategoryTheory.Category.Init
 import Mathlib.Combinatorics.Quiver.Basic
 import Mathlib.Tactic.PPWithUniv
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.Convert
 import Mathlib.Tactic.StacksAttribute
 
 /-!
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
index 38882d4e9f448..f557af4051a62 100644
--- a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
+++ b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Johannes Hölzl, Reid Barton, Sean Leather, Yury Kudryashov
 -/
 import Mathlib.CategoryTheory.Types
+import Mathlib.Util.AssertExists
 
 /-!
 # Concrete categories
diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean
index 1d28f0410aa9e..56dfcbeef6c7f 100644
--- a/Mathlib/CategoryTheory/DiscreteCategory.lean
+++ b/Mathlib/CategoryTheory/DiscreteCategory.lean
@@ -6,6 +6,8 @@ Authors: Stephen Morgan, Kim Morrison, Floris van Doorn
 import Mathlib.CategoryTheory.EqToHom
 import Mathlib.CategoryTheory.Pi.Basic
 import Mathlib.Data.ULift
+import Mathlib.Tactic.CasesM
+import Mathlib.Tactic.FailIfNoProgress
 
 /-!
 # Discrete categories
diff --git a/Mathlib/CategoryTheory/EssentiallySmall.lean b/Mathlib/CategoryTheory/EssentiallySmall.lean
index d3d3eb2c323fb..96b3d10205c6a 100644
--- a/Mathlib/CategoryTheory/EssentiallySmall.lean
+++ b/Mathlib/CategoryTheory/EssentiallySmall.lean
@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Category.ULift
 import Mathlib.CategoryTheory.Skeletal
 import Mathlib.Logic.UnivLE
 import Mathlib.Logic.Small.Basic
+import Mathlib.Tactic.Constructor
 
 /-!
 # Essentially small categories.
diff --git a/Mathlib/CategoryTheory/Functor/FullyFaithful.lean b/Mathlib/CategoryTheory/Functor/FullyFaithful.lean
index 82f3de969be51..2ecfa0d840aa4 100644
--- a/Mathlib/CategoryTheory/Functor/FullyFaithful.lean
+++ b/Mathlib/CategoryTheory/Functor/FullyFaithful.lean
@@ -5,6 +5,7 @@ Authors: Kim Morrison
 -/
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.Logic.Equiv.Defs
+import Mathlib.Tactic.Cases
 
 /-!
 # Full and faithful functors
diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
index 4ea68229bb26b..c1c21956203c9 100644
--- a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
+++ b/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
@@ -6,6 +6,7 @@ Authors: Joël Riou
 import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
 import Mathlib.CategoryTheory.Limits.Shapes.Equivalence
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
+import Mathlib.Tactic.NthRewrite
 
 /-!
 # Kan extensions
diff --git a/Mathlib/CategoryTheory/GlueData.lean b/Mathlib/CategoryTheory/GlueData.lean
index 433fa5d3d835c..0534f8582d492 100644
--- a/Mathlib/CategoryTheory/GlueData.lean
+++ b/Mathlib/CategoryTheory/GlueData.lean
@@ -8,6 +8,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
 import Mathlib.CategoryTheory.Limits.Constructions.EpiMono
 import Mathlib.CategoryTheory.Limits.Preserves.Limits
 import Mathlib.CategoryTheory.Limits.Shapes.Types
+import Mathlib.Tactic.ApplyWith
 
 /-!
 # Gluing data
diff --git a/Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean b/Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
index 7b6b62d4ce4c8..a7acdc734708c 100644
--- a/Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
+++ b/Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
@@ -5,6 +5,7 @@ Authors: Rémi Bottinelli
 -/
 import Mathlib.CategoryTheory.Groupoid
 import Mathlib.CategoryTheory.PathCategory.Basic
+import Mathlib.Tactic.NthRewrite
 
 /-!
 # Free groupoid on a quiver
diff --git a/Mathlib/CategoryTheory/Limits/Final.lean b/Mathlib/CategoryTheory/Limits/Final.lean
index 2cd80eb36a4f4..0522201131db6 100644
--- a/Mathlib/CategoryTheory/Limits/Final.lean
+++ b/Mathlib/CategoryTheory/Limits/Final.lean
@@ -11,6 +11,7 @@ import Mathlib.CategoryTheory.Filtered.Basic
 import Mathlib.CategoryTheory.Limits.Yoneda
 import Mathlib.CategoryTheory.PUnit
 import Mathlib.CategoryTheory.Grothendieck
+import Mathlib.Tactic.RSuffices
 
 /-!
 # Final and initial functors
diff --git a/Mathlib/CategoryTheory/Limits/IsLimit.lean b/Mathlib/CategoryTheory/Limits/IsLimit.lean
index 663c41495a819..a217ebca5e3bb 100644
--- a/Mathlib/CategoryTheory/Limits/IsLimit.lean
+++ b/Mathlib/CategoryTheory/Limits/IsLimit.lean
@@ -6,6 +6,7 @@ Authors: Reid Barton, Mario Carneiro, Kim Morrison, Floris van Doorn
 import Mathlib.CategoryTheory.Adjunction.Basic
 import Mathlib.CategoryTheory.Limits.Cones
 import Batteries.Tactic.Congr
+import Mathlib.Tactic.Choose
 
 /-!
 # Limits and colimits
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean b/Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean
index 323fb438c4e70..02c1be006c317 100644
--- a/Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean
@@ -5,6 +5,7 @@ Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Limits.Opposites
 import Mathlib.CategoryTheory.Limits.Preserves.Finite
+import Mathlib.Tactic.ApplyWith
 
 /-!
 # Limit preservation properties of `Functor.op` and related constructions
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Countable.lean b/Mathlib/CategoryTheory/Limits/Shapes/Countable.lean
index a50342b46d933..533b5839806a3 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Countable.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Countable.lean
@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Limits.Final
 import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
 import Mathlib.CategoryTheory.Countable
 import Mathlib.Data.Countable.Defs
+import Mathlib.Tactic.ClearExclamation
 /-!
 # Countable limits and colimits
 
diff --git a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean
index 465d603552c31..71266699ea8de 100644
--- a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean
+++ b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 import Mathlib.CategoryTheory.Localization.CalculusOfFractions
+import Mathlib.Tactic.NthRewrite
 
 /-!
 # Lemmas on fractions
diff --git a/Mathlib/CategoryTheory/Monad/Comonadicity.lean b/Mathlib/CategoryTheory/Monad/Comonadicity.lean
index 2649f2cfb69b3..3487f2a7562f6 100644
--- a/Mathlib/CategoryTheory/Monad/Comonadicity.lean
+++ b/Mathlib/CategoryTheory/Monad/Comonadicity.lean
@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
 import Mathlib.CategoryTheory.Limits.Shapes.Reflexive
 import Mathlib.CategoryTheory.Monad.Equalizer
 import Mathlib.CategoryTheory.Monad.Limits
+import Mathlib.Tactic.ApplyWith
 
 /-!
 # Comonadicity theorems
diff --git a/Mathlib/CategoryTheory/Monad/Monadicity.lean b/Mathlib/CategoryTheory/Monad/Monadicity.lean
index 329b6f0907bb9..594a953c04b79 100644
--- a/Mathlib/CategoryTheory/Monad/Monadicity.lean
+++ b/Mathlib/CategoryTheory/Monad/Monadicity.lean
@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
 import Mathlib.CategoryTheory.Limits.Shapes.Reflexive
 import Mathlib.CategoryTheory.Monad.Coequalizer
 import Mathlib.CategoryTheory.Monad.Limits
+import Mathlib.Tactic.ApplyWith
 
 /-!
 # Monadicity theorems
diff --git a/Mathlib/CategoryTheory/Products/Basic.lean b/Mathlib/CategoryTheory/Products/Basic.lean
index 3abbf24a0925d..f3da86c00d62c 100644
--- a/Mathlib/CategoryTheory/Products/Basic.lean
+++ b/Mathlib/CategoryTheory/Products/Basic.lean
@@ -6,6 +6,7 @@ Authors: Stephen Morgan, Kim Morrison
 import Mathlib.CategoryTheory.Functor.Const
 import Mathlib.CategoryTheory.Opposites
 import Mathlib.Data.Prod.Basic
+import Mathlib.Tactic.Says
 
 /-!
 # Cartesian products of categories
diff --git a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
index 21ae0858e76d2..84f1fbb18c244 100644
--- a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
+++ b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
@@ -3,11 +3,12 @@ Copyright (c) 2021 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import Mathlib.CategoryTheory.Sites.Sheaf
+import Mathlib.CategoryTheory.Adjunction.FullyFaithful
 import Mathlib.CategoryTheory.Sites.CoverLifting
 import Mathlib.CategoryTheory.Sites.CoverPreserving
-import Mathlib.CategoryTheory.Adjunction.FullyFaithful
 import Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
+import Mathlib.CategoryTheory.Sites.Sheaf
+import Mathlib.Tactic.ApplyWith
 
 /-!
 # Dense subsites
diff --git a/Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean b/Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean
index f0f3a969c4866..a065963d28b84 100644
--- a/Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean
+++ b/Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean
@@ -5,6 +5,8 @@ Authors: Adam Topaz
 -/
 import Mathlib.CategoryTheory.Sites.Sieves
 import Mathlib.CategoryTheory.EffectiveEpi.Basic
+import Mathlib.Tactic.NthRewrite
+
 /-!
 
 # Effective epimorphic sieves
diff --git a/Mathlib/CategoryTheory/Sites/Sieves.lean b/Mathlib/CategoryTheory/Sites/Sieves.lean
index 66591c5a8f117..1056f35edb891 100644
--- a/Mathlib/CategoryTheory/Sites/Sieves.lean
+++ b/Mathlib/CategoryTheory/Sites/Sieves.lean
@@ -3,8 +3,9 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Edward Ayers
 -/
-import Mathlib.Data.Set.Lattice
 import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
+import Mathlib.Data.Set.Lattice
+import Mathlib.Tactic.TermCongr
 
 /-!
 # Theory of sieves
diff --git a/Mathlib/CategoryTheory/Thin.lean b/Mathlib/CategoryTheory/Thin.lean
index a2c9cb1099b9c..27a3a78efb39e 100644
--- a/Mathlib/CategoryTheory/Thin.lean
+++ b/Mathlib/CategoryTheory/Thin.lean
@@ -5,6 +5,7 @@ Authors: Kim Morrison, Bhavik Mehta
 -/
 import Mathlib.CategoryTheory.Functor.Category
 import Mathlib.CategoryTheory.Iso
+import Mathlib.Tactic.Subsingleton
 
 /-!
 # Thin categories
diff --git a/Mathlib/Combinatorics/Quiver/Covering.lean b/Mathlib/Combinatorics/Quiver/Covering.lean
index 28e85b2f31ed9..d6062dc7a4573 100644
--- a/Mathlib/Combinatorics/Quiver/Covering.lean
+++ b/Mathlib/Combinatorics/Quiver/Covering.lean
@@ -7,7 +7,7 @@ import Mathlib.Combinatorics.Quiver.Cast
 import Mathlib.Combinatorics.Quiver.Symmetric
 import Mathlib.Data.Sigma.Basic
 import Mathlib.Logic.Equiv.Basic
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.Cases
 
 /-!
 # Covering
diff --git a/Mathlib/Combinatorics/SetFamily/Compression/Down.lean b/Mathlib/Combinatorics/SetFamily/Compression/Down.lean
index 6a0dbfd4822da..1a62e17393e60 100644
--- a/Mathlib/Combinatorics/SetFamily/Compression/Down.lean
+++ b/Mathlib/Combinatorics/SetFamily/Compression/Down.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Data.Finset.Lattice
+import Mathlib.Tactic.Set
 
 /-!
 # Down-compressions
diff --git a/Mathlib/Computability/PartrecCode.lean b/Mathlib/Computability/PartrecCode.lean
index 723eb31bfc2be..48b766c36e884 100644
--- a/Mathlib/Computability/PartrecCode.lean
+++ b/Mathlib/Computability/PartrecCode.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Computability.Partrec
 import Mathlib.Data.Option.Basic
+import Mathlib.Tactic.RSuffices
 
 /-!
 # Gödel Numbering for Partial Recursive Functions.
diff --git a/Mathlib/Computability/TuringMachine.lean b/Mathlib/Computability/TuringMachine.lean
index a75fdceac64eb..bdabb8559e4cf 100644
--- a/Mathlib/Computability/TuringMachine.lean
+++ b/Mathlib/Computability/TuringMachine.lean
@@ -6,12 +6,14 @@ Authors: Mario Carneiro
 import Mathlib.Data.Fintype.Option
 import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Fintype.Pi
-import Mathlib.Data.Vector.Basic
+import Mathlib.Data.List.GetD
 import Mathlib.Data.PFun
+import Mathlib.Data.Vector.Basic
 import Mathlib.Logic.Function.Iterate
 import Mathlib.Order.Basic
 import Mathlib.Tactic.ApplyFun
-import Mathlib.Data.List.GetD
+import Mathlib.Tactic.DefEqTransformations
+import Mathlib.Tactic.RSuffices
 
 /-!
 # Turing machines
diff --git a/Mathlib/Control/Bifunctor.lean b/Mathlib/Control/Bifunctor.lean
index b02897a6225a2..c36210e9ef833 100644
--- a/Mathlib/Control/Bifunctor.lean
+++ b/Mathlib/Control/Bifunctor.lean
@@ -3,9 +3,11 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
-import Mathlib.Control.Functor
-import Mathlib.Tactic.Common
+import Aesop
 import Batteries.Data.Sum.Basic
+import Mathlib.Control.Functor
+import Mathlib.Logic.Function.Basic
+import Mathlib.Tactic.HigherOrder
 
 /-!
 # Functors with two arguments
diff --git a/Mathlib/Control/Fix.lean b/Mathlib/Control/Fix.lean
index 0c11259b0ee51..a6b91b0be8241 100644
--- a/Mathlib/Control/Fix.lean
+++ b/Mathlib/Control/Fix.lean
@@ -7,7 +7,6 @@ import Mathlib.Data.Part
 import Mathlib.Data.Nat.Find
 import Mathlib.Data.Nat.Upto
 import Mathlib.Data.Stream.Defs
-import Mathlib.Tactic.Common
 
 /-!
 # Fixed point
diff --git a/Mathlib/Control/LawfulFix.lean b/Mathlib/Control/LawfulFix.lean
index f22207cffe5c1..a363aeba4c12e 100644
--- a/Mathlib/Control/LawfulFix.lean
+++ b/Mathlib/Control/LawfulFix.lean
@@ -3,10 +3,11 @@ Copyright (c) 2020 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
-import Mathlib.Data.Stream.Init
-import Mathlib.Tactic.ApplyFun
 import Mathlib.Control.Fix
+import Mathlib.Data.Stream.Init
 import Mathlib.Order.OmegaCompletePartialOrder
+import Mathlib.Tactic.ApplyFun
+import Mathlib.Tactic.WLOG
 
 /-!
 # Lawful fixed point operators
diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean
index 95384eac7bdcf..26a4ee651e29a 100644
--- a/Mathlib/Data/Fin/Basic.lean
+++ b/Mathlib/Data/Fin/Basic.lean
@@ -8,8 +8,8 @@ import Mathlib.Data.Nat.Defs
 import Mathlib.Data.Int.DivMod
 import Mathlib.Logic.Embedding.Basic
 import Mathlib.Logic.Equiv.Set
-import Mathlib.Tactic.Common
 import Mathlib.Tactic.Attr.Register
+import Mathlib.Tactic.Cases
 
 /-!
 # The finite type with `n` elements
diff --git a/Mathlib/Data/Fin/Tuple/Basic.lean b/Mathlib/Data/Fin/Tuple/Basic.lean
index 81cd43b8a59f1..27f07173b92b1 100644
--- a/Mathlib/Data/Fin/Tuple/Basic.lean
+++ b/Mathlib/Data/Fin/Tuple/Basic.lean
@@ -5,6 +5,7 @@ Authors: Floris van Doorn, Yury Kudryashov, Sébastien Gouëzel, Chris Hughes
 -/
 import Mathlib.Data.Fin.Basic
 import Mathlib.Data.Nat.Find
+import Mathlib.Tactic.Set
 
 /-!
 # Operation on tuples
diff --git a/Mathlib/Data/Finset/Max.lean b/Mathlib/Data/Finset/Max.lean
index a972df5dc3ddc..5b758e9aa974b 100644
--- a/Mathlib/Data/Finset/Max.lean
+++ b/Mathlib/Data/Finset/Max.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.Finset.Lattice
+import Mathlib.Tactic.Set
 
 /-!
 # Maximum and minimum of finite sets
diff --git a/Mathlib/Data/Finset/Update.lean b/Mathlib/Data/Finset/Update.lean
index d4dfb055c18ea..4abe71b665012 100644
--- a/Mathlib/Data/Finset/Update.lean
+++ b/Mathlib/Data/Finset/Update.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 import Mathlib.Data.Finset.Basic
+import Mathlib.Tactic.Set
 
 /-!
 # Update a function on a set of values
diff --git a/Mathlib/Data/Fintype/Card.lean b/Mathlib/Data/Fintype/Card.lean
index e5e21cc3387b4..50cb9390c5ab3 100644
--- a/Mathlib/Data/Fintype/Card.lean
+++ b/Mathlib/Data/Fintype/Card.lean
@@ -8,6 +8,7 @@ import Mathlib.Data.Finset.Card
 import Mathlib.Data.List.NodupEquivFin
 import Mathlib.Data.Set.Image
 import Mathlib.Order.WellFounded
+import Mathlib.Tactic.WLOG
 
 /-!
 # Cardinalities of finite types
diff --git a/Mathlib/Data/Fintype/CardEmbedding.lean b/Mathlib/Data/Fintype/CardEmbedding.lean
index da9e62d27dcf0..debd34b055313 100644
--- a/Mathlib/Data/Fintype/CardEmbedding.lean
+++ b/Mathlib/Data/Fintype/CardEmbedding.lean
@@ -5,6 +5,7 @@ Authors: Eric Rodriguez
 -/
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Logic.Equiv.Embedding
+import Mathlib.Tactic.ClearExclamation
 
 /-!
 # Number of embeddings
diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean
index e0bc3e616150f..5aeaa09842046 100644
--- a/Mathlib/Data/Int/Bitwise.lean
+++ b/Mathlib/Data/Int/Bitwise.lean
@@ -6,6 +6,7 @@ Authors: Jeremy Avigad
 import Mathlib.Algebra.Ring.Int
 import Mathlib.Data.Nat.Bitwise
 import Mathlib.Data.Nat.Size
+import Mathlib.Tactic.DefEqTransformations
 
 /-!
 # Bitwise operations on integers
diff --git a/Mathlib/Data/Int/Sqrt.lean b/Mathlib/Data/Int/Sqrt.lean
index 1c6db061ba8f7..1fbce30337572 100644
--- a/Mathlib/Data/Int/Sqrt.lean
+++ b/Mathlib/Data/Int/Sqrt.lean
@@ -5,7 +5,6 @@ Authors: Kenny Lau
 -/
 import Mathlib.Data.Int.Defs
 import Mathlib.Data.Nat.Sqrt
-import Mathlib.Tactic.Common
 
 /-!
 # Square root of integers
diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
index efee2daa93ea1..f89cff58043a5 100644
--- a/Mathlib/Data/List/Basic.lean
+++ b/Mathlib/Data/List/Basic.lean
@@ -11,7 +11,12 @@ import Mathlib.Data.List.Monad
 import Mathlib.Logic.OpClass
 import Mathlib.Logic.Unique
 import Mathlib.Order.Basic
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.Cases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Says
+import Mathlib.Tactic.Subsingleton
+import Mathlib.Tactic.TermCongr
+import Mathlib.Tactic.Use
 
 /-!
 # Basic properties of lists
diff --git a/Mathlib/Data/List/Chain.lean b/Mathlib/Data/List/Chain.lean
index 8b844a1f6243c..a2aa619723a74 100644
--- a/Mathlib/Data/List/Chain.lean
+++ b/Mathlib/Data/List/Chain.lean
@@ -6,6 +6,7 @@ Authors: Mario Carneiro, Kenny Lau, Yury Kudryashov
 import Mathlib.Logic.Relation
 import Mathlib.Data.List.Forall2
 import Mathlib.Data.List.Lex
+import Mathlib.Tactic.ByContra
 
 /-!
 # Relation chain
diff --git a/Mathlib/Data/List/Count.lean b/Mathlib/Data/List/Count.lean
index 13c127b563b2a..3ef8754a3c9f5 100644
--- a/Mathlib/Data/List/Count.lean
+++ b/Mathlib/Data/List/Count.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
 -/
 import Mathlib.Logic.Function.Basic
-import Mathlib.Tactic.Common
+import Mathlib.Util.AssertExists
 
 /-!
 # Counting in lists
diff --git a/Mathlib/Data/List/Forall2.lean b/Mathlib/Data/List/Forall2.lean
index 79f5bf6c1cb0a..ea4305e0b3747 100644
--- a/Mathlib/Data/List/Forall2.lean
+++ b/Mathlib/Data/List/Forall2.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johannes Hölzl
 -/
 import Mathlib.Data.List.Basic
+import Mathlib.Tactic.MkIffOfInductiveProp
 
 /-!
 # Double universal quantification on a list
diff --git a/Mathlib/Data/List/Infix.lean b/Mathlib/Data/List/Infix.lean
index 030675eb9f683..0b9c3b9ecbb1b 100644
--- a/Mathlib/Data/List/Infix.lean
+++ b/Mathlib/Data/List/Infix.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.List.Basic
+import Mathlib.Tactic.NthRewrite
 
 /-!
 # Prefixes, suffixes, infixes
diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean
index 0aa5947c0e464..48d9a6e7a8eae 100644
--- a/Mathlib/Data/Multiset/Basic.lean
+++ b/Mathlib/Data/Multiset/Basic.lean
@@ -10,6 +10,7 @@ import Mathlib.Data.Set.List
 import Mathlib.Order.Hom.Basic
 import Mathlib.Data.List.Perm.Lattice
 import Mathlib.Data.List.Perm.Basic
+import Mathlib.Tactic.Constructor
 
 /-!
 # Multisets
diff --git a/Mathlib/Data/NNRat/Lemmas.lean b/Mathlib/Data/NNRat/Lemmas.lean
index 88467e704c1a4..60170332d8eca 100644
--- a/Mathlib/Data/NNRat/Lemmas.lean
+++ b/Mathlib/Data/NNRat/Lemmas.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Field.Rat
 import Mathlib.Algebra.Group.Indicator
 import Mathlib.Algebra.GroupWithZero.Action.End
 import Mathlib.Algebra.Order.Field.Rat
+import Mathlib.Tactic.NthRewrite
 
 /-!
 # Field and action structures on the nonnegative rationals
diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
index 70965de4413df..6545d7a1d1049 100644
--- a/Mathlib/Data/Nat/Bitwise.lean
+++ b/Mathlib/Data/Nat/Bitwise.lean
@@ -10,7 +10,8 @@ import Mathlib.Data.List.GetD
 import Mathlib.Data.Nat.Bits
 import Mathlib.Order.Basic
 import Mathlib.Tactic.AdaptationNote
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.Cases
+import Mathlib.Tactic.Set
 
 /-!
 # Bitwise operations on natural numbers
diff --git a/Mathlib/Data/Nat/Cast/Field.lean b/Mathlib/Data/Nat/Cast/Field.lean
index d532397a177fd..a75d157a9a2e5 100644
--- a/Mathlib/Data/Nat/Cast/Field.lean
+++ b/Mathlib/Data/Nat/Cast/Field.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro, Yaël Dillies, Patrick Stevens
 -/
 import Mathlib.Algebra.CharZero.Defs
 import Mathlib.Data.Nat.Cast.Basic
-import Mathlib.Tactic.Common
 import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.GroupWithZero.Units.Basic
 
diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean
index 79539c43a7625..4f59e07a536ca 100644
--- a/Mathlib/Data/Nat/Factorial/Basic.lean
+++ b/Mathlib/Data/Nat/Factorial/Basic.lean
@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Chris Hughes, Floris van Doorn, Yaël Dillies
 -/
 import Mathlib.Data.Nat.Defs
+import Mathlib.Tactic.Cases
 import Mathlib.Tactic.GCongr.CoreAttrs
-import Mathlib.Tactic.Common
 import Mathlib.Tactic.Monotonicity.Attr
+import Mathlib.Tactic.NthRewrite
 
 /-!
 # Factorial and variants
diff --git a/Mathlib/Data/Nat/GCD/Basic.lean b/Mathlib/Data/Nat/GCD/Basic.lean
index ff926c64b4005..47763907fd856 100644
--- a/Mathlib/Data/Nat/GCD/Basic.lean
+++ b/Mathlib/Data/Nat/GCD/Basic.lean
@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura
 import Batteries.Data.Nat.Gcd
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.Ring.Nat
+import Mathlib.Tactic.NthRewrite
 
 /-!
 # Properties of `Nat.gcd`, `Nat.lcm`, and `Nat.Coprime`
diff --git a/Mathlib/Data/Nat/MaxPowDiv.lean b/Mathlib/Data/Nat/MaxPowDiv.lean
index 34905e1420912..4f122e9bd53b8 100644
--- a/Mathlib/Data/Nat/MaxPowDiv.lean
+++ b/Mathlib/Data/Nat/MaxPowDiv.lean
@@ -5,7 +5,7 @@ Authors: Matthew Robert Ballard
 -/
 import Mathlib.Algebra.Divisibility.Units
 import Mathlib.Algebra.Order.Ring.Nat
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.NthRewrite
 
 /-!
 # The maximal power of one natural number dividing another
diff --git a/Mathlib/Data/Nat/Prime/Basic.lean b/Mathlib/Data/Nat/Prime/Basic.lean
index 24bdc1be8b0c1..de75f562a265e 100644
--- a/Mathlib/Data/Nat/Prime/Basic.lean
+++ b/Mathlib/Data/Nat/Prime/Basic.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 import Mathlib.Algebra.Associated.Basic
 import Mathlib.Algebra.Ring.Parity
 import Mathlib.Data.Nat.Prime.Defs
+import Mathlib.Tactic.ByContra
 
 /-!
 # Prime numbers
diff --git a/Mathlib/Data/Rat/Defs.lean b/Mathlib/Data/Rat/Defs.lean
index 196de7dc71c26..b0b40f887dbba 100644
--- a/Mathlib/Data/Rat/Defs.lean
+++ b/Mathlib/Data/Rat/Defs.lean
@@ -7,7 +7,9 @@ import Mathlib.Algebra.Group.Defs
 import Mathlib.Data.Int.Defs
 import Mathlib.Data.Rat.Init
 import Mathlib.Order.Basic
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.Cases
+import Mathlib.Tactic.Coe
+import Mathlib.Tactic.Tauto
 import Batteries.Data.Rat.Lemmas
 
 /-!
diff --git a/Mathlib/Data/Rat/Lemmas.lean b/Mathlib/Data/Rat/Lemmas.lean
index 2423ed18b9d60..e48258775c460 100644
--- a/Mathlib/Data/Rat/Lemmas.lean
+++ b/Mathlib/Data/Rat/Lemmas.lean
@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.Ring.Rat
 import Mathlib.Data.PNat.Defs
+import Mathlib.Tactic.NthRewrite
 
 /-!
 # Further lemmas for the Rational Numbers
diff --git a/Mathlib/Data/Real/Basic.lean b/Mathlib/Data/Real/Basic.lean
index 3465de02f2a9a..5117b9fd7d0d6 100644
--- a/Mathlib/Data/Real/Basic.lean
+++ b/Mathlib/Data/Real/Basic.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Floris van Doorn
 -/
 import Mathlib.Algebra.Order.CauSeq.Completion
 import Mathlib.Algebra.Order.Field.Rat
+import Mathlib.Tactic.IrreducibleDef
 
 /-!
 # Real numbers from Cauchy sequences
diff --git a/Mathlib/Data/Seq/Computation.lean b/Mathlib/Data/Seq/Computation.lean
index 0cb816198ffd8..79baab6237a14 100644
--- a/Mathlib/Data/Seq/Computation.lean
+++ b/Mathlib/Data/Seq/Computation.lean
@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Data.Nat.Find
 import Mathlib.Data.Stream.Init
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.DefEqTransformations
 
 /-!
 # Coinductive formalization of unbounded computations.
diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index b005e06bce8fb..7fed98f3a13fd 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Data.Option.NAry
 import Mathlib.Data.Seq.Computation
+import Batteries.Data.MLList.Basic
 
 /-!
 # Possibly infinite lists
diff --git a/Mathlib/Data/Seq/WSeq.lean b/Mathlib/Data/Seq/WSeq.lean
index 5b57888ef3f6e..0c8e4e2e6825e 100644
--- a/Mathlib/Data/Seq/WSeq.lean
+++ b/Mathlib/Data/Seq/WSeq.lean
@@ -3,10 +3,11 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Logic.Relation
+import Batteries.Data.DList.Basic
 import Mathlib.Data.Option.Basic
 import Mathlib.Data.Seq.Seq
-import Batteries.Data.DList.Basic
+import Mathlib.Logic.Relation
+import Mathlib.Tactic.Substs
 
 /-!
 # Partially defined possibly infinite lists
diff --git a/Mathlib/Data/Set/Enumerate.lean b/Mathlib/Data/Set/Enumerate.lean
index 908974989a9e3..44b150ca7d885 100644
--- a/Mathlib/Data/Set/Enumerate.lean
+++ b/Mathlib/Data/Set/Enumerate.lean
@@ -5,8 +5,9 @@ Authors: Johannes Hölzl
 -/
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Nat
-import Mathlib.Tactic.Common
 import Mathlib.Data.Set.Basic
+import Mathlib.Tactic.Says
+import Mathlib.Tactic.SwapVar
 
 /-!
 # Set enumeration
diff --git a/Mathlib/Data/Set/Lattice.lean b/Mathlib/Data/Set/Lattice.lean
index f85d0821bddfd..eccd62e67f70d 100644
--- a/Mathlib/Data/Set/Lattice.lean
+++ b/Mathlib/Data/Set/Lattice.lean
@@ -7,6 +7,7 @@ import Mathlib.Logic.Pairwise
 import Mathlib.Order.CompleteBooleanAlgebra
 import Mathlib.Order.Directed
 import Mathlib.Order.GaloisConnection
+import Mathlib.Tactic.Cases
 
 /-!
 # The set lattice
diff --git a/Mathlib/Data/Set/Pairwise/Basic.lean b/Mathlib/Data/Set/Pairwise/Basic.lean
index ec5b714ca6538..9c49e4d3c8782 100644
--- a/Mathlib/Data/Set/Pairwise/Basic.lean
+++ b/Mathlib/Data/Set/Pairwise/Basic.lean
@@ -6,6 +6,7 @@ Authors: Johannes Hölzl
 import Mathlib.Data.Set.Function
 import Mathlib.Logic.Pairwise
 import Mathlib.Logic.Relation
+import Mathlib.Tactic.Cases
 
 /-!
 # Relations holding pairwise
diff --git a/Mathlib/Data/TypeVec.lean b/Mathlib/Data/TypeVec.lean
index df15092ea20be..b928c9f3a606d 100644
--- a/Mathlib/Data/TypeVec.lean
+++ b/Mathlib/Data/TypeVec.lean
@@ -5,7 +5,6 @@ Authors: Jeremy Avigad, Mario Carneiro, Simon Hudon
 -/
 import Mathlib.Data.Fin.Fin2
 import Mathlib.Logic.Function.Basic
-import Mathlib.Tactic.Common
 
 /-!
 
diff --git a/Mathlib/Data/Vector/Basic.lean b/Mathlib/Data/Vector/Basic.lean
index 50418d58cb02f..eead21e1dde08 100644
--- a/Mathlib/Data/Vector/Basic.lean
+++ b/Mathlib/Data/Vector/Basic.lean
@@ -10,6 +10,7 @@ import Mathlib.Data.List.OfFn
 import Mathlib.Data.List.InsertIdx
 import Mathlib.Control.Applicative
 import Mathlib.Control.Traversable.Basic
+import Mathlib.Tactic.ClearExcept
 
 /-!
 # Additional theorems and definitions about the `Vector` type
diff --git a/Mathlib/Data/Vector/Defs.lean b/Mathlib/Data/Vector/Defs.lean
index 24273d810fe4f..166fdcbd50369 100644
--- a/Mathlib/Data/Vector/Defs.lean
+++ b/Mathlib/Data/Vector/Defs.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Mathlib.Data.List.Defs
-import Mathlib.Tactic.Common
+import Mathlib.Util.AssertExists
 
 /-!
 The type `Vector` represents lists with fixed length.
diff --git a/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean b/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean
index e3a6f25954b2b..2a4a8f6f95d9e 100644
--- a/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean
+++ b/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Wärn, Eric Wieser, Joachim Breitner
 -/
 import Mathlib.GroupTheory.FreeGroup.Basic
+import Mathlib.Tactic.IrreducibleDef
 
 /-!
 # Free groups structures on arbitrary types
diff --git a/Mathlib/GroupTheory/GroupAction/Defs.lean b/Mathlib/GroupTheory/GroupAction/Defs.lean
index 0beafab0cdd6f..d38b033750db6 100644
--- a/Mathlib/GroupTheory/GroupAction/Defs.lean
+++ b/Mathlib/GroupTheory/GroupAction/Defs.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Group.Pointwise.Set.Basic
 import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Algebra.GroupWithZero.Action.Defs
+import Mathlib.Tactic.Set
 
 /-!
 # Definition of `orbit`, `fixedPoints` and `stabilizer`
diff --git a/Mathlib/GroupTheory/OreLocalization/Basic.lean b/Mathlib/GroupTheory/OreLocalization/Basic.lean
index 82c2f2d7c5cd1..07b248d205f08 100644
--- a/Mathlib/GroupTheory/OreLocalization/Basic.lean
+++ b/Mathlib/GroupTheory/OreLocalization/Basic.lean
@@ -5,6 +5,8 @@ Authors: Jakob von Raumer, Kevin Klinge, Andrew Yang
 -/
 import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.GroupTheory.OreLocalization.OreSet
+import Mathlib.Tactic.DefEqTransformations
+import Mathlib.Tactic.Set
 
 /-!
 
diff --git a/Mathlib/GroupTheory/Perm/Basic.lean b/Mathlib/GroupTheory/Perm/Basic.lean
index 70e6c423d6dfd..a83a3ec4f5556 100644
--- a/Mathlib/GroupTheory/Perm/Basic.lean
+++ b/Mathlib/GroupTheory/Perm/Basic.lean
@@ -7,7 +7,7 @@ import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Group.Units.Equiv
 import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.Logic.Equiv.Set
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.NthRewrite
 
 /-!
 # The group of permutations (self-equivalences) of a type `α`
diff --git a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
index b81a28f1405ee..aea5c70ab850c 100644
--- a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
@@ -5,6 +5,7 @@ Authors: Zhangir Azerbayev, Adam Topaz, Eric Wieser
 -/
 import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
 import Mathlib.LinearAlgebra.Alternating.Basic
+import Mathlib.Tactic.ExistsI
 
 /-!
 # Exterior Algebras
diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean
index 549483263a2a1..42cc266bc6fc4 100644
--- a/Mathlib/LinearAlgebra/PiTensorProduct.lean
+++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean
@@ -5,6 +5,7 @@ Authors: Frédéric Dupuis, Eric Wieser
 -/
 import Mathlib.LinearAlgebra.Multilinear.TensorProduct
 import Mathlib.Tactic.AdaptationNote
+import Mathlib.Tactic.ExistsI
 
 /-!
 # Tensor product of an indexed family of modules over commutative semirings
diff --git a/Mathlib/Logic/Pairwise.lean b/Mathlib/Logic/Pairwise.lean
index 13ae772203bbe..ba62702441eb9 100644
--- a/Mathlib/Logic/Pairwise.lean
+++ b/Mathlib/Logic/Pairwise.lean
@@ -5,7 +5,6 @@ Authors: Johannes Hölzl
 -/
 import Mathlib.Logic.Function.Basic
 import Mathlib.Data.Set.Defs
-import Mathlib.Tactic.Common
 
 /-!
 # Relations holding pairwise
diff --git a/Mathlib/MeasureTheory/Measure/Portmanteau.lean b/Mathlib/MeasureTheory/Measure/Portmanteau.lean
index 4d82e897d1771..cf5987e5abbbb 100644
--- a/Mathlib/MeasureTheory/Measure/Portmanteau.lean
+++ b/Mathlib/MeasureTheory/Measure/Portmanteau.lean
@@ -7,6 +7,7 @@ import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
 import Mathlib.MeasureTheory.Integral.Layercake
 import Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
+import Mathlib.Tactic.InferParam
 
 /-!
 # Characterizations of weak convergence of finite measures and probability measures
diff --git a/Mathlib/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean
index 2f16137420ef0..54f60f2549f43 100644
--- a/Mathlib/MeasureTheory/PiSystem.lean
+++ b/Mathlib/MeasureTheory/PiSystem.lean
@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Martin Zinkevich, Rémy Degenne
 -/
 import Mathlib.Logic.Encodable.Lattice
 import Mathlib.MeasureTheory.MeasurableSpace.Defs
+import Mathlib.Tactic.DefEqTransformations
 
 /-!
 # Induction principles for measurable sets, related to π-systems and λ-systems.
diff --git a/Mathlib/NumberTheory/BernoulliPolynomials.lean b/Mathlib/NumberTheory/BernoulliPolynomials.lean
index f333c35443ce6..db816ee89c0fc 100644
--- a/Mathlib/NumberTheory/BernoulliPolynomials.lean
+++ b/Mathlib/NumberTheory/BernoulliPolynomials.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Polynomial.AlgebraMap
 import Mathlib.Algebra.Polynomial.Derivative
 import Mathlib.Data.Nat.Choose.Cast
 import Mathlib.NumberTheory.Bernoulli
+import Mathlib.Tactic.ApplyCongr
 
 /-!
 # Bernoulli polynomials
diff --git a/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean b/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean
index 12ed3466ca3dc..123b1f78482b7 100644
--- a/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean
+++ b/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean
@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
 import Mathlib.NumberTheory.Liouville.Basic
+import Mathlib.Tactic.Rename
 import Mathlib.Topology.Instances.Irrational
 
 /-!
diff --git a/Mathlib/NumberTheory/RamificationInertia.lean b/Mathlib/NumberTheory/RamificationInertia.lean
index cd2da449ce790..f41c208ce4a04 100644
--- a/Mathlib/NumberTheory/RamificationInertia.lean
+++ b/Mathlib/NumberTheory/RamificationInertia.lean
@@ -5,6 +5,7 @@ Authors: Anne Baanen
 -/
 import Mathlib.LinearAlgebra.Dimension.DivisionRing
 import Mathlib.RingTheory.DedekindDomain.Ideal
+import Mathlib.Tactic.ApplyWith
 
 /-!
 # Ramification index and inertia degree
diff --git a/Mathlib/Order/Filter/AtTopBot.lean b/Mathlib/Order/Filter/AtTopBot.lean
index fc058972b73f4..0587c2d55f80a 100644
--- a/Mathlib/Order/Filter/AtTopBot.lean
+++ b/Mathlib/Order/Filter/AtTopBot.lean
@@ -9,6 +9,7 @@ import Mathlib.Order.Filter.Bases
 import Mathlib.Order.Filter.Prod
 import Mathlib.Order.Interval.Set.Disjoint
 import Mathlib.Order.Interval.Set.OrderIso
+import Mathlib.Tactic.RSuffices
 
 /-!
 # `Filter.atTop` and `Filter.atBot` filters on preorders, monoids and groups.
diff --git a/Mathlib/Order/FixedPoints.lean b/Mathlib/Order/FixedPoints.lean
index e6f40735b5ddc..60691845f1d4d 100644
--- a/Mathlib/Order/FixedPoints.lean
+++ b/Mathlib/Order/FixedPoints.lean
@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Kenny Lau, Yury Kudryashov
 import Mathlib.Dynamics.FixedPoints.Basic
 import Mathlib.Order.Hom.Order
 import Mathlib.Order.OmegaCompletePartialOrder
+import Mathlib.Tactic.Set
 
 /-!
 # Fixed point construction on complete lattices
diff --git a/Mathlib/Order/Heyting/Boundary.lean b/Mathlib/Order/Heyting/Boundary.lean
index bd8e498fc6eed..c286e0f42c67e 100644
--- a/Mathlib/Order/Heyting/Boundary.lean
+++ b/Mathlib/Order/Heyting/Boundary.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Order.BooleanAlgebra
-import Mathlib.Tactic.Common
 
 /-!
 # Co-Heyting boundary
diff --git a/Mathlib/Order/Interval/Set/OrdConnectedComponent.lean b/Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
index 54ddf55dae58b..aeaa54d58e0f1 100644
--- a/Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
+++ b/Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Order.Interval.Set.OrdConnected
 import Mathlib.Data.Set.Lattice
+import Mathlib.Tactic.WLOG
 
 /-!
 # Order connected components of a set
diff --git a/Mathlib/Order/Interval/Set/UnorderedInterval.lean b/Mathlib/Order/Interval/Set/UnorderedInterval.lean
index 22ca451903d02..66b4f7d1dd59d 100644
--- a/Mathlib/Order/Interval/Set/UnorderedInterval.lean
+++ b/Mathlib/Order/Interval/Set/UnorderedInterval.lean
@@ -5,7 +5,6 @@ Authors: Zhouhang Zhou
 -/
 import Mathlib.Order.Interval.Set.Image
 import Mathlib.Order.Bounds.Basic
-import Mathlib.Tactic.Common
 
 /-!
 # Intervals without endpoints ordering
diff --git a/Mathlib/Order/OrderIsoNat.lean b/Mathlib/Order/OrderIsoNat.lean
index da0fabb452ad3..5a1010eaa9121 100644
--- a/Mathlib/Order/OrderIsoNat.lean
+++ b/Mathlib/Order/OrderIsoNat.lean
@@ -9,6 +9,7 @@ import Mathlib.Logic.Denumerable
 import Mathlib.Logic.Function.Iterate
 import Mathlib.Order.Hom.Basic
 import Mathlib.Data.Set.Subsingleton
+import Mathlib.Tactic.CongrM
 
 /-!
 # Relation embeddings from the naturals
diff --git a/Mathlib/Order/Part.lean b/Mathlib/Order/Part.lean
index 095e4622ab550..622dda2c3a303 100644
--- a/Mathlib/Order/Part.lean
+++ b/Mathlib/Order/Part.lean
@@ -5,7 +5,6 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Data.Part
 import Mathlib.Order.Hom.Basic
-import Mathlib.Tactic.Common
 
 /-!
 # Monotonicity of monadic operations on `Part`
diff --git a/Mathlib/Order/PiLex.lean b/Mathlib/Order/PiLex.lean
index 4fd435168435e..138d70447433f 100644
--- a/Mathlib/Order/PiLex.lean
+++ b/Mathlib/Order/PiLex.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import Mathlib.Order.WellFounded
-import Mathlib.Tactic.Common
+import Mathlib.Tactic.Cases
 
 /-!
 # Lexicographic order on Pi types
diff --git a/Mathlib/Order/PrimeSeparator.lean b/Mathlib/Order/PrimeSeparator.lean
index 25826ad97ce55..8233d96a79a6f 100644
--- a/Mathlib/Order/PrimeSeparator.lean
+++ b/Mathlib/Order/PrimeSeparator.lean
@@ -6,6 +6,7 @@ Authors: Sam van Gool
 
 import Mathlib.Order.PrimeIdeal
 import Mathlib.Order.Zorn
+import Mathlib.Tactic.Set
 
 /-!
 # Separating prime filters and ideals
diff --git a/Mathlib/Order/SuccPred/Archimedean.lean b/Mathlib/Order/SuccPred/Archimedean.lean
index 4ba2d38f22bdc..a6370dc3d1a58 100644
--- a/Mathlib/Order/SuccPred/Archimedean.lean
+++ b/Mathlib/Order/SuccPred/Archimedean.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Order.SuccPred.Basic
+import Mathlib.Tactic.ApplyAt
+import Mathlib.Tactic.WLOG
 
 /-!
 # Archimedean successor and predecessor
diff --git a/Mathlib/Order/SuccPred/Basic.lean b/Mathlib/Order/SuccPred/Basic.lean
index 55b6157d4a5db..bf7617b1c5811 100644
--- a/Mathlib/Order/SuccPred/Basic.lean
+++ b/Mathlib/Order/SuccPred/Basic.lean
@@ -6,6 +6,7 @@ Authors: Yaël Dillies
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Order.Cover
 import Mathlib.Order.Iterate
+import Mathlib.Tactic.TermCongr
 
 /-!
 # Successor and predecessor
diff --git a/Mathlib/RingTheory/Localization/Defs.lean b/Mathlib/RingTheory/Localization/Defs.lean
index 3d6a50bf16c29..c43bfd8319e80 100644
--- a/Mathlib/RingTheory/Localization/Defs.lean
+++ b/Mathlib/RingTheory/Localization/Defs.lean
@@ -5,6 +5,7 @@ Authors: Kenny Lau, Mario Carneiro, Johan Commelin, Amelia Livingston, Anne Baan
 -/
 import Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
 import Mathlib.RingTheory.OreLocalization.Ring
+import Mathlib.Tactic.ApplyAt
 import Mathlib.Tactic.Ring
 
 /-!
diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean
index 5ba8201e865fb..d8e8f077199a3 100644
--- a/Mathlib/RingTheory/Localization/FractionRing.lean
+++ b/Mathlib/RingTheory/Localization/FractionRing.lean
@@ -8,6 +8,7 @@ import Mathlib.Algebra.Field.Equiv
 import Mathlib.Algebra.Order.Field.Rat
 import Mathlib.Algebra.Order.Ring.Int
 import Mathlib.RingTheory.Localization.Basic
+import Mathlib.Tactic.IrreducibleDef
 
 /-!
 # Fraction ring / fraction field Frac(R) as localization
diff --git a/Mathlib/RingTheory/Valuation/ValExtension.lean b/Mathlib/RingTheory/Valuation/ValExtension.lean
index 11ee048743d9c..b016908a64324 100644
--- a/Mathlib/RingTheory/Valuation/ValExtension.lean
+++ b/Mathlib/RingTheory/Valuation/ValExtension.lean
@@ -3,8 +3,9 @@ Copyright (c) 2024 Jiedong Jiang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jiedong Jiang, Bichang Lei
 -/
-import Mathlib.RingTheory.Valuation.Integers
 import Mathlib.Algebra.Group.Units.Hom
+import Mathlib.RingTheory.Valuation.Integers
+import Mathlib.Tactic.ApplyAt
 
 /-!
 # Extension of Valuation
diff --git a/Mathlib/Tactic/CategoryTheory/Bicategory/Datatypes.lean b/Mathlib/Tactic/CategoryTheory/Bicategory/Datatypes.lean
index 42225947c25da..052095884f8b8 100644
--- a/Mathlib/Tactic/CategoryTheory/Bicategory/Datatypes.lean
+++ b/Mathlib/Tactic/CategoryTheory/Bicategory/Datatypes.lean
@@ -5,6 +5,7 @@ Authors: Yuma Mizuno
 -/
 import Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
 import Mathlib.Tactic.CategoryTheory.BicategoricalComp
+import QQ
 
 /-!
 # Expressions for bicategories
diff --git a/Mathlib/Tactic/Widget/StringDiagram.lean b/Mathlib/Tactic/Widget/StringDiagram.lean
index c2745df6eff9a..8ac0a8073cd77 100644
--- a/Mathlib/Tactic/Widget/StringDiagram.lean
+++ b/Mathlib/Tactic/Widget/StringDiagram.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Yuma Mizuno. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuma Mizuno
 -/
+import ProofWidgets.Component.OfRpcMethod
 import ProofWidgets.Component.PenroseDiagram
 import ProofWidgets.Component.Panel.Basic
 import ProofWidgets.Presentation.Expr
diff --git a/Mathlib/Testing/SlimCheck/Functions.lean b/Mathlib/Testing/SlimCheck/Functions.lean
index 7b73daf4bdbcb..201a629d0bdfa 100644
--- a/Mathlib/Testing/SlimCheck/Functions.lean
+++ b/Mathlib/Testing/SlimCheck/Functions.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
+import Batteries.Data.MLList.Basic
 import Mathlib.Data.List.Sigma
 import Mathlib.Data.Int.Range
 import Mathlib.Data.Finsupp.Defs
diff --git a/Mathlib/Topology/Algebra/ProperAction/Basic.lean b/Mathlib/Topology/Algebra/ProperAction/Basic.lean
index 5b68b2d2d0d6f..c9d0740298aa1 100644
--- a/Mathlib/Topology/Algebra/ProperAction/Basic.lean
+++ b/Mathlib/Topology/Algebra/ProperAction/Basic.lean
@@ -6,6 +6,7 @@ Authors: Anatole Dedeker, Etienne Marion, Florestan Martin-Baillon, Vincent Guir
 import Mathlib.Topology.Algebra.MulAction
 import Mathlib.Topology.Maps.Proper.Basic
 import Mathlib.Topology.Maps.OpenQuotient
+import Mathlib.Tactic.CongrM
 
 /-!
 # Proper group action
diff --git a/Mathlib/Topology/Defs/Filter.lean b/Mathlib/Topology/Defs/Filter.lean
index bf9b961755c3a..aab9695a75f09 100644
--- a/Mathlib/Topology/Defs/Filter.lean
+++ b/Mathlib/Topology/Defs/Filter.lean
@@ -3,9 +3,10 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Jeremy Avigad
 -/
-import Mathlib.Topology.Defs.Basic
-import Mathlib.Order.Filter.Ultrafilter
 import Mathlib.Data.Set.Lattice
+import Mathlib.Order.Filter.Ultrafilter
+import Mathlib.Tactic.IrreducibleDef
+import Mathlib.Topology.Defs.Basic
 
 /-!
 # Definitions about filters in topological spaces
diff --git a/Mathlib/Topology/DiscreteSubset.lean b/Mathlib/Topology/DiscreteSubset.lean
index 70e38c4cc3f54..a1b8e8b8035a2 100644
--- a/Mathlib/Topology/DiscreteSubset.lean
+++ b/Mathlib/Topology/DiscreteSubset.lean
@@ -5,6 +5,7 @@ Authors: Oliver Nash, Bhavik Mehta, Daniel Weber
 -/
 import Mathlib.Topology.Constructions
 import Mathlib.Topology.Separation.Basic
+import Mathlib.Tactic.CongrM
 
 /-!
 # Discrete subsets of topological spaces
diff --git a/Mathlib/Topology/Gluing.lean b/Mathlib/Topology/Gluing.lean
index 65f52bacfc964..e12ea2499bd04 100644
--- a/Mathlib/Topology/Gluing.lean
+++ b/Mathlib/Topology/Gluing.lean
@@ -3,12 +3,13 @@ Copyright (c) 2021 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
+import Mathlib.CategoryTheory.ConcreteCategory.EpiMono
+import Mathlib.CategoryTheory.Elementwise
 import Mathlib.CategoryTheory.GlueData
+import Mathlib.Tactic.DefEqTransformations
+import Mathlib.Tactic.Generalize
 import Mathlib.Topology.Category.TopCat.Limits.Pullbacks
 import Mathlib.Topology.Category.TopCat.Opens
-import Mathlib.Tactic.Generalize
-import Mathlib.CategoryTheory.Elementwise
-import Mathlib.CategoryTheory.ConcreteCategory.EpiMono
 
 /-!
 # Gluing Topological spaces
diff --git a/Mathlib/Topology/Sheaves/Stalks.lean b/Mathlib/Topology/Sheaves/Stalks.lean
index 125a7e70f0fc4..4bd42900439a8 100644
--- a/Mathlib/Topology/Sheaves/Stalks.lean
+++ b/Mathlib/Topology/Sheaves/Stalks.lean
@@ -3,15 +3,16 @@ Copyright (c) 2019 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Justus Springer
 -/
-import Mathlib.Topology.Category.TopCat.OpenNhds
-import Mathlib.Topology.Sheaves.Presheaf
-import Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
+import Mathlib.Algebra.Category.Ring.Colimits
+import Mathlib.CategoryTheory.Limits.Final
 import Mathlib.CategoryTheory.Limits.Types
 import Mathlib.CategoryTheory.Limits.Preserves.Filtered
-import Mathlib.CategoryTheory.Limits.Final
-import Mathlib.Tactic.CategoryTheory.Elementwise
-import Mathlib.Algebra.Category.Ring.Colimits
 import Mathlib.CategoryTheory.Sites.Pullback
+import Mathlib.Tactic.CategoryTheory.Elementwise
+import Mathlib.Tactic.Rename
+import Mathlib.Topology.Category.TopCat.OpenNhds
+import Mathlib.Topology.Sheaves.Presheaf
+import Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
 
 /-!
 # Stalks
diff --git a/Mathlib/Topology/UniformSpace/Equicontinuity.lean b/Mathlib/Topology/UniformSpace/Equicontinuity.lean
index f3cca9f71ccdf..a03d6bdee3879 100644
--- a/Mathlib/Topology/UniformSpace/Equicontinuity.lean
+++ b/Mathlib/Topology/UniformSpace/Equicontinuity.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
+import Mathlib.Tactic.CongrM
 import Mathlib.Topology.UniformSpace.UniformConvergenceTopology
 
 /-!