diff --git a/Mathlib.lean b/Mathlib.lean
index c62cba6f5f9743..60b2d927badbb9 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -7311,7 +7311,7 @@ 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.CrossRefAttribute
 public import Mathlib.Tactic.Subsingleton
 public import Mathlib.Tactic.Substs
 public import Mathlib.Tactic.SuccessIfFailWithMsg
diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index 3f6b1f43518fe6..a54fe5caf58e23 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -15,6 +15,7 @@ public import Mathlib.Tactic.MkIffOfInductiveProp
 public import Mathlib.Tactic.OfNat
 public import Mathlib.Data.Nat.Notation
 public import Mathlib.Tactic.Simps.Basic
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Typeclasses for (semi)groups and monoids
@@ -1189,6 +1190,7 @@ with a default so that `a / b = a * b⁻¹` holds by definition.
 Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
 on a type with the minimum proof obligations.
 -/
+@[wikidata Q83478]
 class Group (G : Type u) extends DivInvMonoid G where
   protected inv_mul_cancel : ∀ a : G, a⁻¹ * a = 1
 
diff --git a/Mathlib/Algebra/Ring/Defs.lean b/Mathlib/Algebra/Ring/Defs.lean
index ac636d5b9c3ef7..b4460bc498ee3f 100644
--- a/Mathlib/Algebra/Ring/Defs.lean
+++ b/Mathlib/Algebra/Ring/Defs.lean
@@ -8,7 +8,7 @@ module
 public import Mathlib.Algebra.GroupWithZero.Defs
 public import Mathlib.Data.Int.Cast.Defs
 public import Mathlib.Tactic.Spread
-public import Mathlib.Tactic.StacksAttribute
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Semirings and rings
diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
index eb34b6f6a0f3a3..d99d3ed726ae57 100644
--- a/Mathlib/CategoryTheory/Category/Basic.lean
+++ b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -9,7 +9,7 @@ public import Mathlib.CategoryTheory.Category.Init
 public import Mathlib.Combinatorics.Quiver.Basic
 public import Mathlib.Tactic.PPWithUniv
 public import Mathlib.Tactic.Common
-public import Mathlib.Tactic.StacksAttribute
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.TryThis
 
 /-!
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
index 76ed51fa7c0677..fc22b4577c4f37 100644
--- a/Mathlib/Tactic.lean
+++ b/Mathlib/Tactic.lean
@@ -290,7 +290,7 @@ 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.CrossRefAttribute
 public import Mathlib.Tactic.Subsingleton
 public import Mathlib.Tactic.Substs
 public import Mathlib.Tactic.SuccessIfFailWithMsg
