From 1f7bcc040b85e25891dbd3d58c75fa8613aa7be9 Mon Sep 17 00:00:00 2001
From: blizzard_inc <edegeltje@gmail.com>
Date: Sat, 14 Sep 2024 19:04:55 +0200
Subject: [PATCH 01/21] Add check_note command

---
 Batteries/Util/LibraryNote.lean | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index 8c1d45f786..e9b97fb899 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -35,6 +35,34 @@ creates a new "library note", which can then be cross-referenced using
 -- See note [some tag]
 ```
 in doc-comments.
+Use `#check_note "some tag"` to display all notes with the tag 
+`"some tag"` in the infoview.
 -/
 elab "library_note " title:strLit ppSpace text:docComment : command => do
   modifyEnv (libraryNoteExt.addEntry · (title.getString, text.getDocString))
+
+/--
+`#check_note "some tag"` displays all library notes with tag 
+`"some tag"` in the infoview.
+The command only displays the library notes that are declared in 
+imported files or in the same file above the line containing the command.
+-/
+elab "#check_note" name:strLit : command => do
+  let env ← getEnv
+  
+  -- get the library notes from both this and imported files
+  let local_entries := libraryNoteExt.getEntries env
+  let imported_entries := (libraryNoteExt.toEnvExtension.getState env).importedEntries
+
+  -- filter for the appropriate notes while casting to list
+  let entry_name := name.getString
+  let imported_entries_filtered := imported_entries.flatten.toList.filterMap
+    (fun x => if x.fst == entry_name then Option.some x.snd else Option.none)
+  let valid_entries := imported_entries_filtered ++ local_entries.filterMap 
+    (fun x => if x.fst == entry_name then some x.snd else none)
+
+  -- display results in a readable style
+  if valid_entries.isEmpty then
+    logInfo "Note not found"
+  else
+    logInfo <| "\n\n".intercalate <| valid_entries.reverse.map ("/--" ++ · ++ "-/") 

From 4f13b7c68e29a34d7cece4f2da21cdfc59ce8ef1 Mon Sep 17 00:00:00 2001
From: blizzard_inc <edegeltje@gmail.com>
Date: Thu, 19 Sep 2024 21:34:43 +0200
Subject: [PATCH 02/21] Update LibraryNote.lean

remove trailing whitespace
---
 Batteries/Util/LibraryNote.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index e9b97fb899..9ac618d0f8 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -35,21 +35,21 @@ creates a new "library note", which can then be cross-referenced using
 -- See note [some tag]
 ```
 in doc-comments.
-Use `#check_note "some tag"` to display all notes with the tag 
+Use `#check_note "some tag"` to display all notes with the tag
 `"some tag"` in the infoview.
 -/
 elab "library_note " title:strLit ppSpace text:docComment : command => do
   modifyEnv (libraryNoteExt.addEntry · (title.getString, text.getDocString))
 
 /--
-`#check_note "some tag"` displays all library notes with tag 
+`#check_note "some tag"` displays all library notes with tag
 `"some tag"` in the infoview.
-The command only displays the library notes that are declared in 
+The command only displays the library notes that are declared in
 imported files or in the same file above the line containing the command.
 -/
 elab "#check_note" name:strLit : command => do
   let env ← getEnv
-  
+
   -- get the library notes from both this and imported files
   let local_entries := libraryNoteExt.getEntries env
   let imported_entries := (libraryNoteExt.toEnvExtension.getState env).importedEntries
@@ -58,11 +58,11 @@ elab "#check_note" name:strLit : command => do
   let entry_name := name.getString
   let imported_entries_filtered := imported_entries.flatten.toList.filterMap
     (fun x => if x.fst == entry_name then Option.some x.snd else Option.none)
-  let valid_entries := imported_entries_filtered ++ local_entries.filterMap 
+  let valid_entries := imported_entries_filtered ++ local_entries.filterMap
     (fun x => if x.fst == entry_name then some x.snd else none)
 
   -- display results in a readable style
   if valid_entries.isEmpty then
     logInfo "Note not found"
   else
-    logInfo <| "\n\n".intercalate <| valid_entries.reverse.map ("/--" ++ · ++ "-/") 
+    logInfo <| "\n\n".intercalate <| valid_entries.reverse.map ("/--" ++ · ++ "-/")

From 2b3dc76f8138f75f949be23a4024e254abb01d7e Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Thu, 26 Sep 2024 23:37:47 +0200
Subject: [PATCH 03/21] i promise it builds this time

---
 Batteries/Util/LibraryNote.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index 9ac618d0f8..f8b5313e61 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -41,6 +41,8 @@ Use `#check_note "some tag"` to display all notes with the tag
 elab "library_note " title:strLit ppSpace text:docComment : command => do
   modifyEnv (libraryNoteExt.addEntry · (title.getString, text.getDocString))
 
+
+open Lean Parser in
 /--
 `#check_note "some tag"` displays all library notes with tag
 `"some tag"` in the infoview.

From 479c45c5cc3f838ed905a303db96fb7ea196d292 Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Wed, 16 Oct 2024 11:20:12 +0200
Subject: [PATCH 04/21] change to #help

---
 Batteries/Util/LibraryNote.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index f8b5313e61..df9df5bb42 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -44,12 +44,12 @@ elab "library_note " title:strLit ppSpace text:docComment : command => do
 
 open Lean Parser in
 /--
-`#check_note "some tag"` displays all library notes with tag
+`#help note "some tag"` displays all library notes with tag
 `"some tag"` in the infoview.
 The command only displays the library notes that are declared in
 imported files or in the same file above the line containing the command.
 -/
-elab "#check_note" name:strLit : command => do
+elab "#help note" name:strLit : command => do
   let env ← getEnv
 
   -- get the library notes from both this and imported files

From 600ce8027c5d009225f009e7b5668e6111447252 Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Wed, 16 Oct 2024 11:22:55 +0200
Subject: [PATCH 05/21] more switching, adding authorship

