chore: remove outdated library_note2 usage (leanprover-community#33868)

Vierkantor · Vierkantor · commit 77ff30aa48cb · 2026-01-12T13:34:25.000Z
Mathlib's custom version of library notes is now implemented in Batteries, so we don't need the duplicate `library_note2` command. This PR does a search and replace turning `library_note2` into `library_note`. The syntax remains the same, so search and replace is all that is needed.

Co-authored-by: Anne C.A. Baanen &lt;vierkantor@vierkantor.com&gt;
diff --git a/Archive/Imo/Imo2019Q2.lean b/Archive/Imo/Imo2019Q2.lean
@@ -34,7 +34,7 @@ as `(2 : ℤ) • ∡ _ _ _ = (2 : ℤ) • ∡ _ _ _`.
 -/
 
 
-library_note2 «IMO geometry formalization conventions» /--
+library_note «IMO geometry formalization conventions» /--
 We apply the following conventions for formalizing IMO geometry problems. A problem is assumed
 to take place in the plane unless that is clearly not intended, so it is not required to prove
 that the points are coplanar (whether or not that in fact follows from the other conditions).
diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
@@ -79,7 +79,7 @@ theorem prod_val [CommMonoid M] (s : Finset M) : s.1.prod = s.prod id := by
 
 end Finset
 
-library_note2 «operator precedence of big operators» /--
+library_note «operator precedence of big operators» /--
 There is no established mathematical convention
 for the operator precedence of big operators like `∏` and `∑`.
 We will have to make a choice.
diff --git a/Mathlib/Algebra/Category/Ring/Limits.lean b/Mathlib/Algebra/Category/Ring/Limits.lean
@@ -22,7 +22,7 @@ the underlying types are just the limits in the category of types.
 
 
 -- We use the following trick a lot of times in this file.
-library_note2 «change elaboration strategy with `by apply`» /--
+library_note «change elaboration strategy with `by apply`» /--
 Some definitions may be extremely slow to elaborate, when the target type to be constructed
 is complicated and when the type of the term given in the definition is also complicated and does
 not obviously match the target type. In this case, instead of just giving the term, prefixing it
diff --git a/Mathlib/Algebra/Group/Action/Defs.lean b/Mathlib/Algebra/Group/Action/Defs.lean
@@ -153,7 +153,7 @@ export AddSemigroupAction (add_vadd)
 export SMulCommClass (smul_comm)
 export VAddCommClass (vadd_comm)
 
-library_note2 «bundled maps over different rings» /--
+library_note «bundled maps over different rings» /--
 Frequently, we find ourselves wanting to express a bilinear map `M →ₗ[R] N →ₗ[R] P` or an
 equivalence between maps `(M →ₗ[R] N) ≃ₗ[R] (M' →ₗ[R] N')` where the maps have an associated ring
 `R`. Unfortunately, using definitions like these requires that `R` satisfy `CommSemiring R`, and
diff --git a/Mathlib/Algebra/Group/Conj.lean b/Mathlib/Algebra/Group/Conj.lean
@@ -168,7 +168,7 @@ theorem map_surjective {f : α →* β} (hf : Function.Surjective f) :
   obtain ⟨a, rfl⟩ := hf b
   exact ⟨ConjClasses.mk a, rfl⟩
 
-library_note2 «slow-failing instance priority» /--
+library_note «slow-failing instance priority» /--
 Certain instances trigger further searches when they are considered as candidate instances;
 these instances should be assigned a priority lower than the default of 1000 (for example, 900).
 
diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
@@ -266,7 +266,7 @@ end CommMagma
 @[ext]
 class LeftCancelSemigroup (G : Type u) extends Semigroup G, IsLeftCancelMul G
 
-library_note2 «lower cancel priority» /--
+library_note «lower cancel priority» /--
 We lower the priority of inheriting from cancellative structures.
 This attempts to avoid expensive checks involving bundling and unbundling with the `IsDomain` class.
 since `IsDomain` already depends on `Semiring`, we can synthesize that one first.
@@ -402,7 +402,7 @@ include hn ha
 
 end
 
-library_note2 «forgetful inheritance» /--
+library_note «forgetful inheritance» /--
 Suppose that one can put two mathematical structures on a type, a rich one `R` and a poor one
 `P`, and that one can deduce the poor structure from the rich structure through a map `F` (called a
 forgetful functor) (think `R = MetricSpace` and `P = TopologicalSpace`). A possible
diff --git a/Mathlib/Algebra/Group/Hom/Defs.lean b/Mathlib/Algebra/Group/Hom/Defs.lean
@@ -197,7 +197,7 @@ instance OneHom.funLike : FunLike (OneHom M N) M N where
 instance OneHom.oneHomClass : OneHomClass (OneHom M N) M N where
   map_one := OneHom.map_one'
 
-library_note2 «hom simp lemma priority»
+library_note «hom simp lemma priority»
 /--
 The hom class hierarchy allows for a single lemma, such as `map_one`, to apply to a large variety
 of morphism types, so long as they have an instance of `OneHomClass`. For example, this applies to
diff --git a/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean b/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@@ -53,7 +53,7 @@ pointwise subtraction
 
 assert_not_exists Set.iUnion MulAction MonoidWithZero IsOrderedMonoid
 
-library_note2 «pointwise nat action» /--
+library_note «pointwise nat action» /--
 Pointwise monoids (`Set`, `Finset`, `Filter`) have derived pointwise actions of the form
 `SMul α β → SMul α (Set β)`. When `α` is `ℕ` or `ℤ`, this action conflicts with the
 nat or int action coming from `Set β` being a `Monoid` or `DivInvMonoid`. For example,
diff --git a/Mathlib/Algebra/Group/Submonoid/Operations.lean b/Mathlib/Algebra/Group/Submonoid/Operations.lean
@@ -619,7 +619,7 @@ variable {F : Type*} [FunLike F M N] [mc : MonoidHomClass F M N]
 
 open Submonoid
 
-library_note2 «range copy pattern» /--
+library_note «range copy pattern» /--
 For many categories (monoids, modules, rings, ...) the set-theoretic image of a morphism `f` is
 a subobject of the codomain. When this is the case, it is useful to define the range of a morphism
 in such a way that the underlying carrier set of the range subobject is definitionally
diff --git a/Mathlib/Algebra/HierarchyDesign.lean b/Mathlib/Algebra/HierarchyDesign.lean
@@ -22,7 +22,7 @@ TODO: Add sections about interactions with topological typeclasses, and order ty
 @[expose] public section
 
 
-library_note2 «the algebraic hierarchy» /-- # The algebraic hierarchy
+library_note «the algebraic hierarchy» /-- # The algebraic hierarchy
 
 In any theorem proving environment,
 there are difficult decisions surrounding the design of the "algebraic hierarchy".
@@ -189,7 +189,7 @@ Hopefully this document makes it easy to assemble this list.
 Another alternative to a TODO list in the doc-strings is adding Github issues.
 -/
 
-library_note2 «reducible non-instances» /--
+library_note «reducible non-instances» /--
 Some definitions that define objects of a class cannot be instances, because they have an
 explicit argument that does not occur in the conclusion. An example is `Preorder.lift` that has a
 function `f : α → β` as an explicit argument to lift a preorder on `β` to a preorder on `α`.
@@ -206,7 +206,7 @@ sometimes comes from `Units.Preorder` and sometimes from `Units.PartialOrder`.
 Therefore, `Preorder.lift` and `PartialOrder.lift` are marked `@[reducible]`.
 -/
 
-library_note2 «implicit instance arguments» /--
+library_note «implicit instance arguments» /--
 There are places where typeclass arguments are specified with implicit `{}` brackets instead of
 the usual `[]` brackets. This is done when the instances can be inferred because they are implicit
 arguments to the type of one of the other arguments. There are several reasons for doing so.
@@ -226,7 +226,7 @@ abelian groups, but terms `A : ModuleCat ℤ` come with two (propeq) `Module ℤ
 one from being `ℤ`-modules, and one from being abelian groups.
 -/
 
-library_note2 «lower instance priority» /--
+library_note «lower instance priority» /--
 Certain instances always apply during type-class resolution. For example, the instance
 `AddCommGroup.toAddGroup {α} [AddCommGroup α] : AddGroup α` applies to all type-class
 resolution problems of the form `AddGroup _`, and type-class inference will then do an
@@ -243,7 +243,7 @@ Therefore, if we create an instance that always applies, we set the priority of
 100 (or something similar, which is below the default value of 1000).
 -/
 
-library_note2 «instance argument order» /--
+library_note «instance argument order» /--
 When type class inference applies an instance, it attempts to solve the sub-goals from left to
 right (it used to be from right to left in lean 3). For example in
 ```
diff --git a/Mathlib/Algebra/Order/Hom/Basic.lean b/Mathlib/Algebra/Order/Hom/Basic.lean
@@ -51,7 +51,7 @@ Finitary versions of the current lemmas.
 
 assert_not_exists Field
 
-library_note2 «out-param inheritance» /--
+library_note «out-param inheritance» /--
 Diamond inheritance cannot depend on `outParam`s in the following circumstances:
 * there are three classes `Top`, `Middle`, `Bottom`
 * all of these classes have a parameter `(α : outParam _)`
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Note.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Note.lean
@@ -18,7 +18,7 @@ as the organizational structure within Mathlib.
 @[expose] public section
 
 
-library_note2 «continuous functional calculus» /--
+library_note «continuous functional calculus» /--
 # The continuous functional calculus
 
 In Mathlib, there are two classes --- `NonUnitalContinuousFunctionalCalculus` and
diff --git a/Mathlib/Analysis/RCLike/Lemmas.lean b/Mathlib/Analysis/RCLike/Lemmas.lean
@@ -56,7 +56,7 @@ namespace FiniteDimensional
 
 open RCLike
 
-library_note2 «RCLike instance» /--
+library_note «RCLike instance» /--
 This instance generates a type-class problem with a metavariable `?m` that should satisfy
 `RCLike ?m`. Since this can only be satisfied by `ℝ` or `ℂ`, this does not cause problems. -/
 
diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -34,7 +34,7 @@ local notation:80 g " ⊚ " f:80 => CategoryTheory.CategoryStruct.comp f g    --
 @[expose] public section
 
 
-library_note2 «category theory universes»
+library_note «category theory universes»
 /--
 The typeclass `Category C` describes morphisms associated to objects of type `C : Type u`.
 
diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean
@@ -41,7 +41,7 @@ Whenever you state a lemma about the coercion `ℚ≥0 → ℚ`, check that Lean
 
 assert_not_exists CompleteLattice IsOrderedMonoid
 
-library_note2 «specialised high priority simp lemma» /--
+library_note «specialised high priority simp lemma» /--
 It sometimes happens that a `@[simp]` lemma declared early in the library can be proved by `simp`
 using later, more general simp lemmas. In that case, the following reasons might be arguments for
 the early lemma to be tagged `@[simp high]` (rather than `@[simp, nolint simpNF]` or
diff --git a/Mathlib/Data/Nat/Cast/Defs.lean b/Mathlib/Data/Nat/Cast/Defs.lean
@@ -43,7 +43,7 @@ instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] [Nat.AtLeas
     OfNat R n where
   ofNat := n.cast
 
-library_note2 «no_index around OfNat.ofNat»
+library_note «no_index around OfNat.ofNat»
 /--
 When writing lemmas about `OfNat.ofNat` that assume `Nat.AtLeastTwo`, the term needs to be wrapped
 in `no_index` so as not to confuse `simp`, as `no_index (OfNat.ofNat n)`.
diff --git a/Mathlib/Data/Nat/Init.lean b/Mathlib/Data/Nat/Init.lean
@@ -34,7 +34,7 @@ See note [foundational algebra order theory].
 
 @[expose] public section
 
-library_note2 «foundational algebra order theory» /--
+library_note «foundational algebra order theory» /--
 Batteries has a home-baked development of the algebraic and order-theoretic theory of `ℕ` and `ℤ`
 which, in particular, is not typeclass-mediated. This is useful to set up the algebra and finiteness
 libraries in mathlib (naturals and integers show up as indices/offsets in lists, cardinality in
diff --git a/Mathlib/Geometry/Manifold/Algebra/Monoid.lean b/Mathlib/Geometry/Manifold/Algebra/Monoid.lean
@@ -22,7 +22,7 @@ semigroups.
 
 open scoped Manifold ContDiff
 
-library_note2 «Design choices about smooth algebraic structures» /--
+library_note «Design choices about smooth algebraic structures» /--
 1. All `C^n` algebraic structures on `G` are `Prop`-valued classes that extend
 `IsManifold I n G`. This way we save users from adding both
 `[IsManifold I n G]` and `[ContMDiffMul I n G]` to the assumptions. While many API
diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean
@@ -777,7 +777,7 @@ lemma chartedSpace_of_discreteTopology_chartAt [TopologicalSpace M] [Topological
 
 section Products
 
-library_note2 «Manifold type tags» /-- For technical reasons we introduce two type tags:
+library_note «Manifold type tags» /-- For technical reasons we introduce two type tags:
 
 * `ModelProd H H'` is the same as `H × H'`;
 * `ModelPi H` is the same as `∀ i, H i`, where `H : ι → Type*` and `ι` is a finite type.
diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean
@@ -96,7 +96,7 @@ class Fact (p : Prop) : Prop where
   `Fact p`. -/
   out : p
 
-library_note2 «fact non-instances» /--
+library_note «fact non-instances» /--
 In most cases, we should not have global instances of `Fact`; typeclass search is not an
 advanced proof search engine, and adding any such instance has the potential to cause
 slowdowns everywhere. We instead declare them as lemmata and make them local instances as required.
@@ -167,7 +167,7 @@ theorem by_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
 
 alias by_contra := by_contradiction
 
-library_note2 «decidable namespace» /--
+library_note «decidable namespace» /--
 In most of mathlib, we use the law of excluded middle (LEM) and the axiom of choice (AC) freely.
 The `Decidable` namespace contains versions of lemmas from the root namespace that explicitly
 attempt to avoid the axiom of choice, usually by adding decidability assumptions on the inputs.
@@ -176,7 +176,7 @@ You can check if a lemma uses the axiom of choice by using `#print axioms foo` a
 `Classical.choice` appears in the list.
 -/
 
-library_note2 «decidable arguments» /--
+library_note «decidable arguments» /--
 As mathlib is primarily classical,
 if the type signature of a `def` or `lemma` does not require any `Decidable` instances to state,
 it is preferable not to introduce any `Decidable` instances that are needed in the proof
diff --git a/Mathlib/Tactic/NormNum/Basic.lean b/Mathlib/Tactic/NormNum/Basic.lean
@@ -155,7 +155,7 @@ theorem isintCast {R} [Ring R] (n m : ℤ) :
 
 /-! ### Arithmetic -/
 
-library_note2 «norm_num lemma function equality» /--
+library_note «norm_num lemma function equality» /--
 Note: Many of the lemmas in this file use a function equality hypothesis like `f = HAdd.hAdd`
 below. The reason for this is that when this is applied, to prove e.g. `100 + 200 = 300`, the
 `+` here is `HAdd.hAdd` with an instance that may not be syntactically equal to the one supplied
diff --git a/Mathlib/Tactic/SetLike.lean b/Mathlib/Tactic/SetLike.lean
@@ -23,7 +23,7 @@ public meta section
 declare_aesop_rule_sets [SetLike] (default := true)
 declare_aesop_rule_sets [SetLike!] (default := false)
 
-library_note2 «SetLike Aesop ruleset» /--
+library_note «SetLike Aesop ruleset» /--
 The Aesop tactic (`aesop`) can automatically prove obvious facts about membership in structures
 such as subgroups and subrings. Certain lemmas regarding membership in algebraic substructures
 are given the `aesop` attribute according to the following principles:
diff --git a/Mathlib/Tactic/Simps/Basic.lean b/Mathlib/Tactic/Simps/Basic.lean
@@ -839,7 +839,7 @@ def getRawProjections (stx : Syntax) (str : Name) (traceIfExists : Bool := false
   trace[simps.debug] "Generated raw projection data:{indentD <| toMessageData (rawLevels, projs)}"
   pure (rawLevels, projs)
 
-library_note2 «custom simps projection» /--
+library_note «custom simps projection» /--
 You can specify custom projections for the `@[simps]` attribute.
 To do this for the projection `MyStructure.originalProjection` by adding a declaration
 `MyStructure.Simps.myProjection` that is definitionally equal to
diff --git a/Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean b/Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean
@@ -329,7 +329,7 @@ theorem nonarchimedean (hB : SubmodulesBasis B) : @NonarchimedeanAddGroup M _ hB
     hB.toModuleFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff.mp hU
   exact ⟨hB.openAddSubgroup i, hi⟩
 
-library_note2 «non-Archimedean non-instances» /--
+library_note «non-Archimedean non-instances» /--
 The non-Archimedean subgroup basis lemmas cannot be instances because some instances
 (such as `MeasureTheory.AEEqFun.instAddMonoid` or `IsTopologicalAddGroup.toContinuousAdd`)
 cause the search for `@IsTopologicalAddGroup β ?m1 ?m2`, i.e. a search for a topological group where
diff --git a/Mathlib/Topology/Continuous.lean b/Mathlib/Topology/Continuous.lean
@@ -315,7 +315,7 @@ theorem DenseRange.mem_nhds (h : DenseRange f) (hs : s ∈ 𝓝 x) :
 
 end DenseRange
 
-library_note2 «continuity lemma statement» /--
+library_note «continuity lemma statement» /--
 The library contains many lemmas stating that functions/operations are continuous. There are many
 ways to formulate the continuity of operations. Some are more convenient than others.
 Note: for the most part this note also applies to other properties
@@ -413,7 +413,7 @@ With `ContinuousAt` you can be even more precise about what to prove in case of
 see e.g. `ContinuousAt.comp_div_cases`.
 -/
 
-library_note2 «comp_of_eq lemmas» /--
+library_note «comp_of_eq lemmas» /--
 Lean's elaborator has trouble elaborating applications of lemmas that state that the composition of
 two functions satisfy some property at a point, like `ContinuousAt.comp` / `ContDiffAt.comp` and
 `ContMDiffWithinAt.comp`. The reason is that a lemma like this looks like