diff --git a/Mathlib/Tactic/CrossRefAttribute.lean b/Mathlib/Tactic/CrossRefAttribute.lean
new file mode 100644
index 00000000000000..09d7ce7de39b32
--- /dev/null
+++ b/Mathlib/Tactic/CrossRefAttribute.lean
@@ -0,0 +1,331 @@
+/-
+Copyright (c) 2024 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+module
+
+public meta import Lean.Elab.Command
+public import Mathlib.Init
+
+/-!
+# Cross-reference attributes
+
+This file provides attributes for tagging Mathlib results with cross-references
+to entries in external mathematical databases:
+
+* `@[stacks TAG]` — [Stacks Project](https://stacks.math.columbia.edu/tags)
+* `@[kerodon TAG]` — [Kerodon](https://kerodon.net/tag/)
+* `@[wikidata QID]` — [Wikidata](https://www.wikidata.org)
+
+Each attribute records the cross-reference in an environment extension and appends
+a link to the declaration's docstring.
+
+The shared infrastructure (`Database`, `Tag`, `tagExt`, `addCrossRefDoc`,
+`traceCrossRefs`) is database-agnostic; per-database code defines a parser, the
+attribute syntax, and the trace command.
+-/
+
+public meta section
+
+open Lean Elab
+
+namespace Mathlib.CrossRef
+
+/-- The supported external databases. -/
+inductive Database where
+  | kerodon
+  | stacks
+  | wikidata
+  deriving BEq, Hashable
+
+/-- The base URL for an external database's tag pages. Always ends with `/`. -/
+def databaseURL : Database → String
+  | .kerodon => "https://kerodon.net/tag/"
+  | .stacks => "https://stacks.math.columbia.edu/tag/"
+  | .wikidata => "https://www.wikidata.org/wiki/"
+
+/-- The display label used in docstring links and trace output. -/
+def databaseName : Database → String
+  | .kerodon => "Kerodon Tag"
+  | .stacks => "Stacks Tag"
+  | .wikidata => "Wikidata"
+
+/-- A cross-reference from a Mathlib declaration to an entry in an external database. -/
+structure Tag where
+  /-- The name of the declaration carrying the cross-reference. -/
+  declName : Name
+  /-- The external database the entry belongs to. -/
+  database : Database
+  /-- The database identifier (a tag string or Q-number). -/
+  tag : String
+  /-- An optional comment supplied with the attribute. -/
+  comment : String
+  deriving BEq, Hashable
+
+/-- The environment extension storing all cross-references.
+`addImportedFn` is a constant function to avoid a performance overhead during initialization. -/
+initialize tagExt : SimplePersistentEnvExtension Tag (Array (Array Tag)) ←
+  registerSimplePersistentEnvExtension {
+    addImportedFn tags := tags
+    addEntryFn tags _ := tags
+  }
+
+/--
+`addTagEntry declName db tag comment` records a cross-reference for `declName` in `tagExt`.
+-/
+def addTagEntry {m : Type → Type} [MonadEnv m]
+    (declName : Name) (db : Database) (tag comment : String) : m Unit :=
+  modifyEnv (tagExt.addEntry ·
+    { declName := declName, database := db, tag := tag, comment := comment })
+
+/-- Append a cross-reference link to the docstring of `decl` and record it in `tagExt`.
+This is the database-agnostic core of every cross-reference attribute's `add` handler. -/
+def addCrossRefDoc (db : Database) (decl : Name) (idStr comment : String) : CoreM Unit := do
+  let oldDoc := (← findDocString? (← getEnv) decl).getD ""
+  let commentInDoc := if comment.isEmpty then "" else s!" ({comment})"
+  let link := s!"[{databaseName db} {idStr}]({databaseURL db}{idStr}){commentInDoc}"
+  addDocStringCore decl <| "\n\n".intercalate ([oldDoc, link].filter (· != ""))
+  addTagEntry decl db idStr comment
+
+open Parser
+
+/-! ### Stacks (and Kerodon) parser -/
+
+/-- `stacksTag` is the node kind of Stacks Project Tags: a sequence of digits and
+uppercase letters. -/
+abbrev stacksTagKind : SyntaxNodeKind := `stacksTag
+
+/-- The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or
+uppercase letters. -/
+def stacksTagFn : ParserFn := fun c s =>
+  let i := s.pos
+  let s := takeWhileFn (fun c => c.isAlphanum) c s
+  if s.hasError then
+    s
+  else if s.pos == i then
+    ParserState.mkError s "stacks tag"
+  else
+    let tag := c.extract i s.pos
+    if !tag.all fun (c : Char) => c.isDigit || c.isUpper then
+      ParserState.mkUnexpectedError s
+        "Stacks tags must consist only of digits and uppercase letters."
+    else if tag.length != 4 then
+      ParserState.mkUnexpectedError s "Stacks tags must be exactly 4 characters"
+    else
+      mkNodeToken stacksTagKind i true c s
+
+@[inherit_doc stacksTagFn]
+def stacksTagNoAntiquot : Parser := {
+  fn   := stacksTagFn
+  info := mkAtomicInfo "stacksTag"
+}
+
+@[inherit_doc stacksTagFn]
+def stacksTagParser : Parser :=
+  withAntiquot (mkAntiquot "stacksTag" stacksTagKind) stacksTagNoAntiquot
+
+/-! ### Wikidata parser -/
+
+/-- `wikidataId` is the node kind of Wikidata identifiers: the letter `Q` followed by digits. -/
+abbrev wikidataIdKind : SyntaxNodeKind := `wikidataId
+
+/-- The main parser for Wikidata identifiers: it accepts `Q` followed by one or more digits. -/
+def wikidataIdFn : ParserFn := fun c s =>
+  let i := s.pos
+  let s := takeWhileFn (fun c => c.isAlphanum) c s
+  if s.hasError then
+    s
+  else if s.pos == i then
+    ParserState.mkError s "wikidata id"
+  else
+    let id := c.extract i s.pos
+    match id.toList with
+    | 'Q' :: rest@(_ :: _) =>
+      if rest.all Char.isDigit then
+        mkNodeToken wikidataIdKind i true c s
+      else
+        ParserState.mkUnexpectedError s
+          "Wikidata ids must consist of the letter Q followed by digits."
+    | _ =>
+      ParserState.mkUnexpectedError s
+        "Wikidata ids must start with the letter Q followed by one or more digits."
+
+@[inherit_doc wikidataIdFn]
+def wikidataIdNoAntiquot : Parser := {
+  fn   := wikidataIdFn
+  info := mkAtomicInfo "wikidataId"
+}
+
+@[inherit_doc wikidataIdFn]
+def wikidataIdParser : Parser :=
+  withAntiquot (mkAntiquot "wikidataId" wikidataIdKind) wikidataIdNoAntiquot
+
+end Mathlib.CrossRef
+
+open Mathlib.CrossRef
+
+/-- Extract the underlying tag as a string from a `stacksTag` node. -/
+def Lean.TSyntax.getStacksTag (stx : TSyntax stacksTagKind) : CoreM String := do
+  let some val := Syntax.isLit? stacksTagKind stx | throwError "Malformed Stacks tag"
+  return val
+
+/-- Extract the underlying identifier as a string from a `wikidataId` node. -/
+def Lean.TSyntax.getWikidataId (stx : TSyntax wikidataIdKind) : CoreM String := do
+  let some val := Syntax.isLit? wikidataIdKind stx | throwError "Malformed Wikidata id"
+  return val
+
+namespace Lean.PrettyPrinter
+
+namespace Formatter
+
+/-- The formatter for Stacks Project Tags syntax. -/
+@[combinator_formatter stacksTagNoAntiquot] def stacksTagNoAntiquot.formatter :=
+  visitAtom stacksTagKind
+
+/-- The formatter for Wikidata identifier syntax. -/
+@[combinator_formatter wikidataIdNoAntiquot] def wikidataIdNoAntiquot.formatter :=
+  visitAtom wikidataIdKind
+
+end Formatter
+
+namespace Parenthesizer
+
+/-- The parenthesizer for Stacks Project Tags syntax. -/
+@[combinator_parenthesizer stacksTagNoAntiquot] def stacksTagAntiquot.parenthesizer := visitToken
+
+/-- The parenthesizer for Wikidata identifier syntax. -/
+@[combinator_parenthesizer wikidataIdNoAntiquot] def wikidataIdAntiquot.parenthesizer := visitToken
+
+end Lean.PrettyPrinter.Parenthesizer
+
+namespace Mathlib.CrossRef
+
+/-! ### Stacks / Kerodon attribute -/
+
+/-- The syntax category for the database name. -/
+declare_syntax_cat stacksTagDB
+
+/-- The syntax for a "kerodon" database identifier in a `@[kerodon]` attribute. -/
+syntax "kerodon" : stacksTagDB
+/-- The syntax for a "stacks" database identifier in a `@[stacks]` attribute. -/
+syntax "stacks" : stacksTagDB
+
+/-- The `stacksTag` attribute.
+Use it as `@[kerodon TAG "Optional comment"]` or `@[stacks TAG "Optional comment"]`
+depending on the database you are referencing.
+
+The `TAG` is mandatory and should be a sequence of 4 digits or uppercase letters.
+
+See the [Tags page](https://stacks.math.columbia.edu/tags) in the Stacks project or
+[Tags page](https://kerodon.net/tag/) in the Kerodon project for more details.
+-/
+syntax (name := stacksTag) stacksTagDB stacksTagParser (ppSpace str)? : attr
+
+initialize Lean.registerBuiltinAttribute {
+  name := `stacksTag
+  descr := "Apply a Stacks or Kerodon project tag to a theorem."
+  add := fun decl stx _attrKind => do
+    let (db, tag, comment) := ← match stx with
+      | `(attr| stacks $tag $[$comment]?) => return (Database.stacks, tag, comment)
+      | `(attr| kerodon $tag $[$comment]?) => return (Database.kerodon, tag, comment)
+      | _ => throwUnsupportedSyntax
+    addCrossRefDoc db decl (← tag.getStacksTag) ((comment.map (·.getString)).getD "")
+  -- docstrings are immutable once an asynchronous elaboration task has been started
+  applicationTime := .beforeElaboration
+}
+
+/-! ### Wikidata attribute -/
+
+/-- The `wikidata` attribute.
+Use it as `@[wikidata Q12345 "Optional comment"]` to associate a Mathlib declaration with
+the corresponding [Wikidata](https://www.wikidata.org) item.
+
+The identifier must be the letter `Q` followed by one or more digits.
+-/
+syntax (name := wikidataTag) "wikidata" wikidataIdParser (ppSpace str)? : attr
+
+initialize Lean.registerBuiltinAttribute {
+  name := `wikidataTag
+  descr := "Apply a Wikidata identifier to a declaration."
+  add := fun decl stx _attrKind => do
+    let (id, comment) := ← match stx with
+      | `(attr| wikidata $id $[$comment]?) => return (id, comment)
+      | _ => throwUnsupportedSyntax
+    addCrossRefDoc .wikidata decl (← id.getWikidataId) ((comment.map (·.getString)).getD "")
+  -- docstrings are immutable once an asynchronous elaboration task has been started
+  applicationTime := .beforeElaboration
+}
+
+end Mathlib.CrossRef
+
+/-- Returns the array of `Tag`s in the environment, sorted alphabetically by tag. -/
+private def Lean.Environment.getSortedCrossRefs (env : Environment) : Array Tag :=
+  let tags := PersistentEnvExtension.getState tagExt env
+  tags.2.flatten.appendList tags.1 |>.qsort (·.tag < ·.tag)
+
+/-- Returns the declaration names of results carrying the cross-reference `tag`. -/
+private def Lean.Environment.getCrossRefDeclNames (env : Environment) (tag : String) :
+    Array Name :=
+  env.getSortedCrossRefs.filterMap fun d => if d.tag == tag then some d.declName else none
+
+namespace Mathlib.CrossRef
+
+/-- `traceCrossRefs db verbose` prints the cross-references of database `db` and
+inlines the declaration types if `verbose` is `true`. -/
+def traceCrossRefs (db : Database) (verbose : Bool := false) :
+    Command.CommandElabM Unit := do
+  let env ← getEnv
+  let entries := env.getSortedCrossRefs |>.filter (·.database == db)
+  if entries.isEmpty then logInfo "No tags found." else
+  let mut msgs := #[m!""]
+  for d in entries do
+    let (parL, parR) := if d.comment.isEmpty then ("", "") else (" (", ")")
+    let cmt := parL ++ d.comment ++ parR
+    msgs := msgs.push
+      m!"[{databaseName db} {d.tag}]({databaseURL db ++ d.tag}) \
+        corresponds to declaration '{.ofConstName d.declName}'.{cmt}"
+    if verbose then
+      let dType := ((env.find? d.declName).getD default).type
+      msgs := (msgs.push m!"{dType}").push ""
+  let msg := MessageData.joinSep msgs.toList "\n"
+  logInfo msg
+
+/--
+`#stacks_tags` retrieves all declarations that have the `stacks` attribute.
+
+For each found declaration, it prints a line
+```
+'declaration_name' corresponds to tag 'declaration_tag'.
+```
+The variant `#stacks_tags!` also adds the theorem statement (for theorems)
+or declaration type (for definitions, structures, instances, etc.) after each summary line.
+-/
+elab (name := stacksTags) "#stacks_tags" tk:("!")? : command =>
+  traceCrossRefs .stacks (tk.isSome)
+
+/-- The `#kerodon_tags` command retrieves all declarations that have the `kerodon` attribute.
+
+For each found declaration, it prints a line
+```
+'declaration_name' corresponds to tag 'declaration_tag'.
+```
+The variant `#kerodon_tags!` also adds the theorem statement (for theorems)
+or declaration type (for definitions, structures, instances, etc.) after each summary line.
+-/
+elab (name := kerodonTags) "#kerodon_tags" tk:("!")? : command =>
+  traceCrossRefs .kerodon (tk.isSome)
+
+/-- The `#wikidata_tags` command retrieves all declarations that have the `wikidata` attribute.
+
+For each found declaration, it prints a line
+```
+'declaration_name' corresponds to tag 'declaration_tag'.
+```
+The variant `#wikidata_tags!` also adds the theorem statement (for theorems)
+or declaration type (for definitions, structures, instances, etc.) after each summary line.
+-/
+elab (name := wikidataTags) "#wikidata_tags" tk:("!")? : command =>
+  traceCrossRefs .wikidata (tk.isSome)
+
+end Mathlib.CrossRef
diff --git a/Mathlib/Tactic/StacksAttribute.lean b/Mathlib/Tactic/StacksAttribute.lean
deleted file mode 100644
index a6a179742baff6..00000000000000
--- a/Mathlib/Tactic/StacksAttribute.lean
+++ /dev/null
@@ -1,241 +0,0 @@
-/-
-Copyright (c) 2024 Damiano Testa. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Damiano Testa
--/
-module
-
-public meta import Lean.Elab.Command
-public import Mathlib.Init
-
-/-!
-# The `stacks` and `kerodon` attributes
-
-This allows tagging of mathlib results with the corresponding
-tags from the [Stacks Project](https://stacks.math.columbia.edu/tags) and
-[Kerodon](https://kerodon.net/tag/).
-
-While the Stacks Project is the main focus, because the tag format at Kerodon is
-compatible, the attribute can be used to tag results with Kerodon tags as well.
--/
-
-public meta section
-
-open Lean Elab
-
-namespace Mathlib.StacksTag
-
-/-- Web database users of projects tags -/
-inductive Database where
-  | kerodon
-  | stacks
-  deriving BEq, Hashable
-
-/-- `Tag` is the structure that carries the data of a project tag and a corresponding
-Mathlib declaration. -/
-structure Tag where
-  /-- The name of the declaration with the given tag. -/
-  declName : Name
-  /-- The online database where the tag is found. -/
-  database : Database
-  /-- The database tag. -/
-  tag : String
-  /-- The (optional) comment that comes with the given tag. -/
-  comment : String
-  deriving BEq, Hashable
-
-/-- Defines the `tagExt` extension for storing all `Tag`s in the environment.
-`addImportedFn` is a constant function to avoid a performance overhead during initialization. -/
-initialize tagExt : SimplePersistentEnvExtension Tag (Array (Array Tag)) ←
-  registerSimplePersistentEnvExtension {
-    addImportedFn tags := tags
-    addEntryFn tags _ := tags
-  }
-
-/--
-`addTagEntry declName db tag comment` takes as input the `Name` `declName` of a declaration,
-whether it is a Kerodon or Stacks tag (`db`) and
-the `String`s `tag` and `comment` of the `stacks` or `kerodon` attribute.
-It extends the `Tag` environment extension with the data `declName, db, tag, comment`.
--/
-def addTagEntry {m : Type → Type} [MonadEnv m]
-    (declName : Name) (db : Database) (tag comment : String) : m Unit :=
-  modifyEnv (tagExt.addEntry ·
-    { declName := declName, database := db, tag := tag, comment := comment })
-
-open Parser
-
-/-- `stacksTag` is the node kind of Stacks Project Tags: a sequence of digits and
-uppercase letters. -/
-abbrev stacksTagKind : SyntaxNodeKind := `stacksTag
-
-/-- The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or
-uppercase letters. -/
-def stacksTagFn : ParserFn := fun c s =>
-  let i := s.pos
-  let s := takeWhileFn (fun c => c.isAlphanum) c s
-  if s.hasError then
-    s
-  else if s.pos == i then
-    ParserState.mkError s "stacks tag"
-  else
-    let tag := c.extract i s.pos
-    if !tag.all fun (c : Char) => c.isDigit || c.isUpper then
-      ParserState.mkUnexpectedError s
-        "Stacks tags must consist only of digits and uppercase letters."
-    else if tag.length != 4 then
-      ParserState.mkUnexpectedError s "Stacks tags must be exactly 4 characters"
-    else
-      mkNodeToken stacksTagKind i true c s
-
-@[inherit_doc stacksTagFn]
-def stacksTagNoAntiquot : Parser := {
-  fn   := stacksTagFn
-  info := mkAtomicInfo "stacksTag"
-}
-
-@[inherit_doc stacksTagFn]
-def stacksTagParser : Parser :=
-  withAntiquot (mkAntiquot "stacksTag" stacksTagKind) stacksTagNoAntiquot
-
-end Mathlib.StacksTag
-
-open Mathlib.StacksTag
-
-/-- Extract the underlying tag as a string from a `stacksTag` node. -/
-def Lean.TSyntax.getStacksTag (stx : TSyntax stacksTagKind) : CoreM String := do
-  let some val := Syntax.isLit? stacksTagKind stx | throwError "Malformed Stacks tag"
-  return val
-
-namespace Lean.PrettyPrinter
-
-namespace Formatter
-
-/-- The formatter for Stacks Project Tags syntax. -/
-@[combinator_formatter stacksTagNoAntiquot] def stacksTagNoAntiquot.formatter :=
-  visitAtom stacksTagKind
-
-end Formatter
-
-namespace Parenthesizer
-
-/-- The parenthesizer for Stacks Project Tags syntax. -/
-@[combinator_parenthesizer stacksTagNoAntiquot] def stacksTagAntiquot.parenthesizer := visitToken
-
-end Lean.PrettyPrinter.Parenthesizer
-
-namespace Mathlib.StacksTag
-
-/-- The syntax category for the database name. -/
-declare_syntax_cat stacksTagDB
-
-/-- The syntax for a "kerodon" database identifier in a `@[kerodon]` attribute. -/
-syntax "kerodon" : stacksTagDB
-/-- The syntax for a "stacks" database identifier in a `@[stacks]` attribute. -/
-syntax "stacks" : stacksTagDB
-
-/-- The `stacksTag` attribute.
-Use it as `@[kerodon TAG "Optional comment"]` or `@[stacks TAG "Optional comment"]`
-depending on the database you are referencing.
-
-The `TAG` is mandatory and should be a sequence of 4 digits or uppercase letters.
-
-See the [Tags page](https://stacks.math.columbia.edu/tags) in the Stacks project or
-[Tags page](https://kerodon.net/tag/) in the Kerodon project for more details.
--/
-syntax (name := stacksTag) stacksTagDB stacksTagParser (ppSpace str)? : attr
-
-initialize Lean.registerBuiltinAttribute {
-  name := `stacksTag
-  descr := "Apply a Stacks or Kerodon project tag to a theorem."
-  add := fun decl stx _attrKind => do
-    let oldDoc := (← findDocString? (← getEnv) decl).getD ""
-    let (SorK, database, url, tag, comment) := ← match stx with
-      | `(attr| stacks $tag $[$comment]?) =>
-        return ("Stacks", Database.stacks, "https://stacks.math.columbia.edu/tag", tag, comment)
-      | `(attr| kerodon $tag $[$comment]?) =>
-        return ("Kerodon", Database.kerodon, "https://kerodon.net/tag", tag, comment)
-      | _ => throwUnsupportedSyntax
-    let tagStr ← tag.getStacksTag
-    let comment := (comment.map (·.getString)).getD ""
-    let commentInDoc := if comment = "" then "" else s!" ({comment})"
-    let newDoc := [oldDoc, s!"[{SorK} Tag {tagStr}]({url}/{tagStr}){commentInDoc}"]
-    addDocStringCore decl <| "\n\n".intercalate (newDoc.filter (· != ""))
-    addTagEntry decl database tagStr <| comment
-  -- docstrings are immutable once an asynchronous elaboration task has been started
-  applicationTime := .beforeElaboration
-}
-
-end Mathlib.StacksTag
-
-/--
-`getSortedStackProjectTags env` returns the array of `Tags`, sorted by alphabetical order of tag.
--/
-private def Lean.Environment.getSortedStackProjectTags (env : Environment) : Array Tag :=
-  let tags := PersistentEnvExtension.getState tagExt env
-  tags.2.flatten.appendList tags.1 |>.qsort (·.tag < ·.tag)
-
-/--
-`getSortedStackProjectDeclNames env tag` returns the array of declaration names of results
-with Stacks Project tag equal to `tag`.
--/
-private def Lean.Environment.getSortedStackProjectDeclNames (env : Environment) (tag : String) :
-    Array Name :=
-  let tags := env.getSortedStackProjectTags
-  tags.filterMap fun d => if d.tag == tag then some d.declName else none
-
-namespace Mathlib.StacksTag
-
-private def databaseURL (db : Database) : String :=
-  match db with
-  | .kerodon => "https://kerodon.net/tag/"
-  | .stacks => "https://stacks.math.columbia.edu/tag/"
-
-/--
-`traceStacksTags db verbose` prints the tags of the database `db` to the user and
-inlines the theorem statements if `verbose` is `true`.
--/
-def traceStacksTags (db : Database) (verbose : Bool := false) :
-    Command.CommandElabM Unit := do
-  let env ← getEnv
-  let entries := env.getSortedStackProjectTags |>.filter (·.database == db)
-  if entries.isEmpty then logInfo "No tags found." else
-  let mut msgs := #[m!""]
-  for d in entries do
-    let (parL, parR) := if d.comment.isEmpty then ("", "") else (" (", ")")
-    let cmt := parL ++ d.comment ++ parR
-    msgs := msgs.push
-      m!"[Stacks Tag {d.tag}]({databaseURL db ++ d.tag}) \
-        corresponds to declaration '{.ofConstName d.declName}'.{cmt}"
-    if verbose then
-      let dType := ((env.find? d.declName).getD default).type
-      msgs := (msgs.push m!"{dType}").push ""
-  let msg := MessageData.joinSep msgs.toList "\n"
-  logInfo msg
-
-/--
-`#stacks_tags` retrieves all declarations that have the `stacks` attribute.
-
-For each found declaration, it prints a line
-```
-'declaration_name' corresponds to tag 'declaration_tag'.
-```
-The variant `#stacks_tags!` also adds the theorem statement (for theorems)
-or declaration type (for definitions, structures, instances, etc.) after each summary line.
--/
-elab (name := stacksTags) "#stacks_tags" tk:("!")? : command =>
-  traceStacksTags .stacks (tk.isSome)
-
-/-- The `#kerodon_tags` command retrieves all declarations that have the `kerodon` attribute.
-
-For each found declaration, it prints a line
-```
-'declaration_name' corresponds to tag 'declaration_tag'.
-```
-The variant `#kerodon_tags!` also adds the theorem statement (for theorems)
-or declaration type (for definitions, structures, instances, etc.) after each summary line.
--/
-elab (name := kerodonTags) "#kerodon_tags" tk:("!")? : command =>
-  traceStacksTags .kerodon (tk.isSome)
-
-end Mathlib.StacksTag
diff --git a/Mathlib/Topology/Irreducible.lean b/Mathlib/Topology/Irreducible.lean
index 3f2128895bb2d6..11a2fbfa9ef7aa 100644
--- a/Mathlib/Topology/Irreducible.lean
+++ b/Mathlib/Topology/Irreducible.lean
@@ -8,7 +8,7 @@ module
 public import Mathlib.Order.Minimal
 public import Mathlib.Order.Zorn
 public import Mathlib.Topology.ContinuousOn
-public import Mathlib.Tactic.StacksAttribute
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Topology.DiscreteSubset
 
 /-!
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..adfa5ceb50ec86 100644
--- a/Mathlib/Topology/Separation/Regular.lean
+++ b/Mathlib/Topology/Separation/Regular.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 -/
 module
 
-public import Mathlib.Tactic.StacksAttribute
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Topology.Compactness.Lindelof
 public import Mathlib.Topology.Separation.Hausdorff
 public import Mathlib.Topology.Connected.Clopen
diff --git a/Mathlib/Topology/Spectral/Hom.lean b/Mathlib/Topology/Spectral/Hom.lean
index cd23ce10dc7437..ab98289c10eb41 100644
--- a/Mathlib/Topology/Spectral/Hom.lean
+++ b/Mathlib/Topology/Spectral/Hom.lean
@@ -5,7 +5,7 @@ Authors: Yaël Dillies
 -/
 module
 
-public import Mathlib.Tactic.StacksAttribute
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Topology.ContinuousMap.Basic
 public import Mathlib.Topology.Maps.Proper.Basic
 
diff --git a/MathlibTest/StacksAttribute.lean b/MathlibTest/CrossRefAttribute.lean
similarity index 86%
rename from MathlibTest/StacksAttribute.lean
rename to MathlibTest/CrossRefAttribute.lean
index 7248cf0408cb19..35b93262ae40d0 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. -/
@@ -38,13 +38,13 @@ example : True := .intro
 example : True := .intro
 
 /-- error: <input>:1:3: Stacks tags must be exactly 4 characters -/
-#guard_msgs in #parse Mathlib.StacksTag.stacksTagFn => "A05"
+#guard_msgs in #parse Mathlib.CrossRef.stacksTagFn => "A05"
 
 /-- error: <input>:1:4: Stacks tags must consist only of digits and uppercase letters. -/
-#guard_msgs in #parse Mathlib.StacksTag.stacksTagFn => "A05b"
+#guard_msgs in #parse Mathlib.CrossRef.stacksTagFn => "A05b"
 
 /-- info: 0BD5 -/
-#guard_msgs in #parse Mathlib.StacksTag.stacksTagFn => "0BD5"
+#guard_msgs in #parse Mathlib.CrossRef.stacksTagFn => "0BD5"
 
 /--
 info:
@@ -63,7 +63,7 @@ True
 
 /--
 info:
-[Stacks Tag B15R](https://kerodon.net/tag/B15R) corresponds to declaration 'X.tagged'. (Also a comment)
+[Kerodon Tag B15R](https://kerodon.net/tag/B15R) corresponds to declaration 'X.tagged'. (Also a comment)
 True
 -/
 #guard_msgs in
@@ -71,7 +71,7 @@ True
 
 section errors
 
-open Lean Parser Mathlib.StacksTag
+open Lean Parser Mathlib.CrossRef
 
 def captureException (env : Environment) (s : ParserFn) (input : String) : Except String Syntax :=
   let ictx := mkInputContext input "<input>"
diff --git a/scripts/noshake.json b/scripts/noshake.json
index abdbf6f15988c4..d4075533047b12 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -170,7 +170,7 @@
   "Mathlib.Tactic.Simps.NotationClass",
   "Mathlib.Tactic.SplitIfs",
   "Mathlib.Tactic.Spread",
-  "Mathlib.Tactic.StacksAttribute",
+  "Mathlib.Tactic.CrossRefAttribute",
   "Mathlib.Tactic.Substs",
   "Mathlib.Tactic.SuppressCompilation",
   "Mathlib.Tactic.SwapVar",