refactor: make library notes a definition (#23767)

grunweg · Vierkantor · grunweg · commit d554a1878954 · 2025-10-09T10:59:05.000Z
Make library notes a definition of `Unit` type, whose doc-string is the note's content. As a consequence, - doc-gen will display all library notes without any custom logic, - library notes are shown upon hover (via the use of the doc-string), - go to definition for library notes is easy Automate this using a macro, which also enforces that all library notes are inside the Mathlib.LibraryNote namespace. *Temporarily*, we use the `library_note2` name; if/when the batteries version is changed, we can reclaim the original name. This PR does not address how to *refer* to library notes nicely (in a way that is shown in the documentation, checked for typos, with sufficient imports ensured etc.). That is left to a future PR. This is proposal 2a from this zulip discussion: [#mathlib4 > library notes @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/library.20notes/near/510614740) Co-authored-by: grunweg <rothgami@math.hu-berlin.de> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
diff --git a/Archive/Imo/Imo2019Q2.lean b/Archive/Imo/Imo2019Q2.lean
@@ -34,7 +34,7 @@ as `(2 : ℤ) • ∡ _ _ _ = (2 : ℤ) • ∡ _ _ _`.
 -/
 
 
-library_note "IMO geometry formalization conventions"/--
+library_note2 «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
@@ -75,7 +75,7 @@ theorem prod_val [CommMonoid M] (s : Finset M) : s.1.prod = s.prod id := by
 
 end Finset
 
-library_note "operator precedence of big operators"/--
+library_note2 «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
@@ -18,7 +18,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_note "change elaboration strategy with `by apply`"/--
+library_note2 «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
@@ -124,7 +124,7 @@ export AddAction (add_vadd)
 export SMulCommClass (smul_comm)
 export VAddCommClass (vadd_comm)
 
-library_note "bundled maps over different rings"/--
+library_note2 «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
@@ -164,7 +164,7 @@ theorem map_surjective {f : α →* β} (hf : Function.Surjective f) :
   obtain ⟨a, rfl⟩ := hf b
   exact ⟨ConjClasses.mk a, rfl⟩
 
-library_note "slow-failing instance priority"/--
+library_note2 «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
@@ -11,7 +11,7 @@ import Mathlib.Data.Nat.BinaryRec
 import Mathlib.Logic.Function.Defs
 import Mathlib.Tactic.MkIffOfInductiveProp
 import Mathlib.Tactic.OfNat
-import Mathlib.Tactic.Simps.Basic
+import Mathlib.Tactic.Basic
 
 /-!
 # Typeclasses for (semi)groups and monoids
@@ -265,7 +265,7 @@ end CommMagma
 @[ext]
 class LeftCancelSemigroup (G : Type u) extends Semigroup G, IsLeftCancelMul G
 
-library_note "lower cancel priority" /--
+library_note2 «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.
@@ -378,7 +378,7 @@ include hn ha
 
 end
 
-library_note "forgetful inheritance"/--
+library_note2 «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
@@ -193,7 +193,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_note "hom simp lemma priority"
+library_note2 «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
@@ -49,7 +49,7 @@ pointwise subtraction
 
 assert_not_exists Set.iUnion MulAction MonoidWithZero OrderedAddCommMonoid
 
-library_note "pointwise nat action"/--
+library_note2 «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/Pointwise/Set/Scalar.lean b/Mathlib/Algebra/Group/Pointwise/Set/Scalar.lean
@@ -49,18 +49,6 @@ pointwise subtraction
 
 assert_not_exists Set.iUnion MulAction MonoidWithZero OrderedAddCommMonoid
 
-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,
-`2 • {a, b}` can both be `{2 • a, 2 • b}` (pointwise action, pointwise repeated addition,
-`Set.smulSet`) and `{a + a, a + b, b + a, b + b}` (nat or int action, repeated pointwise
-addition, `Set.NSMul`).
-
-Because the pointwise action can easily be spelled out in such cases, we give higher priority to the
-nat and int actions.
--/
-
 open Function MulOpposite
 
 variable {F α β γ : Type*}
diff --git a/Mathlib/Algebra/Group/Submonoid/Operations.lean b/Mathlib/Algebra/Group/Submonoid/Operations.lean
@@ -610,7 +610,7 @@ variable {F : Type*} [FunLike F M N] [mc : MonoidHomClass F M N]
 
 open Submonoid
 
-library_note "range copy pattern"/--
+library_note2 «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
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Eric Wieser
 -/
 import Mathlib.Init
-import Batteries.Util.LibraryNote
+import Mathlib.Tactic.Basic
 
 /-!
 # Documentation of the algebraic hierarchy
@@ -18,7 +18,7 @@ TODO: Add sections about interactions with topological typeclasses, and order ty
 -/
 
 
-library_note "the algebraic hierarchy"/-- # The algebraic hierarchy
+library_note2 «the algebraic hierarchy» /-- # The algebraic hierarchy
 
 In any theorem proving environment,
 there are difficult decisions surrounding the design of the "algebraic hierarchy".
@@ -184,8 +184,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_note "reducible non-instances"/--
+library_note2 «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 `α`.
@@ -202,7 +201,7 @@ sometimes comes from `Units.Preorder` and sometimes from `Units.PartialOrder`.
 Therefore, `Preorder.lift` and `PartialOrder.lift` are marked `@[reducible]`.
 -/
 
-library_note "implicit instance arguments"/--
+library_note2 «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. When they can be inferred from these other
@@ -213,7 +212,7 @@ and `β` are `Semiring`s as `{rα : Semiring α} {rβ : Semiring β}` rather tha
 `[Semiring α] [Semiring β]`.
 -/
 
-library_note "lower instance priority"/--
+library_note2 «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
@@ -230,7 +229,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_note "instance argument order"/--
+library_note2 «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
@@ -47,7 +47,7 @@ Finitary versions of the current lemmas.
 
 assert_not_exists Field
 
-library_note "out-param inheritance"/--
+library_note2 «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
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 -/
 import Mathlib.Init
-import Batteries.Util.LibraryNote
+import Mathlib.Tactic.Basic
 
 /-!
 # Documentation concerning the continuous functional calculus
@@ -14,7 +14,7 @@ as the organizational structure within Mathlib.
 -/
 
 
-library_note "continuous functional calculus" /--
+library_note2 «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
@@ -52,7 +52,7 @@ namespace FiniteDimensional
 
 open RCLike
 
-library_note "RCLike instance"/--
+library_note2 «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
@@ -30,7 +30,7 @@ local notation:80 g " ⊚ " f:80 => CategoryTheory.CategoryStruct.comp f g    --
 -/
 
 
-library_note "CategoryTheory universes"
+library_note2 «CategoryTheory 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
@@ -37,7 +37,7 @@ Whenever you state a lemma about the coercion `ℚ≥0 → ℚ`, check that Lean
 
 assert_not_exists CompleteLattice OrderedCommMonoid
 
-library_note "specialised high priority simp lemma" /--
+library_note2 «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
@@ -40,7 +40,7 @@ instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] [Nat.AtLeas
     OfNat R n where
   ofNat := n.cast
 
-library_note "no_index around OfNat.ofNat"
+library_note2 «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)`.
@@ -68,7 +68,7 @@ class AddMonoidWithOne (R : Type*) extends NatCast R, AddMonoid R, One R where
 /-- An `AddCommMonoidWithOne` is an `AddMonoidWithOne` satisfying `a + b = b + a`. -/
 class AddCommMonoidWithOne (R : Type*) extends AddMonoidWithOne R, AddCommMonoid R
 
-library_note "coercion into rings"
+library_note2 «coercion into rings»
 /--
 Coercions such as `Nat.castCoe` that go from a concrete structure such as
 `ℕ` to an arbitrary ring `R` should be set up as follows:
diff --git a/Mathlib/Data/Nat/Init.lean b/Mathlib/Data/Nat/Init.lean
@@ -8,6 +8,7 @@ import Batteries.Tactic.Init
 import Mathlib.Init
 import Mathlib.Data.Int.Notation
 import Mathlib.Data.Nat.Notation
+import Mathlib.Tactic.Basic
 import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.TypeStar
 import Mathlib.Util.AssertExists
@@ -30,7 +31,7 @@ upstreamed to Batteries or the Lean standard library easily.
 See note [foundational algebra order theory].
 -/
 
-library_note "foundational algebra order theory"/--
+library_note2 «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
@@ -18,7 +18,7 @@ semigroups.
 
 open scoped Manifold ContDiff
 
-library_note "Design choices about smooth algebraic structures"/--
+library_note2 «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
@@ -773,7 +773,7 @@ lemma chartedSpace_of_discreteTopology_chartAt [TopologicalSpace M] [Topological
 
 section Products
 
-library_note "Manifold type tags" /-- For technical reasons we introduce two type tags:
+library_note2 «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
@@ -95,7 +95,7 @@ class Fact (p : Prop) : Prop where
   `Fact p`. -/
   out : p
 
-library_note "fact non-instances"/--
+library_note2 «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.
@@ -165,7 +165,7 @@ theorem by_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
 
 alias by_contra := by_contradiction
 
-library_note "decidable namespace"/--
+library_note2 «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.
@@ -174,7 +174,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_note "decidable arguments"/--
+library_note2 «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/Basic.lean b/Mathlib/Tactic/Basic.lean
@@ -126,3 +126,39 @@ elab (name := clearAuxDecl) "clear_aux_decl" : tactic => withMainContext do
 attribute [pp_with_univ] ULift PUnit PEmpty
 
 end Mathlib.Tactic
+
+/-- A mathlib library note: the note's content should be contained in its doc-string. -/
+def LibraryNote := Unit
+
+open Lean in
+/-- `library_note2 «my note» /-- documentation -/` creates a library note named `my note`
+in the `Mathlib.LibraryNote` namespace, whose content is `/-- documentation -/`.
+You can access this note using, for example, `#print Mathlib.LibraryNote.«my note»`.
+-/
+macro "library_note2 " name:ident ppSpace dc:docComment : command =>
+  `($dc:docComment def $(mkIdent (Name.append `Mathlib.LibraryNote name.getId)) : LibraryNote := ())
+
+open Lean Elab Command in
+/-- Support the old `library_note "foo"` syntax, with a deprecation warning. -/
+elab "library_note2 " name:str ppSpace dc:docComment : command => do
+  logWarningAt name <|
+    "deprecation warning: library_note2 now takes an identifier instead of a string.\n" ++
+    "Hint: replace the double quotes with «french quotes»."
+  let name := Name.mkSimple name.getString
+  let stx ← `(library_note2 $(mkIdent name):ident $dc:docComment)
+  elabCommandTopLevel stx
+
+library_note2 «partially-applied ext lemmas»
+/--
+When possible, `ext` lemmas are stated without a full set of arguments. As an example, for bundled
+homs `f`, `g`, and `of`, `f.comp of = g.comp of → f = g` is a better `ext` lemma than
+`(∀ x, f (of x) = g (of x)) → f = g`, as the former allows a second type-specific extensionality
+lemmas to be applied to `f.comp of = g.comp of`.
+If the domain of `of` is `ℕ` or `ℤ` and `of` is a `RingHom`, such a lemma could then make the goal
+`f (of 1) = g (of 1)`.
+
+For bundled morphisms, there is a `ext` lemma that always applies of the form
+`(∀ x, ⇑f x = ⇑g x) → f = g`. When adding type-specific `ext` lemmas like the one above, we want
+these to be tried first. This happens automatically since the type-specific lemmas are inevitably
+defined later.
+-/
diff --git a/Mathlib/Tactic/NormNum/Basic.lean b/Mathlib/Tactic/NormNum/Basic.lean
@@ -137,7 +137,7 @@ theorem isintCast {R} [Ring R] (n m : ℤ) :
 
 /-! # Arithmetic -/
 
-library_note "norm_num lemma function equality"/--
+library_note2 «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
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 -/
 
-import Mathlib.Init
+import Mathlib.Tactic.Basic
 import Aesop
 
 /-!
@@ -18,7 +18,7 @@ so we must put this declaration into its own file.
 declare_aesop_rule_sets [SetLike] (default := true)
 declare_aesop_rule_sets [SetLike!] (default := false)
 
-library_note "SetLike Aesop ruleset"/--
+library_note2 «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
@@ -7,6 +7,7 @@ import Lean.Elab.Tactic.Simp
 import Lean.Elab.App
 import Mathlib.Tactic.Simps.NotationClass
 import Mathlib.Lean.Expr.Basic
+import Mathlib.Tactic.Basic
 
 /-!
 # Simps attribute
@@ -832,7 +833,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_note "custom simps projection" /--
+library_note2 «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/InfiniteSum/Defs.lean b/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
@@ -149,7 +149,7 @@ notation3 "∏'[" L "]" (...)", "r:67:(scoped f => tprod f L) => r
 @[inherit_doc tsum]
 notation3 "∑'[" L "]" (...)", "r:67:(scoped f => tsum f L) => r
 
--- see Note [operator precedence of big operators]
+-- see note [operator precedence of big operators]
 @[inherit_doc tprod]
 notation3 "∏' "(...)", "r:67:(scoped f => tprod f (unconditional _)) => r
 @[inherit_doc tsum]
diff --git a/Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean b/Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean
diff --git a/Mathlib/Topology/Continuous.lean b/Mathlib/Topology/Continuous.lean