---
 Batteries/Util/LibraryNote.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index df9df5bb42..5802b7ceea 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Gabriel Ebner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner
+Authors: Gabriel Ebner, Edward van de Meent
 -/
 import Lean.Elab.Command
 
@@ -35,7 +35,7 @@ creates a new "library note", which can then be cross-referenced using
 -- See note [some tag]
 ```
 in doc-comments.
-Use `#check_note "some tag"` to display all notes with the tag
+Use `#help note "some tag"` to display all notes with the tag
 `"some tag"` in the infoview.
 -/
 elab "library_note " title:strLit ppSpace text:docComment : command => do

From 7b56b6f516305af821cf581d9375d12962fc407c Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Wed, 16 Oct 2024 11:54:43 +0200
Subject: [PATCH 06/21] improve style, add test

---
 Batteries/Util/LibraryNote.lean |  3 ++-
 test/library_note.lean          | 43 +++++++++++++++++++++++++++++++++
 2 files changed, 45 insertions(+), 1 deletion(-)
 create mode 100644 test/library_note.lean

diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index 5802b7ceea..2e91d1bfd9 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -67,4 +67,5 @@ elab "#help note" name:strLit : command => do
   if valid_entries.isEmpty then
     logInfo "Note not found"
   else
-    logInfo <| "\n\n".intercalate <| valid_entries.reverse.map ("/--" ++ · ++ "-/")
+    logInfo <| "\n\n".intercalate <|
+      valid_entries.reverse.map ("/--\n" ++ String.trim · ++ "\n-/")
diff --git a/test/library_note.lean b/test/library_note.lean
new file mode 100644
index 0000000000..9ad4c0adff
--- /dev/null
+++ b/test/library_note.lean
@@ -0,0 +1,43 @@
+import Batteries.Util.LibraryNote
+
+
+/--
+info: Note not found
+-/
+#guard_msgs in
+#help note "test"
+
+library_note "test"
+/-- Lorem ipsum dolor sit amet, consectetur adipiscing elit.
+Sed viverra.
+-/
+
+/--
+info: /--
+Lorem ipsum dolor sit amet, consectetur adipiscing elit.
+Sed viverra.
+-/
+-/
+#guard_msgs in
+#help note "test"
+
+
+library_note "test" /--
+Cras ut luctus neque.
+Mauris ullamcorper turpis in eros vulputate.
+-/
+
+
+/--
+info: /--
+Lorem ipsum dolor sit amet, consectetur adipiscing elit.
+Sed viverra.
+-/
+
+/--
+Cras ut luctus neque.
+Mauris ullamcorper turpis in eros vulputate.
+-/
+-/
+#guard_msgs in
+#help note "test"

From 174a55ce5f499ac0c59e5a6d3b3f9cb643bf1721 Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Wed, 16 Oct 2024 12:36:42 +0200
Subject: [PATCH 07/21] add additional notes for testing, test imported notes.
 make sure the order is correct.

---
 Batteries/Test/Internal/DummyLibraryNote.lean | 10 +++++
 .../Test/Internal/DummyLibraryNote2.lean      |  6 +++
 Batteries/Util/LibraryNote.lean               |  4 +-
 test/library_note.lean                        | 40 ++++++++++---------
 4 files changed, 39 insertions(+), 21 deletions(-)
 create mode 100644 Batteries/Test/Internal/DummyLibraryNote.lean
 create mode 100644 Batteries/Test/Internal/DummyLibraryNote2.lean

diff --git a/Batteries/Test/Internal/DummyLibraryNote.lean b/Batteries/Test/Internal/DummyLibraryNote.lean
new file mode 100644
index 0000000000..ff7cf78902
--- /dev/null
+++ b/Batteries/Test/Internal/DummyLibraryNote.lean
@@ -0,0 +1,10 @@
+import Batteries.Util.LibraryNote
+
+library_note "test" /--
+1: This is a testnote for testing the library note feature of batteries.
+The `#help note` command should be able to find this note when imported.
+-/
+
+library_note "test" /--
+2: This is a second testnote for testing the library note feature of batteries.
+-/
diff --git a/Batteries/Test/Internal/DummyLibraryNote2.lean b/Batteries/Test/Internal/DummyLibraryNote2.lean
new file mode 100644
index 0000000000..1dd8f4961f
--- /dev/null
+++ b/Batteries/Test/Internal/DummyLibraryNote2.lean
@@ -0,0 +1,6 @@
+import Batteries.Test.Internal.DummyLibraryNote
+
+library_note "test" /--
+3: this is a note in a different file importing the above testnotes,
+but still imported by the actual testfile.
+-/
diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index 2e91d1bfd9..2a27e0b96d 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -53,7 +53,7 @@ elab "#help note" name:strLit : command => do
   let env ← getEnv
 
   -- get the library notes from both this and imported files
-  let local_entries := libraryNoteExt.getEntries env
+  let local_entries := (libraryNoteExt.getEntries env).reverse
   let imported_entries := (libraryNoteExt.toEnvExtension.getState env).importedEntries
 
   -- filter for the appropriate notes while casting to list
@@ -68,4 +68,4 @@ elab "#help note" name:strLit : command => do
     logInfo "Note not found"
   else
     logInfo <| "\n\n".intercalate <|
-      valid_entries.reverse.map ("/--\n" ++ String.trim · ++ "\n-/")
+      valid_entries.map ("/--\n" ++ String.trim · ++ "\n-/")
diff --git a/test/library_note.lean b/test/library_note.lean
index 9ad4c0adff..34cab0f486 100644
--- a/test/library_note.lean
+++ b/test/library_note.lean
@@ -1,42 +1,44 @@
 import Batteries.Util.LibraryNote
-
+import Batteries.Test.Internal.DummyLibraryNote2
 
 /--
 info: Note not found
 -/
 #guard_msgs in
