chore: remove Mathlib namespace from library note links

data/documentation.yaml

@@ -479,47 +479,47 @@ documentation:
     tags:
       - elementary
   - title: "library note [the algebraic hierarchy]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«the algebraic hierarchy»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«the algebraic hierarchy»#doc"
     description: "Explains the structure of the algebraic hierarchy and how to add new elements to it."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - classes
   - title: "library note [reducible non-instances]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«reducible non-instances»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«reducible non-instances»#doc"
     description: "Definitions that cannot be instances should be made reducible."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - classes
   - title: "library note [implicit instance arguments]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«implicit instance arguments»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«implicit instance arguments»#doc"
     description: "Some places prefer implicit `{}` brackets for typeclass arguments instead of typical instance `[]` brackets."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - classes
   - title: "library note [lower instance priority]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«lower instance priority»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«lower instance priority»#doc"
     description: "When creating an instance that always applies, give it a lower priority."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - classes
   - title: "library note [instance argument order]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«instance argument order»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«instance argument order»#doc"
     description: "A trick to speed up typeclass instance synthesis by putting more specific goals first."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - classes
   - title: "library note [SetLike Aesop ruleset]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«SetLike Aesop ruleset»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«SetLike Aesop ruleset»#doc"
     description: "How to add rules about `SetLike` membership to Aesop."
     authors: the Mathlib community
     accessed_at: 2025-10-02
@@ -528,23 +528,23 @@ documentation:
       - elementary
       - tactics
   - title: "library note [no_index around OfNat.ofNat]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«no_index around OfNat.ofNat»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«no_index around OfNat.ofNat»#doc"
     authors: the Mathlib community
     description: "Write `ofNat(n)` in lemmas instead of `OfNat.ofNat n`."
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - elementary
   - title: "library note [coercion into rings]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«coercion into rings»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«coercion into rings»#doc"
     description: "How to set up coercions from a concrete structure like `ℕ` to an arbitrary ring `R`."
     authors: the Mathlib community
     accessed_at: 2025-10-06
     category: explanation
     tags:
       - ring theory
   - title: "library note [RCLike instance]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«RCLike instance»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«RCLike instance»#doc"
     description: "An instance creating a goal `[RCLike ?m]` is okay since there are only two choices, `ℝ` or `ℂ`."
     authors: the Mathlib community
     accessed_at: 2025-10-02
@@ -553,111 +553,111 @@ documentation:
       - analysis
       - classes
   - title: "library note [fact non-instances]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«fact non-instances»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«fact non-instances»#doc"
     description: "We do not declare any global instances of the `Fact` typeclass."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - classes
   - title: "library note [decidable namespace]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«decidable namespace»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«decidable namespace»#doc"
     description: "The `Decidable` namespace contains theorems that avoid the use of the Law of Excluded Middle by using `Decidable` instances instead."
     authors: the Mathlib community
     accessed_at: 2025-10-06
     category: explanation
     tags:
       - declarations
   - title: "library note [decidable arguments]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«decidable arguments»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«decidable arguments»#doc"
     description: "If a `Decidable` hypothesis is not needed for the type signature of a theorem or lemma, use `classical` instead."
     authors: the Mathlib community
     accessed_at: 2025-10-06
     category: explanation
     tags:
       - declarations
   - title: "library note [slow-failing instance priority]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«slow-failing instance priority»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«slow-failing instance priority»#doc"
     description: "Instances that would be slow to fail to apply should have a lower priority."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - classes
   - title: "library note [foundational algebra order theory]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«foundational algebra order theory»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«foundational algebra order theory»#doc"
     description: "Batteries sets up the algebraic and order theoretic properties of `Nat` and `Int`; Mathlib replaces this with a typeclass-based system."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - elementary
   - title: "library note [continuity lemma statement]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«continuity lemma statement»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«continuity lemma statement»#doc"
     description: "How to write more useful continuity lemmas."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - topology
   - title: "library note [comp_of_eq lemmas]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«comp_of_eq lemmas»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«comp_of_eq lemmas»#doc"
     description: "How to avoid elaboration problems when writing the continuity of a composition."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - topology
   - title: "library note [IMO geometry formalization conventions]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«IMO geometry formalization conventions»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«IMO geometry formalization conventions»#doc"
     description: "Conventions for formalizing geometry problems from the IMO as part of Mathlib's Archive."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - euclidean geometry
   - title: "library note [change elaboration strategy with `by apply`]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«change elaboration strategy with `by apply`»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«change elaboration strategy with `by apply`»#doc"
     description: "A trick to elaborate a term and its type in a different order."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - tactics
   - title: "library note [pointwise nat action]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«pointwise nat action»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«pointwise nat action»#doc"
     description: "The action of natural numbers or integers on sets takes precedence over pointwise actions."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - elementary
   - title: "library note [Design choices about smooth algebraic structures]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«Design choices about smooth algebraic structures»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«Design choices about smooth algebraic structures»#doc"
     description: "Mathlib's design choices about smooth algebraic structures"
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - differential geometry
   - title: "library note [Manifold type tags]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«Manifold type tags»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«Manifold type tags»#doc"
     description: "Explains why `ModelProd` and `ModelPi` exist."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - differential geometry
   - title: "library note [non-Archimedean non-instances]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«non-Archimedean non-instances»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«non-Archimedean non-instances»#doc"
     description: "Why non-Archimedean subgroup basis lemmas cannot be instances."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - topology
   - title: "library note [range copy pattern]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«range copy pattern»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«range copy pattern»#doc"
     description: "The image of a morphism `f` is defined using `Set.range` if possible, not `map ⊤ f`."
     authors: the Mathlib community
     accessed_at: 2025-10-02
