From aa726920887e2e051a305016c8c6ca2ed50417bb Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 28 Dec 2024 03:20:00 +0000
Subject: [PATCH] chore: use `app_delab` (#20249)

This has the same behavior as `delab app.`, but protects against typos.

The feature appeared in https://github.com/leanprover/lean4/pull/4976, though won't be documented until https://github.com/leanprover/lean4/pull/6450.
---
 Mathlib/Algebra/BigOperators/Expect.lean            | 2 +-
 Mathlib/Algebra/BigOperators/Group/Finset.lean      | 4 ++--
 Mathlib/Analysis/InnerProductSpace/PiL2.lean        | 2 +-
 Mathlib/CategoryTheory/Closed/Cartesian.lean        | 2 +-
 Mathlib/CategoryTheory/Monoidal/Category.lean       | 2 +-
 Mathlib/Data/Matrix/Notation.lean                   | 2 +-
 Mathlib/Data/Prod/Basic.lean                        | 4 ++--
 Mathlib/Data/SetLike/Basic.lean                     | 2 +-
 Mathlib/FieldTheory/Adjoin.lean                     | 2 +-
 Mathlib/LinearAlgebra/LinearIndependent.lean        | 2 +-
 Mathlib/LinearAlgebra/Matrix/PosDef.lean            | 2 +-
 Mathlib/Order/SetNotation.lean                      | 8 ++++----
 Mathlib/RingTheory/Derivation/DifferentialRing.lean | 2 +-
 Mathlib/Util/Delaborators.lean                      | 4 ++--
 14 files changed, 20 insertions(+), 20 deletions(-)

diff --git a/Mathlib/Algebra/BigOperators/Expect.lean b/Mathlib/Algebra/BigOperators/Expect.lean
index df5560dfae390..10df5c9c7e7b3 100644
--- a/Mathlib/Algebra/BigOperators/Expect.lean
+++ b/Mathlib/Algebra/BigOperators/Expect.lean
@@ -85,7 +85,7 @@ open Batteries.ExtendedBinder
 
 /-- Delaborator for `Finset.expect`. The `pp.piBinderTypes` option controls whether
 to show the domain type when the expect is over `Finset.univ`. -/
-@[scoped delab app.Finset.expect] def delabFinsetExpect : Delab :=
+@[scoped app_delab Finset.expect] def delabFinsetExpect : Delab :=
   whenPPOption getPPNotation <| withOverApp 6 <| do
   let #[_, _, _, _, s, f] := (← getExpr).getAppArgs | failure
   guard <| f.isLambda
diff --git a/Mathlib/Algebra/BigOperators/Group/Finset.lean b/Mathlib/Algebra/BigOperators/Group/Finset.lean
index d8de2d605f7b1..47e77cc8c7ce4 100644
--- a/Mathlib/Algebra/BigOperators/Group/Finset.lean
+++ b/Mathlib/Algebra/BigOperators/Group/Finset.lean
@@ -218,7 +218,7 @@ open scoped Batteries.ExtendedBinder
 
 /-- Delaborator for `Finset.prod`. The `pp.piBinderTypes` option controls whether
 to show the domain type when the product is over `Finset.univ`. -/
-@[delab app.Finset.prod] def delabFinsetProd : Delab :=
+@[app_delab Finset.prod] def delabFinsetProd : Delab :=
   whenPPOption getPPNotation <| withOverApp 5 <| do
   let #[_, _, _, s, f] := (← getExpr).getAppArgs | failure
   guard <| f.isLambda
@@ -239,7 +239,7 @@ to show the domain type when the product is over `Finset.univ`. -/
 
 /-- Delaborator for `Finset.sum`. The `pp.piBinderTypes` option controls whether
 to show the domain type when the sum is over `Finset.univ`. -/
-@[delab app.Finset.sum] def delabFinsetSum : Delab :=
+@[app_delab Finset.sum] def delabFinsetSum : Delab :=
   whenPPOption getPPNotation <| withOverApp 5 <| do
   let #[_, _, _, s, f] := (← getExpr).getAppArgs | failure
   guard <| f.isLambda
diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
index 2f76e57c56c2e..e45fd08b5881d 100644
--- a/Mathlib/Analysis/InnerProductSpace/PiL2.lean
+++ b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
@@ -119,7 +119,7 @@ macro_rules | `(!$p:subscript[$e:term,*]) => do
 
 set_option trace.debug true in
 /-- Unexpander for the `!₂[x, y, ...]` notation. -/
-@[delab app.DFunLike.coe]
+@[app_delab DFunLike.coe]
 def EuclideanSpace.delabVecNotation : Delab :=
   whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 6 do
     -- check that the `(WithLp.equiv _ _).symm` is present
diff --git a/Mathlib/CategoryTheory/Closed/Cartesian.lean b/Mathlib/CategoryTheory/Closed/Cartesian.lean
index 0607788f02110..c79932f744135 100644
--- a/Mathlib/CategoryTheory/Closed/Cartesian.lean
+++ b/Mathlib/CategoryTheory/Closed/Cartesian.lean
@@ -117,7 +117,7 @@ notation:20 A " ⟹ " B:19 => (exp A).obj B
 
 open Lean PrettyPrinter.Delaborator SubExpr in
 /-- Delaborator for `Prefunctor.obj` -/
-@[delab app.Prefunctor.obj]
+@[app_delab Prefunctor.obj]
 def delabPrefunctorObjExp : Delab := whenPPOption getPPNotation <| withOverApp 6 <| do
   let e ← getExpr
   guard <| e.isAppOfArity' ``Prefunctor.obj 6
diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean
index 59c3f0eca4f26..a0d928049644b 100644
--- a/Mathlib/CategoryTheory/Monoidal/Category.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Category.lean
@@ -124,7 +124,7 @@ scoped notation "𝟙_ " C:max => (MonoidalCategoryStruct.tensorUnit : C)
 
 open Lean PrettyPrinter.Delaborator SubExpr in
 /-- Used to ensure that `𝟙_` notation is used, as the ascription makes this not automatic. -/
-@[delab app.CategoryTheory.MonoidalCategoryStruct.tensorUnit]
+@[app_delab CategoryTheory.MonoidalCategoryStruct.tensorUnit]
 def delabTensorUnit : Delab := whenPPOption getPPNotation <| withOverApp 3 do
   let e ← getExpr
   guard <| e.isAppOfArity ``MonoidalCategoryStruct.tensorUnit 3
diff --git a/Mathlib/Data/Matrix/Notation.lean b/Mathlib/Data/Matrix/Notation.lean
index 26667c8ae47fb..66a14eeaec9ed 100644
--- a/Mathlib/Data/Matrix/Notation.lean
+++ b/Mathlib/Data/Matrix/Notation.lean
@@ -111,7 +111,7 @@ macro_rules
   | `(!![$[,%$commas]*]) => `(@Matrix.of (Fin 0) (Fin $(quote commas.size)) _ ![])
 
 /-- Delaborator for the `!![]` notation. -/
-@[delab app.DFunLike.coe]
+@[app_delab DFunLike.coe]
 def delabMatrixNotation : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <|
   withOverApp 6 do
     let mkApp3 (.const ``Matrix.of _) (.app (.const ``Fin _) em) (.app (.const ``Fin _) en) _ :=
diff --git a/Mathlib/Data/Prod/Basic.lean b/Mathlib/Data/Prod/Basic.lean
index 98f729aaec3e6..7df6836ea3cac 100644
--- a/Mathlib/Data/Prod/Basic.lean
+++ b/Mathlib/Data/Prod/Basic.lean
@@ -304,13 +304,13 @@ section delaborators
 open Lean PrettyPrinter Delaborator
 
 /-- Delaborator for `Prod.fst x` as `x.1`. -/
-@[delab app.Prod.fst]
+@[app_delab Prod.fst]
 def delabProdFst : Delab := withOverApp 3 do
   let x ← SubExpr.withAppArg delab
   `($(x).1)
 
 /-- Delaborator for `Prod.snd x` as `x.2`. -/
-@[delab app.Prod.snd]
+@[app_delab Prod.snd]
 def delabProdSnd : Delab := withOverApp 3 do
   let x ← SubExpr.withAppArg delab
   `($(x).2)
diff --git a/Mathlib/Data/SetLike/Basic.lean b/Mathlib/Data/SetLike/Basic.lean
index 1e120903e60ff..fb74683ca034a 100644
--- a/Mathlib/Data/SetLike/Basic.lean
+++ b/Mathlib/Data/SetLike/Basic.lean
@@ -117,7 +117,7 @@ open Lean PrettyPrinter.Delaborator SubExpr
 /-- For terms that match the `CoeSort` instance's body, pretty print as `↥S`
 rather than as `{ x // x ∈ S }`. The discriminating feature is that membership
 uses the `SetLike.instMembership` instance. -/
-@[delab app.Subtype]
+@[app_delab Subtype]
 def delabSubtypeSetLike : Delab := whenPPOption getPPNotation do
   let #[_, .lam n _ body _] := (← getExpr).getAppArgs | failure
   guard <| body.isAppOf ``Membership.mem
diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean
index 464f52592988b..6c85ffedec641 100644
--- a/Mathlib/FieldTheory/Adjoin.lean
+++ b/Mathlib/FieldTheory/Adjoin.lean
@@ -600,7 +600,7 @@ generated by these elements. -/
 scoped macro:max K:term "⟮" xs:term,* "⟯" : term => do ``(adjoin $K $(← mkInsertTerm xs.getElems))
 
 open Lean PrettyPrinter.Delaborator SubExpr in
-@[delab app.IntermediateField.adjoin]
+@[app_delab IntermediateField.adjoin]
 partial def delabAdjoinNotation : Delab := whenPPOption getPPNotation do
   let e ← getExpr
   guard <| e.isAppOfArity ``adjoin 6
diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean
index 071d3990c70ae..aa5849bf7df41 100644
--- a/Mathlib/LinearAlgebra/LinearIndependent.lean
+++ b/Mathlib/LinearAlgebra/LinearIndependent.lean
@@ -109,7 +109,7 @@ in case the family of vectors is over a `Set`.
 
 Type hints look like `LinearIndependent fun (v : ↑s) => ↑v` or `LinearIndependent (ι := ↑s) f`,
 depending on whether the family is a lambda expression or not. -/
-@[delab app.LinearIndependent]
+@[app_delab LinearIndependent]
 def delabLinearIndependent : Delab :=
   whenPPOption getPPNotation <|
   whenNotPPOption getPPAnalysisSkip <|
diff --git a/Mathlib/LinearAlgebra/Matrix/PosDef.lean b/Mathlib/LinearAlgebra/Matrix/PosDef.lean
index 73d3c0be13503..fb373744d8173 100644
--- a/Mathlib/LinearAlgebra/Matrix/PosDef.lean
+++ b/Mathlib/LinearAlgebra/Matrix/PosDef.lean
@@ -172,7 +172,7 @@ noncomputable def sqrt : Matrix n n 𝕜 :=
 
 open Lean PrettyPrinter.Delaborator SubExpr in
 /-- Custom elaborator to produce output like `(_ : PosSemidef A).sqrt` in the goal view. -/
-@[delab app.Matrix.PosSemidef.sqrt]
+@[app_delab Matrix.PosSemidef.sqrt]
 def delabSqrt : Delab :=
   whenPPOption getPPNotation <|
   whenNotPPOption getPPAnalysisSkip <|
diff --git a/Mathlib/Order/SetNotation.lean b/Mathlib/Order/SetNotation.lean
index 7feb44d478558..fb19f19f22d55 100644
--- a/Mathlib/Order/SetNotation.lean
+++ b/Mathlib/Order/SetNotation.lean
@@ -88,7 +88,7 @@ section delaborators
 open Lean Lean.PrettyPrinter.Delaborator
 
 /-- Delaborator for indexed supremum. -/
-@[delab app.iSup]
+@[app_delab iSup]
 def iSup_delab : Delab := whenPPOption Lean.getPPNotation <| withOverApp 4 do
   let #[_, ι, _, f] := (← SubExpr.getExpr).getAppArgs | failure
   unless f.isLambda do failure
@@ -116,7 +116,7 @@ def iSup_delab : Delab := whenPPOption Lean.getPPNotation <| withOverApp 4 do
   return stx
 
 /-- Delaborator for indexed infimum. -/
-@[delab app.iInf]
+@[app_delab iInf]
 def iInf_delab : Delab := whenPPOption Lean.getPPNotation <| withOverApp 4 do
   let #[_, ι, _, f] := (← SubExpr.getExpr).getAppArgs | failure
   unless f.isLambda do failure
@@ -193,7 +193,7 @@ section delaborators
 open Lean Lean.PrettyPrinter.Delaborator
 
 /-- Delaborator for indexed unions. -/
-@[delab app.Set.iUnion]
+@[app_delab Set.iUnion]
 def iUnion_delab : Delab := whenPPOption Lean.getPPNotation do
   let #[_, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
   unless f.isLambda do failure
@@ -221,7 +221,7 @@ def iUnion_delab : Delab := whenPPOption Lean.getPPNotation do
   return stx
 
 /-- Delaborator for indexed intersections. -/
-@[delab app.Set.iInter]
+@[app_delab Set.iInter]
 def sInter_delab : Delab := whenPPOption Lean.getPPNotation do
   let #[_, ι, f] := (← SubExpr.getExpr).getAppArgs | failure
   unless f.isLambda do failure
diff --git a/Mathlib/RingTheory/Derivation/DifferentialRing.lean b/Mathlib/RingTheory/Derivation/DifferentialRing.lean
index f26d5aab07492..a0d6e22ba7f17 100644
--- a/Mathlib/RingTheory/Derivation/DifferentialRing.lean
+++ b/Mathlib/RingTheory/Derivation/DifferentialRing.lean
@@ -27,7 +27,7 @@ open Lean PrettyPrinter Delaborator SubExpr in
 A delaborator for the x′ notation. This is required because it's not direct function application,
 so the default delaborator doesn't work.
 -/
-@[delab app.DFunLike.coe]
+@[app_delab DFunLike.coe]
 def delabDeriv : Delab := do
   let e ← getExpr
   guard <| e.isAppOfArity' ``DFunLike.coe 6
diff --git a/Mathlib/Util/Delaborators.lean b/Mathlib/Util/Delaborators.lean
index b45007dc4e2af..e091a084b2c56 100644
--- a/Mathlib/Util/Delaborators.lean
+++ b/Mathlib/Util/Delaborators.lean
@@ -97,7 +97,7 @@ open Lean Parser Term PrettyPrinter Delaborator
 
 /-- Delaborator for existential quantifier, including extended binders. -/
 -- TODO: reduce the duplication in this code
-@[delab app.Exists]
+@[app_delab Exists]
 def exists_delab : Delab := whenPPOption Lean.getPPNotation do
   let #[ι, f] := (← SubExpr.getExpr).getAppArgs | failure
   unless f.isLambda do failure
@@ -159,7 +159,7 @@ end existential
 open Lean Lean.PrettyPrinter.Delaborator
 
 /-- Delaborator for `∉`. -/
-@[delab app.Not] def delab_not_in := whenPPOption Lean.getPPNotation do
+@[app_delab Not] def delab_not_in := whenPPOption Lean.getPPNotation do
   let #[f] := (← SubExpr.getExpr).getAppArgs | failure
   guard <| f.isAppOfArity ``Membership.mem 5
   let stx₁ ← SubExpr.withAppArg <| SubExpr.withNaryArg 3 delab