-#help note "test"
+#help note "no note"
+
+library_note "test"/--
+4: This note was not imported, and therefore appears below the imported notes.
+-/
 
-library_note "test"
-/-- Lorem ipsum dolor sit amet, consectetur adipiscing elit.
-Sed viverra.
+library_note "test"/--
+5: This note was also not imported, and therefore appears below the imported notes,
+and the previously added note.
 -/
 
+
 /--
 info: /--
-Lorem ipsum dolor sit amet, consectetur adipiscing elit.
-Sed viverra.
--/
+1: This is a testnote for testing the library note feature of batteries.
+The `#help note` command should be able to find this note when imported.
 -/
-#guard_msgs in
-#help note "test"
-
 
-library_note "test" /--
-Cras ut luctus neque.
-Mauris ullamcorper turpis in eros vulputate.
+/--
+2: This is a second testnote for testing the library note feature of batteries.
 -/
 
+/--
+3: this is a note in a different file importing the above testnotes,
+but still imported by the actual testfile.
+-/
 
 /--
-info: /--
-Lorem ipsum dolor sit amet, consectetur adipiscing elit.
-Sed viverra.
+4: This note was not imported, and therefore appears below the imported notes.
 -/
 
 /--
-Cras ut luctus neque.
-Mauris ullamcorper turpis in eros vulputate.
+5: This note was also not imported, and therefore appears below the imported notes,
+and the previously added note.
 -/
 -/
 #guard_msgs in

From 4201f3af8c8f812fdc8e71e6d5f8641c58fe6c56 Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Wed, 16 Oct 2024 13:40:58 +0200
Subject: [PATCH 08/21] fix batteries.lean, add code for prefix search.

---
 Batteries.lean                  |  2 ++
 Batteries/Util/LibraryNote.lean | 25 +++++++++++++++++++++++++
 2 files changed, 27 insertions(+)

diff --git a/Batteries.lean b/Batteries.lean
index 7d3486f15b..ba63eb231e 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -95,6 +95,8 @@ import Batteries.Tactic.SqueezeScope
 import Batteries.Tactic.Unreachable
 import Batteries.Tactic.Where
 import Batteries.Test.Internal.DummyLabelAttr
+import Batteries.Test.Internal.DummyLibraryNote
+import Batteries.Test.Internal.DummyLibraryNote2
 import Batteries.Util.Cache
 import Batteries.Util.ExtendedBinder
 import Batteries.Util.LibraryNote
diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index 2a27e0b96d..86c3a63303 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -69,3 +69,28 @@ elab "#help note" name:strLit : command => do
   else
     logInfo <| "\n\n".intercalate <|
       valid_entries.map ("/--\n" ++ String.trim · ++ "\n-/")
+
+  -- for when `List.nil_ne_mem_groupBy` has landed in batteries or higher in the hierarchy.
+  /-
+  let imported_entries_filtered := imported_entries.flatten.toList.filterMap
+    (fun x => if entry_name.isPrefixOf x.fst then some x else Option.none)
+  let valid_entries := imported_entries_filtered ++ local_entries.filterMap
+    (fun x => if entry_name.isPrefixOf x.fst then some x else none)
+
+  let grouped_valid_entries := valid_entries.mergeSort (·.fst ≤ ·.fst)
+    |>.groupBy (·.fst == ·.fst)
+
+  -- display results in a readable style
+  if grouped_valid_entries.isEmpty then
+    logInfo "Note not found"
+  else
+    logInfo <| "\n\n".intercalate <|
+      grouped_valid_entries.attach.map (fun ⟨l,h⟩ =>
+        "library_note \"" ++ (l.head (by
+          unfold grouped_valid_entries at h
+          -- `exact List.nil_ne_mem_groupBy h`
+          -- from mathlib would prove this
+          sorry)
+          ).fst ++ "\"\n"
+        ++ ("\n\n".intercalate <| l.map (fun e => "/--\n" ++ e.snd.trim ++ "\n-/")))
+  -/

From e31da2fce0fb42eed973719f88e22df0bdb59604 Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Wed, 16 Oct 2024 13:48:24 +0200
Subject: [PATCH 09/21] fix typo

---
 Batteries/Util/LibraryNote.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index 86c3a63303..37590cb7e8 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -70,7 +70,7 @@ elab "#help note" name:strLit : command => do
     logInfo <| "\n\n".intercalate <|
       valid_entries.map ("/--\n" ++ String.trim · ++ "\n-/")
 
-  -- for when `List.nil_ne_mem_groupBy` has landed in batteries or higher in the hierarchy.
+  -- for when `List.nil_not_mem_groupBy` has landed in batteries or higher in the hierarchy.
   /-
   let imported_entries_filtered := imported_entries.flatten.toList.filterMap
     (fun x => if entry_name.isPrefixOf x.fst then some x else Option.none)