@@ -667,55 +667,55 @@ documentation:
       - linear algebra
       - ring theory
   - title: "library note [continuous functional calculus]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«continuous functional calculus»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«continuous functional calculus»#doc"
     description: "Design overview of the ontinuous functional calculus in Mathlib."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - analysis
   - title: "library note [specialised high priority simp lemma]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«specialised high priority simp lemma»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«specialised high priority simp lemma»#doc"
     description: "When not to un-`@[simp]` a lemma in favour of a more powerful version."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - tactics
   - title: "library note [out-param inheritance]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«out-param inheritance»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«out-param inheritance»#doc"
     description: "Limitations on the interaction of typeclass inheritance and `outParam`s."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - classes
   - title: "library note [lower cancel priority]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«lower cancel priority»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«lower cancel priority»#doc"
     description: "Inheritance from cancellative algebraic structures gets a lower priority."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - classes
   - title: "library note [forgetful inheritance]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«forgetful inheritance»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«forgetful inheritance»#doc"
     description: "Design pattern for typeclass inheritance where we include all fields, even if they can be inferred."
     authors: the Mathlib community
     accessed_at: 2025-10-06
     category: explanation
     tags:
       - classes
   - title: "library note [custom simps projection]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«custom simps projection»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«custom simps projection»#doc"
     description: "How to register projections for the `@[simps]` attribute."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: how-to
     tags:
       - tactics
   - title: "library note [norm_num lemma function equality]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«norm_num lemma function equality»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«norm_num lemma function equality»#doc"
     description: "Why lemmas for the `norm_num` tactic use a parameter `f` and hypothesis `f = HAdd.add` instead of writing `+`."
     authors: the Mathlib community
     accessed_at: 2025-10-02
@@ -724,7 +724,7 @@ documentation:
       - declarations
       - metaprogramming
   - title: "library note [hom simp lemma priority]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«hom simp lemma priority»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«hom simp lemma priority»#doc"
     description: "Widely applicable `@[simp]` lemmas should receive `mid` priority."
     authors: the Mathlib community
     accessed_at: 2025-10-02
@@ -733,7 +733,7 @@ documentation:
       - classes
       - tactics
   - title: "library note [category theory universes]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«category theory universes»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«category theory universes»#doc"
     description: "Design patterns for ordering the universe levels in category theory declarations."
     authors: the Mathlib community
     accessed_at: 2025-10-02
@@ -742,15 +742,15 @@ documentation:
       - category theory
       - declarations
   - title: "library note [operator precedence of big operators]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«operator precedence of big operators»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«operator precedence of big operators»#doc"
     description: "The choice of operator precedence for `∏` and `∑` operators in Mathlib."
     authors: the Mathlib community
     accessed_at: 2025-10-02
     category: explanation
     tags:
       - group theory
   - title: "library note [bundled maps over different rings]"
-    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.LibraryNote.«bundled maps over different rings»#doc"
+    url: "https://leanprover-community.github.io/mathlib4_docs/find/?pattern=LibraryNote.«bundled maps over different rings»#doc"
     description: "A design trick for when bundled maps have stronger properties if certain typeclass assumptions are satisfied."
     authors: the Mathlib community
     accessed_at: 2025-10-02