diff --git a/Mathlib/Algebra/LinearRecurrence.lean b/Mathlib/Algebra/LinearRecurrence.lean
index 6634b8b7951ff4..cbbc654009610a 100644
--- a/Mathlib/Algebra/LinearRecurrence.lean
+++ b/Mathlib/Algebra/LinearRecurrence.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Polynomial.Degree.Operations
 public import Mathlib.Algebra.Polynomial.Eval.Defs
 public import Mathlib.LinearAlgebra.Dimension.Constructions
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Linear recurrence
@@ -48,6 +49,7 @@ open Polynomial
 
 /-- A "linear recurrence relation" over a commutative semiring is given by its
   order `n` and `n` coefficients. -/
+@[wikidata Q364089]
 structure LinearRecurrence (R : Type*) [CommSemiring R] where
   /-- Order of the linear recurrence -/
   order : ℕ
diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
index 9836ea7f5a2ede..f915ca4763ad8d 100644
--- a/Mathlib/Analysis/InnerProductSpace/PiL2.lean
+++ b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
@@ -10,6 +10,7 @@ public import Mathlib.Analysis.Normed.Lp.PiLp
 public import Mathlib.Analysis.Normed.Lp.Matrix
 public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
 public import Mathlib.LinearAlgebra.UnitaryGroup
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Util.Superscript
 
 /-!
@@ -108,6 +109,7 @@ space use `EuclideanSpace 𝕜 (Fin n)`.
 
 For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
 analogous to `![x, y, ...]` notation. -/
+@[wikidata Q17295]
 abbrev EuclideanSpace (𝕜 : Type*) (n : Type*) : Type _ :=
   PiLp 2 fun _ : n => 𝕜
 
diff --git a/Mathlib/LinearAlgebra/Basis/Defs.lean b/Mathlib/LinearAlgebra/Basis/Defs.lean
index c66920d1a2c6eb..c4ff6d939ed635 100644
--- a/Mathlib/LinearAlgebra/Basis/Defs.lean
+++ b/Mathlib/LinearAlgebra/Basis/Defs.lean
@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Alexander Bentkamp
 module
 
 public import Mathlib.LinearAlgebra.Finsupp.LinearCombination
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Bases
@@ -85,6 +86,7 @@ To turn a linear independent family of vectors spanning `M` into a basis, use `B
 They are internally represented as linear equivs `M ≃ₗ[R] (ι →₀ R)`,
 available as `Basis.repr`.
 -/
+@[wikidata Q189569]
 structure Basis where
   /-- `Basis.ofRepr` constructs a basis given an assignment of coordinates to each vector. -/
   ofRepr ::
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
index d6eb7a6bedd007..33ca6fe5da724c 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
@@ -9,6 +9,7 @@ public import Mathlib.RingTheory.Congruence.Hom
 public import Mathlib.LinearAlgebra.TensorAlgebra.Basic
 public import Mathlib.LinearAlgebra.QuadraticForm.Isometry
 public import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Clifford Algebras
@@ -69,6 +70,7 @@ end CliffordAlgebra
 
 /-- The Clifford algebra of an `R`-module `M` equipped with a `QuadraticForm` `Q`.
 -/
+@[wikidata Q674689]
 def CliffordAlgebra := CliffordAlgebra.ringCon Q |>.Quotient
 deriving Inhabited, Ring, Algebra R
 
diff --git a/Mathlib/LinearAlgebra/Dual/Defs.lean b/Mathlib/LinearAlgebra/Dual/Defs.lean
index 62a06d2c073886..0323991b305053 100644
--- a/Mathlib/LinearAlgebra/Dual/Defs.lean
+++ b/Mathlib/LinearAlgebra/Dual/Defs.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.LinearAlgebra.BilinearMap
 public import Mathlib.LinearAlgebra.Span.Defs
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Dual vector spaces
@@ -57,6 +58,7 @@ variable (R A M : Type*)
 variable [CommSemiring R] [AddCommMonoid M] [Module R M]
 
 /-- The left dual space of an R-module M is the R-module of linear maps `M → R`. -/
+@[wikidata Q752487]
 abbrev Dual (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M] :=
   M →ₗ[R] R
 
diff --git a/Mathlib/LinearAlgebra/RootSystem/Defs.lean b/Mathlib/LinearAlgebra/RootSystem/Defs.lean
index 1b5b341eac3111..3dd44ce2f78b71 100644
--- a/Mathlib/LinearAlgebra/RootSystem/Defs.lean
+++ b/Mathlib/LinearAlgebra/RootSystem/Defs.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.LinearAlgebra.PerfectPairing.Basic
 public import Mathlib.LinearAlgebra.Reflection
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Root data and root systems
@@ -113,6 +114,7 @@ variable {ι R M N}
 variable (P : RootPairing ι R M N) (i j : ι)
 
 /-- A root system is a root pairing for which the roots and coroots span their ambient modules. -/
+@[wikidata Q534131]
 class IsRootSystem : Prop where
   span_root_eq_top : span R (range P.root) = ⊤
   span_coroot_eq_top : span R (range P.coroot) = ⊤
diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
index fda5b38bd6fb45..6cfccad643f8bb 100644
--- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
+++ b/Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
@@ -6,6 +6,7 @@ Authors: Rémy Degenne
 module
 
 public import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
+public import Mathlib.Tactic.CrossRefAttribute
 
 import Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum
 
@@ -97,6 +98,7 @@ It is defined as 0 if any one of the following conditions is true:
 - `m` is not a sub-σ-algebra of `m₀`,
 - `μ` is not σ-finite with respect to `m`,
 - `f` is not integrable. -/
+@[wikidata Q772232]
 noncomputable irreducible_def condExp (μ : Measure[m₀] α) (f : α → E) : α → E :=
   if hm : m ≤ m₀ then
     if h : SigmaFinite (μ.trim hm) ∧ Integrable f μ then
diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean
index 7e7ca233026342..358f01e9d06fb1 100644
--- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean
+++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.MeasureTheory.Function.JacobianOneDim
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Integration by parts and by substitution
@@ -526,6 +527,7 @@ theorem integral_comp_mul_deriv' {f f' g : ℝ → ℝ} (h : ∀ x ∈ uIcc a b,
 and `g` is continuous, then we can substitute `u = f x` to get
 `∫ x in a..b, (g ∘ f) x * f' x = ∫ u in f a..f b, g u`.
 -/
