chore: rename manifold delaborators to match the naming convention (#39821)

Change from delab_foo to delabFoo (as these are Type-valued, not Prop-valued, so should be lowerCamelCase by naming rule 4).
And ensure to namespace all delaborators under manifold.

This should not need deprecations, as presumably these delaborators are never called directly.

Author: grunweg

Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

@@ -431,7 +431,7 @@ open Bundle PrettyPrinter Delaborator SubExpr
 -- There is no need to special-case any arguments which could use the T% s elaborator:
 -- the argument to `mvfderiv` is a vector-valued function, which a map to a total space
 -- can never be.
-@[app_delab mvfderiv] meta def delab_mvfderiv : Delab := do
+@[app_delab mvfderiv] meta def delabMVFDeriv : Delab := do
   whenPPOption getPPNotation do
   withOverApp 15 do
   let fs ← withAppArg delab

Mathlib/Geometry/Manifold/Notation.lean

@@ -973,26 +973,28 @@ initialize registerTraceClass `Elab.DiffGeo.MDiff (inherited := true)
 
 end trace
 
-section delaborators
-
 /-!
 ### Delaborators
 
-In this section we make sure the infoview also uses those notations.
-Not all notations are supported yet.
+In this section we make sure the infoview also uses the above notation.
+Not all elaborators are supported yet.
 -/
+section delaborators
+
+namespace Manifold
+
 open Bundle PrettyPrinter Delaborator SubExpr
 
 /-- Delaborator for `Bundle.TotalSpace.mk` using anonymous constructor notation. -/
-@[app_delab TotalSpace.mk] meta def delabTotalSpace_mk : Delab := do
+@[app_delab TotalSpace.mk] meta def delabTotalSpaceMk : Delab := do
   whenPPOption getPPNotation do
   withOverApp 5 do
   let bd ← withNaryArg 3 <| delab
   let vd ← withNaryArg 4 <| delab
   `(⟨$bd, $vd⟩)
 
 /-- Delaborator for `Bundle.TotalSpace.mk'` using anonymous constructor notation. -/
-@[app_delab Bundle.TotalSpace.mk'] meta def delabTotalSpace_mk' : Delab := do
+@[app_delab Bundle.TotalSpace.mk'] meta def delabTotalSpaceMkPrime : Delab := do
   whenPPOption getPPNotation do
   withOverApp 5 do
   let bd ← withNaryArg 3 <| delab
@@ -1001,7 +1003,7 @@ open Bundle PrettyPrinter Delaborator SubExpr
 
 /-- Delaborator for `mfderiv` using the custom elaborator, and special-casing
 arguments that can use the `T%` elaborator. -/
-@[app_delab mfderiv] meta def delab_mfderiv : Delab := do
+@[app_delab mfderiv] meta def delabMFDeriv : Delab := do
   whenPPOption getPPNotation do
   withOverApp 21 do
   try
@@ -1103,4 +1105,6 @@ arguments that can use the `T%` elaborator. -/
 
 -- TODO: when adding more elaborators, also add the corresponding delaborators
 
+end Manifold
+
 end delaborators

scripts/nolints.json

@@ -4,9 +4,6 @@
  ["defsWithUnderscore", "cfcₙHom_of_cfcHom"],
  ["defsWithUnderscore", "commandSuppress_compilation"],
  ["defsWithUnderscore", "decidableEq_of_subsingleton"],
- ["defsWithUnderscore", "delabTotalSpace_mk"],
- ["defsWithUnderscore", "delabTotalSpace_mk'"],
- ["defsWithUnderscore", "delab_mfderiv"],
  ["defsWithUnderscore", "delab_not_in"],
  ["defsWithUnderscore", "equiv_linearIndependent"],
  ["defsWithUnderscore", "exists_delab"],
@@ -186,7 +183,6 @@
  ["defsWithUnderscore", "List.lex_chains"],
  ["defsWithUnderscore", "List.maximum_of_length_pos"],
  ["defsWithUnderscore", "List.minimum_of_length_pos"],
- ["defsWithUnderscore", "Manifold.delab_mvfderiv"],
  ["defsWithUnderscore", "Matrix.cons_val"],
  ["defsWithUnderscore", "Matrix.equiv_GL_linearindependent"],
  ["defsWithUnderscore", "Matroid.aesop_mat"],