diff --git a/Mathlib.lean b/Mathlib.lean
index c62cba6f5f9743..76b7ec63f136f7 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -7095,6 +7095,7 @@ public import Mathlib.Tactic.Contrapose
 public import Mathlib.Tactic.Conv
 public import Mathlib.Tactic.Convert
 public import Mathlib.Tactic.Core
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.DSimpPercent
 public import Mathlib.Tactic.DeclarationNames
 public import Mathlib.Tactic.DefEqAbuse
@@ -7311,7 +7312,6 @@ public import Mathlib.Tactic.Simps.Basic
 public import Mathlib.Tactic.Simps.NotationClass
 public import Mathlib.Tactic.SplitIfs
 public import Mathlib.Tactic.Spread
-public import Mathlib.Tactic.StacksAttribute
 public import Mathlib.Tactic.Subsingleton
 public import Mathlib.Tactic.Substs
 public import Mathlib.Tactic.SuccessIfFailWithMsg
diff --git a/Mathlib/Algebra/Ring/Defs.lean b/Mathlib/Algebra/Ring/Defs.lean
index ac636d5b9c3ef7..2c2a9eb9aecfb6 100644
--- a/Mathlib/Algebra/Ring/Defs.lean
+++ b/Mathlib/Algebra/Ring/Defs.lean
@@ -7,8 +7,8 @@ module
 
 public import Mathlib.Algebra.GroupWithZero.Defs
 public import Mathlib.Data.Int.Cast.Defs
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.Spread
-public import Mathlib.Tactic.StacksAttribute
 
 /-!
 # Semirings and rings
diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
index eb34b6f6a0f3a3..1a55f91f20c3e1 100644
--- a/Mathlib/CategoryTheory/Category/Basic.lean
+++ b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -8,8 +8,8 @@ module
 public import Mathlib.CategoryTheory.Category.Init
 public import Mathlib.Combinatorics.Quiver.Basic
 public import Mathlib.Tactic.PPWithUniv
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.Common
-public import Mathlib.Tactic.StacksAttribute
 public import Mathlib.Tactic.TryThis
 
 /-!
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
index 76ed51fa7c0677..f127f12741db40 100644
--- a/Mathlib/Tactic.lean
+++ b/Mathlib/Tactic.lean
@@ -74,6 +74,7 @@ public import Mathlib.Tactic.Contrapose
 public import Mathlib.Tactic.Conv
 public import Mathlib.Tactic.Convert
 public import Mathlib.Tactic.Core
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.DSimpPercent
 public import Mathlib.Tactic.DeclarationNames
 public import Mathlib.Tactic.DefEqAbuse
@@ -290,7 +291,6 @@ public import Mathlib.Tactic.Simps.Basic
 public import Mathlib.Tactic.Simps.NotationClass
 public import Mathlib.Tactic.SplitIfs
 public import Mathlib.Tactic.Spread
-public import Mathlib.Tactic.StacksAttribute
 public import Mathlib.Tactic.Subsingleton
 public import Mathlib.Tactic.Substs
 public import Mathlib.Tactic.SuccessIfFailWithMsg
diff --git a/Mathlib/Tactic/StacksAttribute.lean b/Mathlib/Tactic/CrossRefAttribute.lean
similarity index 100%
rename from Mathlib/Tactic/StacksAttribute.lean
rename to Mathlib/Tactic/CrossRefAttribute.lean
diff --git a/Mathlib/Topology/Irreducible.lean b/Mathlib/Topology/Irreducible.lean
index 3f2128895bb2d6..eae92e4ab9ec88 100644
--- a/Mathlib/Topology/Irreducible.lean
+++ b/Mathlib/Topology/Irreducible.lean
@@ -8,8 +8,8 @@ module
 public import Mathlib.Order.Minimal
 public import Mathlib.Order.Zorn
 public import Mathlib.Topology.ContinuousOn
-public import Mathlib.Tactic.StacksAttribute
 public import Mathlib.Topology.DiscreteSubset
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Irreducibility in topological spaces
diff --git a/Mathlib/Topology/JacobsonSpace.lean b/Mathlib/Topology/JacobsonSpace.lean
index e7382bf2182581..582242e789be61 100644
--- a/Mathlib/Topology/JacobsonSpace.lean
+++ b/Mathlib/Topology/JacobsonSpace.lean
@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Topology.LocalAtTarget
 public import Mathlib.Topology.Separation.Regular
-public import Mathlib.Tactic.StacksAttribute
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 
diff --git a/Mathlib/Topology/Separation/Basic.lean b/Mathlib/Topology/Separation/Basic.lean
index dcb639f75d119e..e357eafb2d8345 100644
--- a/Mathlib/Topology/Separation/Basic.lean
+++ b/Mathlib/Topology/Separation/Basic.lean
@@ -11,7 +11,7 @@ public import Mathlib.Topology.Piecewise
 public import Mathlib.Topology.Separation.SeparatedNhds
 public import Mathlib.Topology.Compactness.LocallyCompact
 public import Mathlib.Topology.Bases
-public import Mathlib.Tactic.StacksAttribute
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Separation properties of topological spaces
diff --git a/Mathlib/Topology/Separation/Regular.lean b/Mathlib/Topology/Separation/Regular.lean
index 99c5afbb75e764..374b1b9bff07b7 100644
--- a/Mathlib/Topology/Separation/Regular.lean
+++ b/Mathlib/Topology/Separation/Regular.lean
@@ -5,10 +5,10 @@ Authors: Johannes Hölzl, Mario Carneiro
 -/
 module
 
-public import Mathlib.Tactic.StacksAttribute
 public import Mathlib.Topology.Compactness.Lindelof
 public import Mathlib.Topology.Separation.Hausdorff
 public import Mathlib.Topology.Connected.Clopen
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Regular, normal, T₃, T₄ and T₅ spaces
diff --git a/Mathlib/Topology/Spectral/Hom.lean b/Mathlib/Topology/Spectral/Hom.lean
index cd23ce10dc7437..6415162e93d736 100644
--- a/Mathlib/Topology/Spectral/Hom.lean
+++ b/Mathlib/Topology/Spectral/Hom.lean
@@ -5,9 +5,9 @@ Authors: Yaël Dillies
 -/
 module
 
-public import Mathlib.Tactic.StacksAttribute
 public import Mathlib.Topology.ContinuousMap.Basic
 public import Mathlib.Topology.Maps.Proper.Basic
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Spectral maps
diff --git a/MathlibTest/StacksAttribute.lean b/MathlibTest/CrossRefAttribute.lean
similarity index 98%
rename from MathlibTest/StacksAttribute.lean
rename to MathlibTest/CrossRefAttribute.lean
index 7248cf0408cb19..d56640d62ddfb2 100644
--- a/MathlibTest/StacksAttribute.lean
+++ b/MathlibTest/CrossRefAttribute.lean
@@ -1,4 +1,4 @@
-import Mathlib.Tactic.StacksAttribute
+import Mathlib.Tactic.CrossRefAttribute
 import Mathlib.Util.ParseCommand
 
 /-- info: No tags found. -/