+@[wikidata Q1071270]
 theorem integral_comp_mul_deriv {f f' g : ℝ → ℝ} (h : ∀ x ∈ uIcc a b, HasDerivAt f (f' x) x)
     (h' : ContinuousOn f' (uIcc a b)) (hg : Continuous g) :
     (∫ x in a..b, (g ∘ f) x * f' x) = ∫ x in f a..f b, g x :=
diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean
index 243d55e8c4436f..0fe73938b60340 100644
--- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean
+++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean
@@ -6,6 +6,7 @@ Authors: P. Michael Kielstra
 module
 
 public import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Tactic.Field
 
 /-!
@@ -29,6 +30,7 @@ open MeasureTheory intervalIntegral Interval Finset HasDerivWithinAt Set
 /-- Integration of `f` from `a` to `b` using the trapezoidal rule with `N+1` total evaluations of
 `f`.  (Note the off-by-one problem here: `N` counts the number of trapezoids, not the number of
 evaluations.) -/
+@[wikidata Q833293]
 noncomputable def trapezoidal_integral (f : ℝ → ℝ) (N : ℕ) (a b : ℝ) : ℝ :=
   ((b - a) / N) * ((f a + f b) / 2 + ∑ k ∈ range (N - 1), f (a + (k + 1) * (b - a) / N))
 
diff --git a/Mathlib/NumberTheory/LSeries/RiemannZeta.lean b/Mathlib/NumberTheory/LSeries/RiemannZeta.lean
index fdff2c94adcfd8..3c92195fce20df 100644
--- a/Mathlib/NumberTheory/LSeries/RiemannZeta.lean
+++ b/Mathlib/NumberTheory/LSeries/RiemannZeta.lean
@@ -117,6 +117,7 @@ lemma completedRiemannZeta_residue_one :
 -/
 
 /-- The Riemann zeta function `ζ(s)`. -/
+@[wikidata Q187235]
 def riemannZeta := hurwitzZetaEven 0
 
 lemma HurwitzZeta.hurwitzZetaEven_zero : hurwitzZetaEven 0 = riemannZeta := rfl
diff --git a/Mathlib/Order/Filter/Extr.lean b/Mathlib/Order/Filter/Extr.lean
index 0c646f48feabca..f8337827d8f967 100644
--- a/Mathlib/Order/Filter/Extr.lean
+++ b/Mathlib/Order/Filter/Extr.lean
@@ -9,6 +9,7 @@ public import Mathlib.Order.Filter.Tendsto
 public import Mathlib.Order.ConditionallyCompleteLattice.Indexed
 public import Mathlib.Algebra.Order.Group.Defs
 public import Mathlib.Data.Finset.Lattice.Fold
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 # Minimum and maximum w.r.t. a filter and on a set
@@ -114,6 +115,7 @@ def IsMaxOn :=
   IsMaxFilter f (𝓟 s) a
 
 /-- `IsExtrOn f s a` means `IsMinOn f s a` or `IsMaxOn f s a` -/
+@[wikidata Q845060]
 def IsExtrOn : Prop :=
   IsExtrFilter f (𝓟 s) a
 
diff --git a/Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean b/Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean
index 5841aa7aa67bef..dd141c6c82a710 100644
--- a/Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean
+++ b/Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.RingTheory.Ideal.Quotient.Basic
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
+public import Mathlib.Tactic.CrossRefAttribute
 
 /-!
 
@@ -25,6 +26,7 @@ namespace IsLocalRing
 variable (R : Type*) [CommRing R] [IsLocalRing R]
 
 /-- The residue field of a local ring is the quotient of the ring by its maximal ideal. -/
+@[wikidata Q7315530]
 def ResidueField :=
   R ⧸ maximalIdeal R
 deriving CommRing, Inhabited
diff --git a/Mathlib/Topology/Algebra/Module/LocallyConvex.lean b/Mathlib/Topology/Algebra/Module/LocallyConvex.lean
index c252b2838872f4..c73f0cfd0adb75 100644
--- a/Mathlib/Topology/Algebra/Module/LocallyConvex.lean
+++ b/Mathlib/Topology/Algebra/Module/LocallyConvex.lean
@@ -6,6 +6,7 @@ Authors: Anatole Dedecker
 module
 
 public import Mathlib.Analysis.Convex.Topology
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Topology.Connected.LocallyPathConnected
 public import Mathlib.Analysis.Convex.PathConnected
 
@@ -46,6 +47,7 @@ section Semimodule
 
 /-- A `LocallyConvexSpace` is a topological semimodule over an ordered semiring in which convex
 neighborhoods of a point form a neighborhood basis at that point. -/
+@[wikidata Q1572357]
 class LocallyConvexSpace (𝕜 E : Type*) [Semiring 𝕜] [PartialOrder 𝕜]
     [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : Prop where
   convex_basis : ∀ x : E, (𝓝 x).HasBasis (fun s : Set E => s ∈ 𝓝 x ∧ Convex 𝕜 s) id
diff --git a/Mathlib/Topology/UniformSpace/Cauchy.lean b/Mathlib/Topology/UniformSpace/Cauchy.lean
index 343f98439c2ac3..74fd21c99e4b5b 100644
--- a/Mathlib/Topology/UniformSpace/Cauchy.lean
+++ b/Mathlib/Topology/UniformSpace/Cauchy.lean
@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 -/
 module
 
+public import Mathlib.Tactic.CrossRefAttribute
 public import Mathlib.Topology.Algebra.Constructions
 public import Mathlib.Topology.Bases
 public import Mathlib.Algebra.Order.Group.Nat
@@ -365,6 +366,7 @@ theorem isComplete_iUnion_separated {ι : Sort*} {s : ι → Set α} (hs : ∀ i
 
 /-- A complete space is defined here using uniformities. A uniform space
   is complete if every Cauchy filter converges. -/
+@[wikidata Q848569]
 class CompleteSpace (α : Type u) [UniformSpace α] : Prop where
   /-- In a complete uniform space, every Cauchy filter converges. -/
   complete : ∀ {f : Filter α}, Cauchy f → ∃ x, f ≤ 𝓝 x