chore(Tactic): abstract over Stacks attribute, add Wikidata attribute

[jcommelin]

This PR abstracts some of the functionality that sets up the Stacks attribute, and uses the new abstraction to add a Wikidata attribute.

Co-authored with Claude Code.

---

• depends on: [Merged by Bors] - chore(Tactic): move StacksAttribute to CrossRefAttribute #39257

[github-actions]

PR summary 53f8a93a77

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.StacksAttribute	54	0	-54 (-100.00%)

Import changes for all files

Files	Import difference
Mathlib.Tactic.StacksAttribute	-54
797 files Mathlib.Algebra.AddTorsor.Basic Mathlib.Algebra.AddTorsor.Defs Mathlib.Algebra.AffineMonoid.Basic Mathlib.Algebra.AffineMonoid.Irreducible Mathlib.Algebra.BigOperators.Group.Finset.Basic Mathlib.Algebra.BigOperators.Group.Finset.Defs Mathlib.Algebra.BigOperators.Group.Finset.Gaps Mathlib.Algebra.BigOperators.Group.Finset.Indicator Mathlib.Algebra.BigOperators.Group.Finset.Lemmas Mathlib.Algebra.BigOperators.Group.Finset.Pi Mathlib.Algebra.BigOperators.Group.Finset.Piecewise Mathlib.Algebra.BigOperators.Group.Finset.Powerset Mathlib.Algebra.BigOperators.Group.Finset.Preimage Mathlib.Algebra.BigOperators.Group.Finset.Sigma Mathlib.Algebra.BigOperators.Group.List.Basic Mathlib.Algebra.BigOperators.Group.List.Defs Mathlib.Algebra.BigOperators.Group.List.Lemmas Mathlib.Algebra.BigOperators.Group.Multiset.Basic Mathlib.Algebra.BigOperators.Group.Multiset.Defs Mathlib.Algebra.BigOperators.GroupWithZero.Finset Mathlib.Algebra.BigOperators.NatAntidiagonal Mathlib.Algebra.BigOperators.Option Mathlib.Algebra.BigOperators.Sym Mathlib.Algebra.CharZero.Defs Mathlib.Algebra.CharZero.Infinite Mathlib.Algebra.Divisibility.Basic Mathlib.Algebra.Divisibility.Finite Mathlib.Algebra.Divisibility.Hom Mathlib.Algebra.Divisibility.Prod Mathlib.Algebra.Divisibility.Units Mathlib.Algebra.FiniteSupport.Basic Mathlib.Algebra.FreeMonoid.Basic Mathlib.Algebra.FreeMonoid.Count Mathlib.Algebra.FreeMonoid.FreeSemigroup Mathlib.Algebra.FreeMonoid.Symbols Mathlib.Algebra.FreeMonoid.UniqueProds Mathlib.Algebra.Free Mathlib.Algebra.GradedMonoid Mathlib.Algebra.GradedMulAction Mathlib.Algebra.Group.Action.Basic Mathlib.Algebra.Group.Action.Defs Mathlib.Algebra.Group.Action.End Mathlib.Algebra.Group.Action.Equidecomp Mathlib.Algebra.Group.Action.Faithful Mathlib.Algebra.Group.Action.Hom Mathlib.Algebra.Group.Action.Opposite Mathlib.Algebra.Group.Action.Option Mathlib.Algebra.Group.Action.Pi Mathlib.Algebra.Group.Action.Pointwise.Finset Mathlib.Algebra.Group.Action.Pointwise.Set.Basic Mathlib.Algebra.Group.Action.Pointwise.Set.Finite Mathlib.Algebra.Group.Action.Pretransitive Mathlib.Algebra.Group.Action.Prod Mathlib.Algebra.Group.Action.Sigma Mathlib.Algebra.Group.Action.Sum Mathlib.Algebra.Group.Action.TransferInstance Mathlib.Algebra.Group.Action.TypeTags Mathlib.Algebra.Group.Action.Units Mathlib.Algebra.Group.Basic Mathlib.Algebra.Group.Center Mathlib.Algebra.Group.Commutator Mathlib.Algebra.Group.Commute.Basic Mathlib.Algebra.Group.Commute.Defs Mathlib.Algebra.Group.Commute.Hom Mathlib.Algebra.Group.Commute.Units Mathlib.Algebra.Group.Conj Mathlib.Algebra.Group.Defs Mathlib.Algebra.Group.Embedding Mathlib.Algebra.Group.End Mathlib.Algebra.Group.Equiv.Basic Mathlib.Algebra.Group.Equiv.Defs Mathlib.Algebra.Group.Equiv.Finite Mathlib.Algebra.Group.Equiv.Opposite Mathlib.Algebra.Group.Equiv.TypeTags Mathlib.Algebra.Group.Even Mathlib.Algebra.Group.Ext Mathlib.Algebra.Group.Fin.Basic Mathlib.Algebra.Group.Fin.Tuple Mathlib.Algebra.Group.Finsupp Mathlib.Algebra.Group.Graph Mathlib.Algebra.Group.Hom.Basic Mathlib.Algebra.Group.Hom.CompTypeclasses Mathlib.Algebra.Group.Hom.Defs Mathlib.Algebra.Group.Hom.Instances Mathlib.Algebra.Group.Idempotent Mathlib.Algebra.Group.Indicator Mathlib.Algebra.Group.InjSurj Mathlib.Algebra.Group.Int.Defs Mathlib.Algebra.Group.Int.Even Mathlib.Algebra.Group.Int.TypeTags Mathlib.Algebra.Group.Int.Units Mathlib.Algebra.Group.Invertible.Basic Mathlib.Algebra.Group.Invertible.Defs Mathlib.Algebra.Group.Irreducible.Defs Mathlib.Algebra.Group.Irreducible.Indecomposable Mathlib.Algebra.Group.Irreducible.Lemmas Mathlib.Algebra.Group.MinimalAxioms Mathlib.Algebra.Group.ModEq Mathlib.Algebra.Group.Nat.Defs Mathlib.Algebra.Group.Nat.Even Mathlib.Algebra.Group.Nat.Hom Mathlib.Algebra.Group.Nat.Range Mathlib.Algebra.Group.Nat.TypeTags Mathlib.Algebra.Group.Nat.Units Mathlib.Algebra.Group.Opposite Mathlib.Algebra.Group.PUnit Mathlib.Algebra.Group.Pi.Basic Mathlib.Algebra.Group.Pi.Lemmas Mathlib.Algebra.Group.Pi.Units Mathlib.Algebra.Group.Pointwise.Finset.Basic Mathlib.Algebra.Group.Pointwise.Finset.BigOperators Mathlib.Algebra.Group.Pointwise.Finset.Scalar Mathlib.Algebra.Group.Pointwise.Set.Basic Mathlib.Algebra.Group.Pointwise.Set.BigOperators Mathlib.Algebra.Group.Pointwise.Set.Finite Mathlib.Algebra.Group.Pointwise.Set.Lattice Mathlib.Algebra.Group.Pointwise.Set.ListOfFn Mathlib.Algebra.Group.Pointwise.Set.Scalar Mathlib.Algebra.Group.Pointwise.Set.Small Mathlib.Algebra.Group.Prod Mathlib.Algebra.Group.Semiconj.Basic Mathlib.Algebra.Group.Semiconj.Defs Mathlib.Algebra.Group.Semiconj.Units Mathlib.Algebra.Group.Shrink Mathlib.Algebra.Group.Subgroup.Actions Mathlib.Algebra.Group.Subgroup.Basic Mathlib.Algebra.Group.Subgroup.Defs Mathlib.Algebra.Group.Subgroup.Even Mathlib.Algebra.Group.Subgroup.Ker Mathlib.Algebra.Group.Subgroup.Lattice Mathlib.Algebra.Group.Subgroup.Map Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas Mathlib.Algebra.Group.Subgroup.MulOpposite Mathlib.Algebra.Group.Subgroup.Order Mathlib.Algebra.Group.Subgroup.Pointwise Mathlib.Algebra.Group.Subgroup.ZPowers.Basic Mathlib.Algebra.Group.Submonoid.Basic Mathlib.Algebra.Group.Submonoid.BigOperators Mathlib.Algebra.Group.Submonoid.Defs Mathlib.Algebra.Group.Submonoid.DistribMulAction Mathlib.Algebra.Group.Submonoid.Finite Mathlib.Algebra.Group.Submonoid.Membership Mathlib.Algebra.Group.Submonoid.MulAction Mathlib.Algebra.Group.Submonoid.MulOpposite Mathlib.Algebra.Group.Submonoid.Operations Mathlib.Algebra.Group.Submonoid.Pointwise Mathlib.Algebra.Group.Submonoid.Saturation Mathlib.Algebra.Group.Submonoid.Support Mathlib.Algebra.Group.Submonoid.Units Mathlib.Algebra.Group.Subsemigroup.Basic Mathlib.Algebra.Group.Subsemigroup.Defs Mathlib.Algebra.Group.Subsemigroup.Membership Mathlib.Algebra.Group.Subsemigroup.MulOpposite Mathlib.Algebra.Group.Subsemigroup.Operations Mathlib.Algebra.Group.Support Mathlib.Algebra.Group.Torsion Mathlib.Algebra.Group.TransferInstance Mathlib.Algebra.Group.TypeTags.Basic Mathlib.Algebra.Group.TypeTags.Finite Mathlib.Algebra.Group.TypeTags.Hom Mathlib.Algebra.Group.TypeTags.Pointwise Mathlib.Algebra.Group.ULift Mathlib.Algebra.Group.UniqueProds.Basic Mathlib.Algebra.Group.Units.Basic Mathlib.Algebra.Group.Units.Defs Mathlib.Algebra.Group.Units.Equiv Mathlib.Algebra.Group.Units.Hom Mathlib.Algebra.Group.Units.Opposite Mathlib.Algebra.Group.WithOne.Basic Mathlib.Algebra.Group.WithOne.Defs Mathlib.Algebra.Group.WithOne.Map Mathlib.Algebra.GroupWithZero.Action.Basic Mathlib.Algebra.GroupWithZero.Action.Center Mathlib.Algebra.GroupWithZero.Action.ConjAct Mathlib.Algebra.GroupWithZero.Action.Defs Mathlib.Algebra.GroupWithZero.Action.End Mathlib.Algebra.GroupWithZero.Action.Faithful Mathlib.Algebra.GroupWithZero.Action.Hom Mathlib.Algebra.GroupWithZero.Action.Opposite Mathlib.Algebra.GroupWithZero.Action.Pi Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set Mathlib.Algebra.GroupWithZero.Action.Prod Mathlib.Algebra.GroupWithZero.Action.TransferInstance Mathlib.Algebra.GroupWithZero.Action.Units Mathlib.Algebra.GroupWithZero.Associated Mathlib.Algebra.GroupWithZero.Basic Mathlib.Algebra.GroupWithZero.Center Mathlib.Algebra.GroupWithZero.Commute Mathlib.Algebra.GroupWithZero.Conj Mathlib.Algebra.GroupWithZero.Defs Mathlib.Algebra.GroupWithZero.Divisibility Mathlib.Algebra.GroupWithZero.Equiv Mathlib.Algebra.GroupWithZero.Hom Mathlib.Algebra.GroupWithZero.Idempotent Mathlib.Algebra.GroupWithZero.Indicator Mathlib.Algebra.GroupWithZero.InjSurj Mathlib.Algebra.GroupWithZero.Invertible Mathlib.Algebra.GroupWithZero.Nat Mathlib.Algebra.GroupWithZero.NeZero Mathlib.Algebra.GroupWithZero.NonZeroDivisors Mathlib.Algebra.GroupWithZero.Opposite Mathlib.Algebra.GroupWithZero.Pi Mathlib.Algebra.GroupWithZero.Pointwise.Finset Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic Mathlib.Algebra.GroupWithZero.ProdHom Mathlib.Algebra.GroupWithZero.Prod Mathlib.Algebra.GroupWithZero.Range Mathlib.Algebra.GroupWithZero.Regular Mathlib.Algebra.GroupWithZero.Semiconj Mathlib.Algebra.GroupWithZero.Shrink Mathlib.Algebra.GroupWithZero.Subgroup Mathlib.Algebra.GroupWithZero.Submonoid.CancelMulZero Mathlib.Algebra.GroupWithZero.Submonoid.Instances Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise Mathlib.Algebra.GroupWithZero.Submonoid.Primal Mathlib.Algebra.GroupWithZero.TransferInstance Mathlib.Algebra.GroupWithZero.ULift Mathlib.Algebra.GroupWithZero.Units.Basic Mathlib.Algebra.GroupWithZero.Units.Equiv Mathlib.Algebra.GroupWithZero.Units.Lemmas Mathlib.Algebra.GroupWithZero.WithZero Mathlib.Algebra.Homology.ComplexShape Mathlib.Algebra.Homology.HasNoLoop Mathlib.Algebra.Homology.SpectralSequence.ComplexShape Mathlib.Algebra.Module.PointwisePi Mathlib.Algebra.Opposites Mathlib.Algebra.Order.AddGroupWithTop Mathlib.Algebra.Order.AddTorsor Mathlib.Algebra.Order.Antidiag.Prod Mathlib.Algebra.Order.BigOperators.Group.Finset Mathlib.Algebra.Order.BigOperators.Group.List Mathlib.Algebra.Order.BigOperators.Group.Multiset Mathlib.Algebra.Order.BigOperators.GroupWithZero.List Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset Mathlib.Algebra.Order.Field.Pi Mathlib.Algebra.Order.Group.Abs Mathlib.Algebra.Order.Group.Action.End Mathlib.Algebra.Order.Group.Action.Flag Mathlib.Algebra.Order.Group.Action.Synonym Mathlib.Algebra.Order.Group.Action Mathlib.Algebra.Order.Group.Basic Mathlib.Algebra.Order.Group.Bounds Mathlib.Algebra.Order.Group.CompleteLattice Mathlib.Algebra.Order.Group.Cone Mathlib.Algebra.Order.Group.Defs Mathlib.Algebra.Order.Group.DenselyOrdered Mathlib.Algebra.Order.Group.End Mathlib.Algebra.Order.Group.Equiv Mathlib.Algebra.Order.Group.Finset Mathlib.Algebra.Order.Group.Indicator Mathlib.Algebra.Order.Group.Int Mathlib.Algebra.Order.Group.Lattice Mathlib.Algebra.Order.Group.MinMax Mathlib.Algebra.Order.Group.Multiset Mathlib.Algebra.Order.Group.Nat Mathlib.Algebra.Order.Group.Opposite Mathlib.Algebra.Order.Group.OrderIso Mathlib.Algebra.Order.Group.PartialSups Mathlib.Algebra.Order.Group.PiLex Mathlib.Algebra.Order.Group.Pointwise.Bounds Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice Mathlib.Algebra.Order.Group.PosPart Mathlib.Algebra.Order.Group.Synonym Mathlib.Algebra.Order.Group.Unbundled.Abs Mathlib.Algebra.Order.Group.Unbundled.Basic Mathlib.Algebra.Order.Group.Unbundled.Int Mathlib.Algebra.Order.Group.Units Mathlib.Algebra.Order.GroupWithZero.Action.Synonym Mathlib.Algebra.Order.GroupWithZero.Bounds Mathlib.Algebra.Order.GroupWithZero.Canonical Mathlib.Algebra.Order.GroupWithZero.Finset Mathlib.Algebra.Order.GroupWithZero.Lex Mathlib.Algebra.Order.GroupWithZero.Range Mathlib.Algebra.Order.GroupWithZero.Submonoid Mathlib.Algebra.Order.GroupWithZero.Synonym Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso Mathlib.Algebra.Order.GroupWithZero.WithZero Mathlib.Algebra.Order.Hom.MonoidWithZero Mathlib.Algebra.Order.Hom.Monoid Mathlib.Algebra.Order.Hom.Submonoid Mathlib.Algebra.Order.Hom.TypeTags Mathlib.Algebra.Order.Hom.Units Mathlib.Algebra.Order.Interval.Finset.Basic Mathlib.Algebra.Order.Interval.Finset.SuccPred Mathlib.Algebra.Order.Interval.Multiset Mathlib.Algebra.Order.Interval.Set.Monoid Mathlib.Algebra.Order.Interval.Set.SuccPred Mathlib.Algebra.Order.Monoid.Associated Mathlib.Algebra.Order.Monoid.Basic Mathlib.Algebra.Order.Monoid.Canonical.Basic Mathlib.Algebra.Order.Monoid.Canonical.Defs Mathlib.Algebra.Order.Monoid.Defs Mathlib.Algebra.Order.Monoid.Lex Mathlib.Algebra.Order.Monoid.NatCast Mathlib.Algebra.Order.Monoid.OrderDual Mathlib.Algebra.Order.Monoid.Prod Mathlib.Algebra.Order.Monoid.Submonoid Mathlib.Algebra.Order.Monoid.ToMulBot Mathlib.Algebra.Order.Monoid.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Basic Mathlib.Algebra.Order.Monoid.Unbundled.Defs Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE Mathlib.Algebra.Order.Monoid.Unbundled.MinMax Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual Mathlib.Algebra.Order.Monoid.Unbundled.Pow Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Units Mathlib.Algebra.Order.Monoid.Unbundled.WithTop Mathlib.Algebra.Order.Monoid.Units Mathlib.Algebra.Order.Monoid.WithTop Mathlib.Algebra.Order.PUnit Mathlib.Algebra.Order.Quantale Mathlib.Algebra.Order.Sub.Basic Mathlib.Algebra.Order.Sub.Defs Mathlib.Algebra.Order.Sub.Prod Mathlib.Algebra.Order.Sub.Unbundled.Basic Mathlib.Algebra.Order.Sub.WithTop Mathlib.Algebra.Order.SuccPred.PartialSups Mathlib.Algebra.Order.SuccPred.TypeTags Mathlib.Algebra.Order.SuccPred.WithBot Mathlib.Algebra.Order.SuccPred Mathlib.Algebra.Order.UpperLower Mathlib.Algebra.PEmptyInstances Mathlib.Algebra.Pointwise.Stabilizer Mathlib.Algebra.PresentedMonoid.Basic Mathlib.Algebra.Prime.Defs Mathlib.Algebra.Prime.Lemmas Mathlib.Algebra.Regular.Basic Mathlib.Algebra.Regular.Opposite Mathlib.Algebra.Regular.Pi Mathlib.Algebra.Regular.Pow Mathlib.Algebra.Regular.Prod Mathlib.Algebra.Regular.SMul Mathlib.Algebra.Regular.ULift Mathlib.Algebra.Ring.Action.Submonoid Mathlib.Combinatorics.Additive.Convolution Mathlib.Combinatorics.Additive.Dissociation Mathlib.Combinatorics.Additive.SubsetSum Mathlib.Combinatorics.Compactness Mathlib.Combinatorics.Digraph.Basic Mathlib.Combinatorics.Digraph.Orientation Mathlib.Combinatorics.Graph.Basic Mathlib.Combinatorics.Graph.Delete Mathlib.Combinatorics.Graph.Lattice Mathlib.Combinatorics.Graph.Maps Mathlib.Combinatorics.Graph.Subgraph Mathlib.Combinatorics.HalesJewett Mathlib.Combinatorics.Hall.Finite Mathlib.Combinatorics.Quiver.Path.Decomposition Mathlib.Combinatorics.Quiver.Path.Vertices Mathlib.Combinatorics.Quiver.Schreier Mathlib.Combinatorics.SetFamily.Compression.Down Mathlib.Combinatorics.SetFamily.Shatter Mathlib.Combinatorics.SimpleGraph.Basic Mathlib.Combinatorics.SimpleGraph.Cayley Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling Mathlib.Combinatorics.SimpleGraph.Dart Mathlib.Combinatorics.SimpleGraph.Finite Mathlib.Combinatorics.SimpleGraph.Maps Mathlib.Combinatorics.SimpleGraph.Walk.Basic Mathlib.Combinatorics.SimpleGraph.Walk.Chord Mathlib.Combinatorics.SimpleGraph.Walk.Operations Mathlib.Combinatorics.SimpleGraph.Walk.Traversal Mathlib.Combinatorics.SimpleGraph.Walk Mathlib.Combinatorics.Tiling.Tile Mathlib.Combinatorics.Young.SemistandardTableau Mathlib.Combinatorics.Young.YoungDiagram Mathlib.Computability.PostTuringMachine Mathlib.Computability.StateTransition Mathlib.Computability.Tape Mathlib.Computability.TuringMachine.PostTuringMachine Mathlib.Computability.TuringMachine.StackTuringMachine Mathlib.Computability.TuringMachine.Tape Mathlib.Computability.TuringMachine Mathlib.Control.Applicative Mathlib.Control.Bitraversable.Instances Mathlib.Control.Fix Mathlib.Control.LawfulFix Mathlib.Control.Monad.Cont Mathlib.Control.Monad.Writer Mathlib.Control.Random Mathlib.Control.Traversable.Equiv Mathlib.Control.Traversable.Instances Mathlib.Control.Traversable.Lemmas Mathlib.Control.ULiftable Mathlib.Data.Analysis.Filter Mathlib.Data.Analysis.Topology Mathlib.Data.DFinsupp.Defs Mathlib.Data.DFinsupp.Encodable Mathlib.Data.DFinsupp.Ext Mathlib.Data.DFinsupp.FiniteInfinite Mathlib.Data.DFinsupp.NeLocus Mathlib.Data.DFinsupp.Notation Mathlib.Data.DList.Instances Mathlib.Data.Fin.Tuple.BubbleSortInduction Mathlib.Data.Fin.Tuple.Finset Mathlib.Data.Fin.Tuple.Sort Mathlib.Data.FinEnum.Option Mathlib.Data.FinEnum Mathlib.Data.Finite.Prod Mathlib.Data.Finite.Sigma Mathlib.Data.Finite.Sum Mathlib.Data.Finite.Vector Mathlib.Data.Finmap Mathlib.Data.Finset.CastCard Mathlib.Data.Finset.DenselyOrdered Mathlib.Data.Finset.Functor Mathlib.Data.Finset.Lattice.Fold Mathlib.Data.Finset.Lattice.Pi Mathlib.Data.Finset.Lattice.Prod Mathlib.Data.Finset.Lattice.Union Mathlib.Data.Finset.Max Mathlib.Data.Finset.MulAntidiagonal Mathlib.Data.Finset.NAry Mathlib.Data.Finset.NatAntidiagonal Mathlib.Data.Finset.NoncommProd Mathlib.Data.Finset.Option Mathlib.Data.Finset.PImage Mathlib.Data.Finset.Pairwise Mathlib.Data.Finset.PiInduction Mathlib.Data.Finset.Pi Mathlib.Data.Finset.Powerset Mathlib.Data.Finset.Preimage Mathlib.Data.Finset.Prod Mathlib.Data.Finset.SMulAntidiagonal Mathlib.Data.Finset.Sigma Mathlib.Data.Finset.Slice Mathlib.Data.Finset.Sort Mathlib.Data.Finset.Sum Mathlib.Data.Finset.Sups Mathlib.Data.Finset.Sym Mathlib.Data.Finset.Union Mathlib.Data.Finset.Update Mathlib.Data.Finsupp.BigOperators Mathlib.Data.Finsupp.Ext Mathlib.Data.Finsupp.Fin Mathlib.Data.Finsupp.Fintype Mathlib.Data.Finsupp.Indicator Mathlib.Data.Finsupp.NeLocus Mathlib.Data.Finsupp.Notation Mathlib.Data.Finsupp.PWO Mathlib.Data.Finsupp.SMulWithZero Mathlib.Data.Finsupp.Single Mathlib.Data.Fintype.BigOperators Mathlib.Data.Fintype.CardEmbedding Mathlib.Data.Fintype.Fin Mathlib.Data.Fintype.Lattice Mathlib.Data.Fintype.List Mathlib.Data.Fintype.Option Mathlib.Data.Fintype.Order Mathlib.Data.Fintype.Parity Mathlib.Data.Fintype.Perm Mathlib.Data.Fintype.Pi Mathlib.Data.Fintype.Pigeonhole Mathlib.Data.Fintype.Powerset Mathlib.Data.Fintype.Prod Mathlib.Data.Fintype.Quotient Mathlib.Data.Fintype.Sigma Mathlib.Data.Fintype.Sort Mathlib.Data.Fintype.Sum Mathlib.Data.Fintype.Vector Mathlib.Data.Fintype.WithTopBot Mathlib.Data.FunLike.Fintype Mathlib.Data.Int.Cast.Basic Mathlib.Data.Int.Cast.Defs Mathlib.Data.Int.Cast.Prod Mathlib.Data.Int.GCD Mathlib.Data.Int.Range Mathlib.Data.List.Cycle Mathlib.Data.List.Iterate Mathlib.Data.List.PeriodicityLemma Mathlib.Data.List.Pi Mathlib.Data.List.Prime Mathlib.Data.List.SplitLengths Mathlib.Data.List.Sym Mathlib.Data.List.ToFinsupp Mathlib.Data.Matrix.DMatrix Mathlib.Data.Multiset.Antidiagonal Mathlib.Data.Multiset.Bind Mathlib.Data.Multiset.DershowitzManna Mathlib.Data.Multiset.Fintype Mathlib.Data.Multiset.Functor Mathlib.Data.Multiset.OrderedMonoid Mathlib.Data.Multiset.Pi Mathlib.Data.Multiset.Powerset Mathlib.Data.Multiset.Sections Mathlib.Data.Multiset.Sum Mathlib.Data.Multiset.Sym Mathlib.Data.Nat.Cast.Defs Mathlib.Data.Nat.Cast.NeZero Mathlib.Data.Nat.Cast.Prod Mathlib.Data.Nat.Cast.Synonym Mathlib.Data.Nat.Count Mathlib.Data.Nat.GCD.Basic Mathlib.Data.Nat.GCD.BigOperators Mathlib.Data.Nat.GCD.Prime Mathlib.Data.Nat.Lattice Mathlib.Data.Nat.PSub Mathlib.Data.Nat.Prime.Defs Mathlib.Data.Nat.Prime.Infinite Mathlib.Data.Nat.Upto Mathlib.Data.Num.Bitwise Mathlib.Data.Ordmap.Ordnode Mathlib.Data.PFunctor.Multivariate.Basic Mathlib.Data.PFunctor.Multivariate.M Mathlib.Data.PFunctor.Multivariate.W Mathlib.Data.PFunctor.Univariate.Basic Mathlib.Data.PFunctor.Univariate.M Mathlib.Data.PNat.Interval Mathlib.Data.Pi.Interval Mathlib.Data.QPF.Multivariate.Basic Mathlib.Data.QPF.Multivariate.Constructions.Cofix Mathlib.Data.QPF.Multivariate.Constructions.Comp Mathlib.Data.QPF.Multivariate.Constructions.Const Mathlib.Data.QPF.Multivariate.Constructions.Fix Mathlib.Data.QPF.Multivariate.Constructions.Prj Mathlib.Data.QPF.Multivariate.Constructions.Quot Mathlib.Data.QPF.Multivariate.Constructions.Sigma Mathlib.Data.QPF.Univariate.Basic Mathlib.Data.Rat.Defs Mathlib.Data.Set.Accumulate Mathlib.Data.Set.Dissipate Mathlib.Data.Set.Enumerate Mathlib.Data.Set.Finite.Lattice Mathlib.Data.Set.Finite.Lemmas Mathlib.Data.Set.Finite.List Mathlib.Data.Set.Finite.Monad Mathlib.Data.Set.Finite.Powerset Mathlib.Data.Set.FiniteExhaustion Mathlib.Data.Set.MemPartition Mathlib.Data.Set.MulAntidiagonal Mathlib.Data.Set.Pointwise.Support Mathlib.Data.Set.SMulAntidiagonal Mathlib.Data.Set.Sups Mathlib.Data.SetLike.Fintype Mathlib.Data.Setoid.Partition Mathlib.Data.Sigma.Interval Mathlib.Data.String.Basic Mathlib.Data.Sum.Interval Mathlib.Data.Sym.Basic Mathlib.Data.Sym.Card Mathlib.Data.Sym.Sym2.Finsupp Mathlib.Data.Sym.Sym2.Order Mathlib.Data.Sym.Sym2 Mathlib.Data.Tree.Traversable Mathlib.Data.Vector.Basic Mathlib.Data.Vector.MapLemmas Mathlib.Data.Vector.Mem Mathlib.Data.Vector.Snoc Mathlib.Data.Vector.Zip Mathlib.Data.W.Basic Mathlib.Data.W.Constructions Mathlib.Dynamics.BirkhoffSum.Basic Mathlib.Dynamics.FixedPoints.Basic Mathlib.Dynamics.FixedPoints.Prufer Mathlib.Dynamics.PeriodicPts.Defs Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage Mathlib.Geometry.Group.Growth.QuotientInter Mathlib.GroupTheory.Abelianization.Defs Mathlib.GroupTheory.Commutator.Basic Mathlib.GroupTheory.Congruence.Basic Mathlib.GroupTheory.Congruence.BigOperators Mathlib.GroupTheory.Congruence.Defs Mathlib.GroupTheory.Congruence.Hom Mathlib.GroupTheory.Congruence.Opposite Mathlib.GroupTheory.Coprod.Basic Mathlib.GroupTheory.Coset.Basic Mathlib.GroupTheory.Coset.Defs Mathlib.GroupTheory.DedekindFinite Mathlib.GroupTheory.DoubleCoset Mathlib.GroupTheory.EckmannHilton Mathlib.GroupTheory.FinitelyPresentedGroup Mathlib.GroupTheory.Finiteness Mathlib.GroupTheory.FreeGroup.Basic Mathlib.GroupTheory.FreeGroup.IsFreeGroup Mathlib.GroupTheory.FreeGroup.Orbit Mathlib.GroupTheory.FreeGroup.Reduce Mathlib.GroupTheory.Goursat Mathlib.GroupTheory.GroupAction.ConjAct Mathlib.GroupTheory.GroupAction.Defs Mathlib.GroupTheory.GroupAction.Embedding Mathlib.GroupTheory.GroupAction.IterateAct Mathlib.GroupTheory.GroupAction.Support Mathlib.GroupTheory.IsSubnormal Mathlib.GroupTheory.MonoidLocalization.Away Mathlib.GroupTheory.MonoidLocalization.Basic Mathlib.GroupTheory.MonoidLocalization.DivPairs Mathlib.GroupTheory.MonoidLocalization.Finite Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup Mathlib.GroupTheory.MonoidLocalization.Lemmas Mathlib.GroupTheory.MonoidLocalization.Maps Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero Mathlib.GroupTheory.MonoidLocalization.Order Mathlib.GroupTheory.NoncommCoprod Mathlib.GroupTheory.OreLocalization.Basic Mathlib.GroupTheory.OreLocalization.OreSet Mathlib.GroupTheory.Perm.Basic Mathlib.GroupTheory.Perm.List Mathlib.GroupTheory.Perm.Support Mathlib.GroupTheory.Perm.ViaEmbedding Mathlib.GroupTheory.PresentedGroup Mathlib.GroupTheory.QuotientGroup.Defs Mathlib.GroupTheory.QuotientGroup.ModEq Mathlib.GroupTheory.Subgroup.Center Mathlib.GroupTheory.Subgroup.Centralizer Mathlib.GroupTheory.Subgroup.Saturated Mathlib.GroupTheory.Subgroup.Simple Mathlib.GroupTheory.Submonoid.Center Mathlib.GroupTheory.Submonoid.Centralizer Mathlib.GroupTheory.Submonoid.Inverses Mathlib.GroupTheory.Subsemigroup.Center Mathlib.GroupTheory.Subsemigroup.Centralizer Mathlib.LinearAlgebra.AffineSpace.Defs Mathlib.Logic.Encodable.Pi Mathlib.Logic.Equiv.Fin.Rotate Mathlib.Logic.Equiv.Finset Mathlib.Logic.Small.List Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable Mathlib.MeasureTheory.PiSystem Mathlib.MeasureTheory.SetAlgebra Mathlib.MeasureTheory.SetSemiring Mathlib.NumberTheory.Harmonic.Defs Mathlib.Order.Atoms.Finite Mathlib.Order.Birkhoff Mathlib.Order.BooleanGenerators Mathlib.Order.BooleanSubalgebra Mathlib.Order.BourbakiWitt Mathlib.Order.CompactlyGenerated.Basic Mathlib.Order.CompactlyGenerated.Intervals Mathlib.Order.CompleteLattice.Finset Mathlib.Order.CompleteLattice.Group Mathlib.Order.CompleteLattice.SetLike Mathlib.Order.CompletePartialOrder Mathlib.Order.CompleteSublattice Mathlib.Order.ConditionallyCompleteLattice.Finset Mathlib.Order.ConditionallyCompleteLattice.Group Mathlib.Order.CountableDenseLinearOrder Mathlib.Order.Disjointed Mathlib.Order.Filter.AtTopBot.Basic Mathlib.Order.Filter.AtTopBot.BigOperators Mathlib.Order.Filter.AtTopBot.CompleteLattice Mathlib.Order.Filter.AtTopBot.CountablyGenerated Mathlib.Order.Filter.AtTopBot.Defs Mathlib.Order.Filter.AtTopBot.Disjoint Mathlib.Order.Filter.AtTopBot.Finite Mathlib.Order.Filter.AtTopBot.Finset Mathlib.Order.Filter.AtTopBot.Group Mathlib.Order.Filter.AtTopBot.Map Mathlib.Order.Filter.AtTopBot.Monoid Mathlib.Order.Filter.AtTopBot.Prod Mathlib.Order.Filter.AtTopBot.Tendsto Mathlib.Order.Filter.Bases.Basic Mathlib.Order.Filter.Bases.Finite Mathlib.Order.Filter.Basic Mathlib.Order.Filter.Cofinite Mathlib.Order.Filter.CountableInter Mathlib.Order.Filter.CountableSeparatingOn Mathlib.Order.Filter.CountablyGenerated Mathlib.Order.Filter.Curry Mathlib.Order.Filter.EventuallyConst Mathlib.Order.Filter.Extr Mathlib.Order.Filter.Finite Mathlib.Order.Filter.IndicatorFunction Mathlib.Order.Filter.Interval Mathlib.Order.Filter.IsBounded Mathlib.Order.Filter.Ker Mathlib.Order.Filter.Lift Mathlib.Order.Filter.ListTraverse Mathlib.Order.Filter.Map Mathlib.Order.Filter.NAry Mathlib.Order.Filter.Partial Mathlib.Order.Filter.Pi Mathlib.Order.Filter.Prod Mathlib.Order.Filter.SmallSets Mathlib.Order.Filter.Subsingleton Mathlib.Order.Filter.Tendsto Mathlib.Order.Filter.Ultrafilter.Basic Mathlib.Order.Filter.Ultrafilter.Defs Mathlib.Order.FixedPoints Mathlib.Order.GameAdd Mathlib.Order.Ideal Mathlib.Order.Interval.Finset.Basic Mathlib.Order.Interval.Finset.Defs Mathlib.Order.Interval.Finset.DenselyOrdered Mathlib.Order.Interval.Finset.Fin Mathlib.Order.Interval.Finset.Gaps Mathlib.Order.Interval.Finset.Nat Mathlib.Order.Interval.Finset.SuccPred Mathlib.Order.Interval.Multiset Mathlib.Order.Irreducible Mathlib.Order.JordanHolder Mathlib.Order.LiminfLimsup Mathlib.Order.Monotone.Odd Mathlib.Order.Northcott Mathlib.Order.OmegaCompletePartialOrder Mathlib.Order.OrderIsoNat Mathlib.Order.PFilter Mathlib.Order.PartialSups Mathlib.Order.Partition.Basic Mathlib.Order.Partition.Finpartition Mathlib.Order.PrimeIdeal Mathlib.Order.PrimeSeparator Mathlib.Order.RelSeries Mathlib.Order.Restriction Mathlib.Order.SaddlePoint Mathlib.Order.SemiconjSup Mathlib.Order.Sublattice Mathlib.Order.Sublocale Mathlib.Order.SuccPred.LinearLocallyFinite Mathlib.Order.SupClosed Mathlib.Order.SupIndep Mathlib.Order.TeichmullerTukey Mathlib.Order.UpperLower.LocallyFinite Mathlib.Order.WellFoundedSet Mathlib.Order.WellQuasiOrder Mathlib.RingTheory.HahnSeries.Basic Mathlib.RingTheory.OreLocalization.Basic Mathlib.RingTheory.OreLocalization.NonZeroDivisors Mathlib.RingTheory.UniqueFactorizationDomain.Defs Mathlib.SetTheory.Cardinal.SchroederBernstein Mathlib.SetTheory.Descriptive.Tree Mathlib.Tactic.DeriveTraversable Mathlib.Tactic.FieldSimp.Lemmas Mathlib.Tactic.MoveAdd Mathlib.Tactic.Peel Mathlib.Tactic.Sat.FromLRAT Mathlib.Tactic.Zify Mathlib.Testing.Plausible.Functions Mathlib.Topology.AlexandrovDiscrete Mathlib.Topology.Algebra.ContinuousMonoidHom Mathlib.Topology.Algebra.Group.Defs Mathlib.Topology.Algebra.Indicator Mathlib.Topology.Algebra.InfiniteSum.SummationFilter Mathlib.Topology.Algebra.Monoid.Defs Mathlib.Topology.Baire.Lemmas Mathlib.Topology.Bases Mathlib.Topology.Bornology.Basic Mathlib.Topology.Bornology.Constructions Mathlib.Topology.Bornology.Hom Mathlib.Topology.Clopen Mathlib.Topology.Closure Mathlib.Topology.ClusterPt Mathlib.Topology.Coherent Mathlib.Topology.Compactness.Bases Mathlib.Topology.Compactness.Compact Mathlib.Topology.Compactness.CompactlyCoherentSpace Mathlib.Topology.Compactness.Lindelof Mathlib.Topology.Compactness.LocallyCompact Mathlib.Topology.Compactness.LocallyFinite Mathlib.Topology.Compactness.NhdsKer Mathlib.Topology.Compactness.SigmaCompact Mathlib.Topology.Constructions.SumProd Mathlib.Topology.Constructions Mathlib.Topology.ContinuousOn Mathlib.Topology.Continuous Mathlib.Topology.Defs.Sequences Mathlib.Topology.Defs.Ultrafilter Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle Mathlib.Topology.GDelta.Basic Mathlib.Topology.Hom.ContinuousEvalConst Mathlib.Topology.Hom.ContinuousEval Mathlib.Topology.Homeomorph.Defs Mathlib.Topology.Homeomorph.TransferInstance Mathlib.Topology.Inseparable Mathlib.Topology.Instances.Shrink Mathlib.Topology.List Mathlib.Topology.LocallyClosed Mathlib.Topology.LocallyFinite Mathlib.Topology.Maps.Basic Mathlib.Topology.Maps.OpenQuotient Mathlib.Topology.MetricSpace.BundledFun Mathlib.Topology.Neighborhoods Mathlib.Topology.NhdsKer Mathlib.Topology.NhdsSet Mathlib.Topology.NhdsWithin Mathlib.Topology.OpenPartialHomeomorph.Defs Mathlib.Topology.Order.Bornology Mathlib.Topology.Order.Hom.Basic Mathlib.Topology.Order.Hom.Esakia Mathlib.Topology.Order.LeftRight Mathlib.Topology.Order.LocalExtr Mathlib.Topology.Order Mathlib.Topology.Partial Mathlib.Topology.Piecewise Mathlib.Topology.PreorderRestrict Mathlib.Topology.Semicontinuity.Defs Mathlib.Topology.Separation.SeparatedNhds Mathlib.Topology.Ultrafilter Mathlib.Topology.UniformSpace.Basic Mathlib.Topology.UniformSpace.Compact Mathlib.Topology.UniformSpace.Defs Mathlib.Topology.UniformSpace.DiscreteUniformity Mathlib.Topology.UniformSpace.OfFun Mathlib.Topology.UniformSpace.Ultra.Basic	1
Mathlib.Tactic.CrossRefAttribute (new file)	54

---

Declarations diff

+ Lean.Environment.getCrossRefDeclNames
+ Lean.Environment.getSortedCrossRefs
+ Lean.TSyntax.getWikidataId
+ addCrossRefDoc
+ databaseName
+ traceCrossRefs
+ wikidataIdAntiquot.parenthesizer
+ wikidataIdFn
+ wikidataIdKind
+ wikidataIdNoAntiquot
+ wikidataIdNoAntiquot.formatter
+ wikidataIdParser
- Lean.Environment.getSortedStackProjectDeclNames
- Lean.Environment.getSortedStackProjectTags
- traceStacksTags

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

---

note: file Mathlib/Tactic/StacksAttribute.lean was removed.
Please create a follow-up pull request adding a module deprecation. Thanks!

note: file MathlibTest/StacksAttribute.lean` was renamed to `MathlibTest/CrossRefAttribute.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

[grunweg]

Cross-referencing #38070 for the record

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - chore(Tactic): move StacksAttribute to CrossRefAttribute #39257
  By Dependent Issues (🤖). Happy coding!