RFC chore: do not import Tactic.Common in Mathlib

I went through the whole of Mathlib and replaced all imports of `Tactic.Common` with a more specialized file. I'm not sure if this is the right way to go, since it seems rather annoying to have to explicitly import basic tactics. But it should reduce some of the noise when testing how to split imports.

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

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

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

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

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

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
 
 /-!

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

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

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

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

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`

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

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

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

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

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

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.

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

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.

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

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

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

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.

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

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

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

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

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

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

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`

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

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

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
 
 /-!

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
 
 /-!

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

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

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.

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

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

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

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

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

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

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

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