@@ -88,7 +88,7 @@ elab "#help note" name:strLit : command => do
       grouped_valid_entries.attach.map (fun ⟨l,h⟩ =>
         "library_note \"" ++ (l.head (by
           unfold grouped_valid_entries at h
-          -- `exact List.nil_ne_mem_groupBy h`
+          -- `exact List.nil_not_mem_groupBy h`
           -- from mathlib would prove this
           sorry)
           ).fst ++ "\"\n"

From 4c03b24a1138ab1ec57652d958768ec390ada36d Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Wed, 16 Oct 2024 13:50:56 +0200
Subject: [PATCH 10/21] apparently i can't read

---
 Batteries/Util/LibraryNote.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index 37590cb7e8..4944143f42 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -70,7 +70,7 @@ elab "#help note" name:strLit : command => do
     logInfo <| "\n\n".intercalate <|
       valid_entries.map ("/--\n" ++ String.trim · ++ "\n-/")
 
-  -- for when `List.nil_not_mem_groupBy` has landed in batteries or higher in the hierarchy.
+  -- for when `List.ne_nil_of_mem_groupBy` has landed in batteries or higher in the hierarchy.
   /-
   let imported_entries_filtered := imported_entries.flatten.toList.filterMap
     (fun x => if entry_name.isPrefixOf x.fst then some x else Option.none)
@@ -88,7 +88,7 @@ elab "#help note" name:strLit : command => do
       grouped_valid_entries.attach.map (fun ⟨l,h⟩ =>
         "library_note \"" ++ (l.head (by
           unfold grouped_valid_entries at h
-          -- `exact List.nil_not_mem_groupBy h`
+          -- `exact List.ne_nil_of_mem_groupBy h`
           -- from mathlib would prove this
           sorry)
           ).fst ++ "\"\n"

From 319bceb977d6996707f91d2001e254796c07ad2b Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Thu, 17 Oct 2024 14:12:36 +0200
Subject: [PATCH 11/21] use head!, implement prefix search, add tests

---
 Batteries/Test/Internal/DummyLibraryNote.lean |  4 +++
 .../Test/Internal/DummyLibraryNote2.lean      |  9 +++++
 Batteries/Util/LibraryNote.lean               | 35 +++++--------------
 test/library_note.lean                        | 25 +++++++++++--
 4 files changed, 45 insertions(+), 28 deletions(-)

diff --git a/Batteries/Test/Internal/DummyLibraryNote.lean b/Batteries/Test/Internal/DummyLibraryNote.lean
index ff7cf78902..f934823474 100644
--- a/Batteries/Test/Internal/DummyLibraryNote.lean
+++ b/Batteries/Test/Internal/DummyLibraryNote.lean
@@ -8,3 +8,7 @@ The `#help note` command should be able to find this note when imported.
 library_note "test" /--
 2: This is a second testnote for testing the library note feature of batteries.
 -/
+
+library_note "temporary note" /--
+1: This is a testnote whose label also starts with "te", but gets sorted before "test"
+-/
diff --git a/Batteries/Test/Internal/DummyLibraryNote2.lean b/Batteries/Test/Internal/DummyLibraryNote2.lean
index 1dd8f4961f..3a5bc35dc0 100644
--- a/Batteries/Test/Internal/DummyLibraryNote2.lean
+++ b/Batteries/Test/Internal/DummyLibraryNote2.lean
@@ -4,3 +4,12 @@ library_note "test" /--
 3: this is a note in a different file importing the above testnotes,
 but still imported by the actual testfile.
 -/
+
+library_note "Test" /--
+1: this is a testnote with a label starting with "Te"
+-/
+
+library_note "Other" /--
+1: this is a testnote with a label not starting with "te",
+so it shouldn't appear when looking for notes with label starting with "te".
+-/
diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index 4944143f42..7da584f766 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -44,8 +44,9 @@ elab "library_note " title:strLit ppSpace text:docComment : command => do
 
 open Lean Parser in
 /--
-`#help note "some tag"` displays all library notes with tag
-`"some tag"` in the infoview.
+`#help note "foo"` searches (case-insensitively) for all library notes whose
+label starts with "foo", then displays those library notes sorted alphabetically by label,
+grouped (case-sensitively) by label.
 The command only displays the library notes that are declared in
 imported files or in the same file above the line containing the command.
 -/
@@ -57,25 +58,11 @@ elab "#help note" name:strLit : command => do
   let imported_entries := (libraryNoteExt.toEnvExtension.getState env).importedEntries
 
   -- filter for the appropriate notes while casting to list
-  let entry_name := name.getString
-  let imported_entries_filtered := imported_entries.flatten.toList.filterMap
-    (fun x => if x.fst == entry_name then Option.some x.snd else Option.none)
-  let valid_entries := imported_entries_filtered ++ local_entries.filterMap
-    (fun x => if x.fst == entry_name then some x.snd else none)
-
-  -- display results in a readable style
-  if valid_entries.isEmpty then
-    logInfo "Note not found"
-  else
-    logInfo <| "\n\n".intercalate <|
-      valid_entries.map ("/--\n" ++ String.trim · ++ "\n-/")
-
-  -- for when `List.ne_nil_of_mem_groupBy` has landed in batteries or higher in the hierarchy.
-  /-
+  let label_prefix := name.getString.toLower
   let imported_entries_filtered := imported_entries.flatten.toList.filterMap
-    (fun x => if entry_name.isPrefixOf x.fst then some x else Option.none)
+    (fun x => if label_prefix.isPrefixOf x.fst.toLower then some x else none)
   let valid_entries := imported_entries_filtered ++ local_entries.filterMap
-    (fun x => if entry_name.isPrefixOf x.fst then some x else none)
+    (fun x => if label_prefix.isPrefixOf x.fst.toLower then some x else none)
 
   let grouped_valid_entries := valid_entries.mergeSort (·.fst ≤ ·.fst)
     |>.groupBy (·.fst == ·.fst)
@@ -85,12 +72,8 @@ elab "#help note" name:strLit : command => do
     logInfo "Note not found"
   else
     logInfo <| "\n\n".intercalate <|
-      grouped_valid_entries.attach.map (fun ⟨l,h⟩ =>
-        "library_note \"" ++ (l.head (by
-          unfold grouped_valid_entries at h
-          -- `exact List.ne_nil_of_mem_groupBy h`
-          -- from mathlib would prove this
-          sorry)
+      grouped_valid_entries.map (fun l =>
+        "library_note \"" ++ (@List.head! _ ⟨⟨"",""⟩⟩ l
           ).fst ++ "\"\n"
         ++ ("\n\n".intercalate <| l.map (fun e => "/--\n" ++ e.snd.trim ++ "\n-/")))
-  -/
+    -- this could use List.head when List.ne_nil_of_mem_groupBy gets upstreamed from mathlib
diff --git a/test/library_note.lean b/test/library_note.lean
index 34cab0f486..9968967ae6 100644
--- a/test/library_note.lean
+++ b/test/library_note.lean
@@ -7,6 +7,16 @@ info: Note not found
 #guard_msgs in
 #help note "no note"
 
+/--
+info: library_note "Other"
+/--
+1: this is a testnote with a label not starting with "te",
+so it shouldn't appear when looking for notes with label starting with "te".
+-/
+-/
+#guard_msgs in
+#help note "Other"
+
 library_note "test"/--
 4: This note was not imported, and therefore appears below the imported notes.
 -/
@@ -18,7 +28,18 @@ and the previously added note.
 
 
 /--
-info: /--
+info: library_note "Test"
+/--
+1: this is a testnote with a label starting with "Te"
+-/
+
+library_note "temporary note"
+/--
+1: This is a testnote whose label also starts with "te", but gets sorted before "test"
+-/
+
+library_note "test"
+/--
 1: This is a testnote for testing the library note feature of batteries.
 The `#help note` command should be able to find this note when imported.
 -/
@@ -42,4 +63,4 @@ and the previously added note.
 -/
 -/
 #guard_msgs in
-#help note "test"
+#help note "te"

From a5cc8f4104f5e869b9b2f8f268dd1a2651891a48 Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Thu, 17 Oct 2024 15:11:45 +0200
Subject: [PATCH 12/21] add requested style changes

---
 Batteries/Util/LibraryNote.lean | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index 7da584f766..3679cd08f6 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -15,6 +15,7 @@ open Lean
 
 /-- A library note consists of a (short) tag and a (long) note. -/
 def LibraryNoteEntry := String × String
+deriving Inhabited
 
 /-- Environment extension supporting `library_note`. -/
 initialize libraryNoteExt : SimplePersistentEnvExtension LibraryNoteEntry (Array LibraryNoteEntry) ←
@@ -60,10 +61,9 @@ elab "#help note" name:strLit : command => do
   -- filter for the appropriate notes while casting to list
   let label_prefix := name.getString.toLower
   let imported_entries_filtered := imported_entries.flatten.toList.filterMap
-    (fun x => if label_prefix.isPrefixOf x.fst.toLower then some x else none)
+    fun x => if label_prefix.isPrefixOf x.fst.toLower then some x else none
   let valid_entries := imported_entries_filtered ++ local_entries.filterMap
-    (fun x => if label_prefix.isPrefixOf x.fst.toLower then some x else none)
-
+    fun x => if label_prefix.isPrefixOf x.fst.toLower then some x else none
   let grouped_valid_entries := valid_entries.mergeSort (·.fst ≤ ·.fst)
     |>.groupBy (·.fst == ·.fst)
 
@@ -72,8 +72,7 @@ elab "#help note" name:strLit : command => do
     logInfo "Note not found"
   else
     logInfo <| "\n\n".intercalate <|
-      grouped_valid_entries.map (fun l =>
-        "library_note \"" ++ (@List.head! _ ⟨⟨"",""⟩⟩ l
-          ).fst ++ "\"\n"
-        ++ ("\n\n".intercalate <| l.map (fun e => "/--\n" ++ e.snd.trim ++ "\n-/")))
+      grouped_valid_entries.map
+        fun l => "library_note \"" ++ l.head!.fst ++ "\"\n" ++
+          "\n\n".intercalate (l.map fun e => "/--\n" ++ e.snd.trim ++ "\n-/")
     -- this could use List.head when List.ne_nil_of_mem_groupBy gets upstreamed from mathlib

From 4eba128200c282a3c609022aa4f3b59daa2a6faa Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Thu, 17 Oct 2024 16:10:13 +0200
Subject: [PATCH 13/21] remove case-insensitivity

---
 Batteries/Util/LibraryNote.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index 3679cd08f6..31ee5963fc 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -47,7 +47,7 @@ open Lean Parser in
 /--
 `#help note "foo"` searches (case-insensitively) for all library notes whose
 label starts with "foo", then displays those library notes sorted alphabetically by label,
-grouped (case-sensitively) by label.
+grouped by label.
 The command only displays the library notes that are declared in
 imported files or in the same file above the line containing the command.
 -/
@@ -59,11 +59,11 @@ elab "#help note" name:strLit : command => do
   let imported_entries := (libraryNoteExt.toEnvExtension.getState env).importedEntries
 
   -- filter for the appropriate notes while casting to list
-  let label_prefix := name.getString.toLower
+  let label_prefix := name.getString
   let imported_entries_filtered := imported_entries.flatten.toList.filterMap
-    fun x => if label_prefix.isPrefixOf x.fst.toLower then some x else none
+    fun x => if label_prefix.isPrefixOf x.fst then some x else none
   let valid_entries := imported_entries_filtered ++ local_entries.filterMap
-    fun x => if label_prefix.isPrefixOf x.fst.toLower then some x else none
+    fun x => if label_prefix.isPrefixOf x.fst then some x else none
   let grouped_valid_entries := valid_entries.mergeSort (·.fst ≤ ·.fst)
     |>.groupBy (·.fst == ·.fst)
 

From 6f134b5a47059aaeb624da642da1616b0038d310 Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Thu, 17 Oct 2024 16:38:50 +0200
Subject: [PATCH 14/21] change displayed delimiter

---
 Batteries/Util/LibraryNote.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index 31ee5963fc..5a47e7f678 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -74,5 +74,5 @@ elab "#help note" name:strLit : command => do
     logInfo <| "\n\n".intercalate <|
       grouped_valid_entries.map
         fun l => "library_note \"" ++ l.head!.fst ++ "\"\n" ++
-          "\n\n".intercalate (l.map fun e => "/--\n" ++ e.snd.trim ++ "\n-/")
+          "\n\n".intercalate (l.map fun e => "/-\n" ++ e.snd.trim ++ "\n-/")
     -- this could use List.head when List.ne_nil_of_mem_groupBy gets upstreamed from mathlib

From 273078f6dfbe43bf2ddd2d307bc76a64be836fc0 Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Fri, 18 Oct 2024 21:38:17 +0200
Subject: [PATCH 15/21] fix test (for now)

---
 test/library_note.lean | 21 ++++++++-------------
 1 file changed, 8 insertions(+), 13 deletions(-)

diff --git a/test/library_note.lean b/test/library_note.lean
index 9968967ae6..235b48ab14 100644
--- a/test/library_note.lean
+++ b/test/library_note.lean
@@ -9,7 +9,7 @@ info: Note not found
 
 /--
 info: library_note "Other"
-/--
+/-
 1: this is a testnote with a label not starting with "te",
 so it shouldn't appear when looking for notes with label starting with "te".
 -/
@@ -28,36 +28,31 @@ and the previously added note.
 
 
 /--
-info: library_note "Test"
-/--
-1: this is a testnote with a label starting with "Te"
--/
-
-library_note "temporary note"
-/--
+info: library_note "temporary note"
+/-
 1: This is a testnote whose label also starts with "te", but gets sorted before "test"
 -/
 
 library_note "test"
-/--
+/-
 1: This is a testnote for testing the library note feature of batteries.
 The `#help note` command should be able to find this note when imported.
 -/
 
-/--
+/-
 2: This is a second testnote for testing the library note feature of batteries.
 -/
 
-/--
+/-
 3: this is a note in a different file importing the above testnotes,
 but still imported by the actual testfile.
 -/
 
-/--
+/-
 4: This note was not imported, and therefore appears below the imported notes.
 -/
 
-/--
+/-
 5: This note was also not imported, and therefore appears below the imported notes,
 and the previously added note.
 -/

From 375c2f5661edb75e05a10188d68cc8464f2bbd3b Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Sat, 26 Oct 2024 13:06:39 +0200
Subject: [PATCH 16/21] use markdown style formatting. not rendering... yet.

---
 Batteries/Util/LibraryNote.lean |  8 +++++--
 test/library_note.lean          | 38 +++++++++++----------------------
 2 files changed, 18 insertions(+), 28 deletions(-)

diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index 5a47e7f678..d3a61f365e 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -42,6 +42,10 @@ Use `#help note "some tag"` to display all notes with the tag
 elab "library_note " title:strLit ppSpace text:docComment : command => do
   modifyEnv (libraryNoteExt.addEntry · (title.getString, text.getDocString))
 
+/--
+format the string to be included in a single markdown bullet
+-/
+def _root_.String.makeBullet (s:String) := "* " ++ ("\n  ").intercalate (s.splitOn "\n")
 
 open Lean Parser in
 /--
@@ -69,10 +73,10 @@ elab "#help note" name:strLit : command => do
 
   -- display results in a readable style
   if grouped_valid_entries.isEmpty then
-    logInfo "Note not found"
+    logError "Note not found"
   else
     logInfo <| "\n\n".intercalate <|
       grouped_valid_entries.map
         fun l => "library_note \"" ++ l.head!.fst ++ "\"\n" ++
-          "\n\n".intercalate (l.map fun e => "/-\n" ++ e.snd.trim ++ "\n-/")
+          "\n\n".intercalate (l.map (·.snd.trim.makeBullet))
     -- this could use List.head when List.ne_nil_of_mem_groupBy gets upstreamed from mathlib
diff --git a/test/library_note.lean b/test/library_note.lean
index 235b48ab14..ba9fe90414 100644
--- a/test/library_note.lean
+++ b/test/library_note.lean
@@ -2,17 +2,15 @@ import Batteries.Util.LibraryNote
 import Batteries.Test.Internal.DummyLibraryNote2
 
 /--
-info: Note not found
+error: Note not found
 -/
 #guard_msgs in
 #help note "no note"
 
 /--
 info: library_note "Other"
-/-
-1: this is a testnote with a label not starting with "te",
-so it shouldn't appear when looking for notes with label starting with "te".
--/
+* 1: this is a testnote with a label not starting with "te",
+  so it shouldn't appear when looking for notes with label starting with "te".
 -/
 #guard_msgs in
 #help note "Other"
@@ -29,33 +27,21 @@ and the previously added note.
 
 /--
 info: library_note "temporary note"
-/-
-1: This is a testnote whose label also starts with "te", but gets sorted before "test"
--/
+* 1: This is a testnote whose label also starts with "te", but gets sorted before "test"
 
 library_note "test"
-/-
-1: This is a testnote for testing the library note feature of batteries.
-The `#help note` command should be able to find this note when imported.
--/
+* 1: This is a testnote for testing the library note feature of batteries.
+  The `#help note` command should be able to find this note when imported.
 
-/-
-2: This is a second testnote for testing the library note feature of batteries.
--/
+* 2: This is a second testnote for testing the library note feature of batteries.
 
-/-
-3: this is a note in a different file importing the above testnotes,
-but still imported by the actual testfile.
--/
+* 3: this is a note in a different file importing the above testnotes,
+  but still imported by the actual testfile.
 
-/-
-4: This note was not imported, and therefore appears below the imported notes.
--/
+* 4: This note was not imported, and therefore appears below the imported notes.
 
-/-
-5: This note was also not imported, and therefore appears below the imported notes,
-and the previously added note.
--/
+* 5: This note was also not imported, and therefore appears below the imported notes,
+  and the previously added note.
 -/
 #guard_msgs in
 #help note "te"

From 1169c02982e5b31d8efb873f2466720235deea79 Mon Sep 17 00:00:00 2001
From: blizzard_inc <edegeltje@gmail.com>
Date: Sat, 26 Oct 2024 16:45:19 +0200
Subject: [PATCH 17/21] add requested suggestion
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: François G. Dorais <fgdorais@gmail.com>
---
 Batteries/Util/LibraryNote.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index d3a61f365e..2daa13c611 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -55,7 +55,7 @@ grouped by label.
 The command only displays the library notes that are declared in
 imported files or in the same file above the line containing the command.
 -/
-elab "#help note" name:strLit : command => do
+elab "#help " colGt &"note" colGt ppSpace name:strLit : command => do
   let env ← getEnv
 
   -- get the library notes from both this and imported files

From 4f0a07aeb69636ba867b708f1b63703588dc12ff Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Sat, 26 Oct 2024 18:40:30 +0200
Subject: [PATCH 18/21] update module doc for helpcmd

---
 Batteries/Tactic/HelpCmd.lean | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/Batteries/Tactic/HelpCmd.lean b/Batteries/Tactic/HelpCmd.lean
index cf1c0f2646..a2ed5ae71e 100644
--- a/Batteries/Tactic/HelpCmd.lean
+++ b/Batteries/Tactic/HelpCmd.lean
@@ -16,15 +16,20 @@ The `#help` command can be used to list all definitions in a variety of extensib
 * `#help attr` lists attributes (used in `@[myAttr] def foo := ...`)
 * `#help cats` lists syntax categories (like `term`, `tactic`, `stx` etc)
 * `#help cat C` lists elements of syntax category C
+* `#help note "some note"` lists library notes for which "some note" is a prefix of the label
   * `#help term`, `#help tactic`, `#help conv`, `#help command`
     are shorthand for `#help cat term` etc.
   * `#help cat+ C` also shows `elab` and `macro` definitions associated to the syntaxes
 
-All forms take an optional identifier to narrow the search; for example `#help option pp` shows
-only `pp.*` options.
+Most forms take an optional identifier to narrow the search; for example `#help option pp` shows
+only `pp.*` options. However, `#help cat` makes the identifier mandatory, while `#help note` takes
+a mandatory string literal, rather than an identifier.
 
 -/
 
+-- The `#help note` command is defined in a different file,
+-- to make sure it is available wherever there are library notes.
+
 namespace Batteries.Tactic
 open Lean Meta Elab Tactic Command
 

From 2c1b9f118df5f01dcf5735ff3d872e7be8b3eabd Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Sun, 27 Oct 2024 17:10:30 +0100
Subject: [PATCH 19/21] move the command

---
 Batteries/Tactic/HelpCmd.lean   | 44 ++++++++++++++++++++++++++++++--
 Batteries/Util/LibraryNote.lean | 45 +++------------------------------
 test/library_note.lean          |  2 +-
 3 files changed, 46 insertions(+), 45 deletions(-)

diff --git a/Batteries/Tactic/HelpCmd.lean b/Batteries/Tactic/HelpCmd.lean
index a2ed5ae71e..b923c14407 100644
--- a/Batteries/Tactic/HelpCmd.lean
+++ b/Batteries/Tactic/HelpCmd.lean
@@ -1,10 +1,11 @@
 /-
-Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Copyright (c) 2024 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
+Authors: Mario Carneiro, Edward van de Meent
 -/
 import Lean.Elab.Syntax
 import Lean.DocString
+import Batteries.Util.LibraryNote
 
 /-!
 
@@ -281,6 +282,45 @@ elab_rules : command
   | `(#help cat $[+%$more]? $cat $id:ident) => elabHelpCat more cat (id.getId.toString false)
   | `(#help cat $[+%$more]? $cat $id:str) => elabHelpCat more cat id.getString
 
+/--
+format the string to be included in a single markdown bullet
+-/
+def _root_.String.makeBullet (s:String) := "* " ++ ("\n  ").intercalate (s.splitOn "\n")
+
+open Lean Parser Batteries.Util.LibraryNote in
+/--
+`#help note "foo"` searches (case-insensitively) for all library notes whose
+label starts with "foo", then displays those library notes sorted alphabetically by label,
+grouped by label.
+The command only displays the library notes that are declared in
+imported files or in the same file above the line containing the command.
+-/
+elab "#help " colGt &"note" colGt ppSpace name:strLit : command => do
+  let env ← getEnv
+
+  -- get the library notes from both this and imported files
+  let local_entries := (libraryNoteExt.getEntries env).reverse
+  let imported_entries := (libraryNoteExt.toEnvExtension.getState env).importedEntries
+
+  -- filter for the appropriate notes while casting to list
+  let label_prefix := name.getString
+  let imported_entries_filtered := imported_entries.flatten.toList.filterMap
+    fun x => if label_prefix.isPrefixOf x.fst then some x else none
+  let valid_entries := imported_entries_filtered ++ local_entries.filterMap
+    fun x => if label_prefix.isPrefixOf x.fst then some x else none
+  let grouped_valid_entries := valid_entries.mergeSort (·.fst ≤ ·.fst)
+    |>.groupBy (·.fst == ·.fst)
+
+  -- display results in a readable style
+  if grouped_valid_entries.isEmpty then
+    logError "Note not found"
+  else
+    logInfo <| "\n\n".intercalate <|
+      grouped_valid_entries.map
+        fun l => "library_note \"" ++ l.head!.fst ++ "\"\n" ++
+          "\n\n".intercalate (l.map (·.snd.trim.makeBullet))
+    -- this could use List.head when List.ne_nil_of_mem_groupBy gets upstreamed from mathlib
+
 /--
 The command `#help term` shows all term syntaxes that have been defined in the current environment.
 See `#help cat` for more information.
diff --git a/Batteries/Util/LibraryNote.lean b/Batteries/Util/LibraryNote.lean
index 2daa13c611..3d578c342b 100644
--- a/Batteries/Util/LibraryNote.lean
+++ b/Batteries/Util/LibraryNote.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Gabriel Ebner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Edward van de Meent
+Authors: Gabriel Ebner
 -/
 import Lean.Elab.Command
 
@@ -36,47 +36,8 @@ creates a new "library note", which can then be cross-referenced using
 -- See note [some tag]
 ```
 in doc-comments.
-Use `#help note "some tag"` to display all notes with the tag
-`"some tag"` in the infoview.
+Use `#help note "some tag"` to display all notes with the tag `"some tag"` in the infoview.
+This command can be imported from Batteries.Tactic.HelpCmd .
 -/
 elab "library_note " title:strLit ppSpace text:docComment : command => do
   modifyEnv (libraryNoteExt.addEntry · (title.getString, text.getDocString))
-
-/--
-format the string to be included in a single markdown bullet
--/
-def _root_.String.makeBullet (s:String) := "* " ++ ("\n  ").intercalate (s.splitOn "\n")
-
-open Lean Parser in
-/--
-`#help note "foo"` searches (case-insensitively) for all library notes whose
-label starts with "foo", then displays those library notes sorted alphabetically by label,
-grouped by label.
-The command only displays the library notes that are declared in
-imported files or in the same file above the line containing the command.
--/
-elab "#help " colGt &"note" colGt ppSpace name:strLit : command => do
-  let env ← getEnv
-
-  -- get the library notes from both this and imported files
-  let local_entries := (libraryNoteExt.getEntries env).reverse
-  let imported_entries := (libraryNoteExt.toEnvExtension.getState env).importedEntries
-
-  -- filter for the appropriate notes while casting to list
-  let label_prefix := name.getString
-  let imported_entries_filtered := imported_entries.flatten.toList.filterMap
-    fun x => if label_prefix.isPrefixOf x.fst then some x else none
-  let valid_entries := imported_entries_filtered ++ local_entries.filterMap
-    fun x => if label_prefix.isPrefixOf x.fst then some x else none
-  let grouped_valid_entries := valid_entries.mergeSort (·.fst ≤ ·.fst)
-    |>.groupBy (·.fst == ·.fst)
-
-  -- display results in a readable style
-  if grouped_valid_entries.isEmpty then
-    logError "Note not found"
-  else
-    logInfo <| "\n\n".intercalate <|
-      grouped_valid_entries.map
-        fun l => "library_note \"" ++ l.head!.fst ++ "\"\n" ++
-          "\n\n".intercalate (l.map (·.snd.trim.makeBullet))
-    -- this could use List.head when List.ne_nil_of_mem_groupBy gets upstreamed from mathlib
diff --git a/test/library_note.lean b/test/library_note.lean
index ba9fe90414..f7ac514cdc 100644
--- a/test/library_note.lean
+++ b/test/library_note.lean
@@ -1,4 +1,4 @@
-import Batteries.Util.LibraryNote
+import Batteries.Tactic.HelpCmd
 import Batteries.Test.Internal.DummyLibraryNote2
 
 /--

From afde65fce64953e1a55a4565fedb38c84e27af0b Mon Sep 17 00:00:00 2001
From: Blizzard_inc <thrashy4inbox@gmail.com>
Date: Sun, 27 Oct 2024 17:49:21 +0100
Subject: [PATCH 20/21] remove comment

---
 Batteries/Tactic/HelpCmd.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/Batteries/Tactic/HelpCmd.lean b/Batteries/Tactic/HelpCmd.lean
index b923c14407..56a509d7f4 100644
--- a/Batteries/Tactic/HelpCmd.lean
+++ b/Batteries/Tactic/HelpCmd.lean
@@ -28,9 +28,6 @@ a mandatory string literal, rather than an identifier.
 
 -/
 
--- The `#help note` command is defined in a different file,
--- to make sure it is available wherever there are library notes.
-
 namespace Batteries.Tactic
 open Lean Meta Elab Tactic Command
 

From d1fff4b9887edf316593ddf7e46ba749dbe9181b Mon Sep 17 00:00:00 2001
From: blizzard_inc <edegeltje@gmail.com>
Date: Sun, 27 Oct 2024 19:10:35 +0100
Subject: [PATCH 21/21] Apply suggestions from code review
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: François G. Dorais <fgdorais@gmail.com>
---
 Batteries/Tactic/HelpCmd.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Batteries/Tactic/HelpCmd.lean b/Batteries/Tactic/HelpCmd.lean
index 56a509d7f4..7fbe67bf3a 100644
--- a/Batteries/Tactic/HelpCmd.lean
+++ b/Batteries/Tactic/HelpCmd.lean
@@ -17,10 +17,10 @@ The `#help` command can be used to list all definitions in a variety of extensib
 * `#help attr` lists attributes (used in `@[myAttr] def foo := ...`)
 * `#help cats` lists syntax categories (like `term`, `tactic`, `stx` etc)
 * `#help cat C` lists elements of syntax category C
-* `#help note "some note"` lists library notes for which "some note" is a prefix of the label
   * `#help term`, `#help tactic`, `#help conv`, `#help command`
     are shorthand for `#help cat term` etc.
   * `#help cat+ C` also shows `elab` and `macro` definitions associated to the syntaxes
+* `#help note "some note"` lists library notes for which "some note" is a prefix of the label
 
 Most forms take an optional identifier to narrow the search; for example `#help option pp` shows
 only `pp.*` options. However, `#help cat` makes the identifier mandatory, while `#help note` takes
@@ -286,7 +286,7 @@ def _root_.String.makeBullet (s:String) := "* " ++ ("\n  ").intercalate (s.split
 
 open Lean Parser Batteries.Util.LibraryNote in
 /--
-`#help note "foo"` searches (case-insensitively) for all library notes whose
+`#help note "foo"` searches for all library notes whose
 label starts with "foo", then displays those library notes sorted alphabetically by label,
 grouped by label.
 The command only displays the library notes that are declared in
@@ -316,7 +316,6 @@ elab "#help " colGt &"note" colGt ppSpace name:strLit : command => do
       grouped_valid_entries.map
         fun l => "library_note \"" ++ l.head!.fst ++ "\"\n" ++
           "\n\n".intercalate (l.map (·.snd.trim.makeBullet))
-    -- this could use List.head when List.ne_nil_of_mem_groupBy gets upstreamed from mathlib
 
 /--
 The command `#help term` shows all term syntaxes that have been defined in the current environment.