fix: add missing withOverApps (#12022)

This fixes the delaborators for sums, products, infimums, and supremums of pi types and matrices.

Also adds a missing `whenPPOption getPPNotation` to `Prefunctor.obj`.

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/delaborator.20for.20Finset.2Esun.20does.20not.20trigger/near/432068318).

Mathlib/Algebra/BigOperators/Basic.lean

@@ -126,7 +126,8 @@ open Std.ExtendedBinder
 
 /-- Delaborator for `Finset.prod`. The `pp.piBinderTypes` option controls whether
 to show the domain type when the product is over `Finset.univ`. -/
-@[scoped delab app.Finset.prod] def delabFinsetProd : Delab := whenPPOption getPPNotation do
+@[scoped delab app.Finset.prod] def delabFinsetProd : Delab :=
+  whenPPOption getPPNotation <| withOverApp 5 <| do
   let #[_, _, _, s, f] := (← getExpr).getAppArgs | failure
   guard <| f.isLambda
   let ppDomain ← getPPOption getPPPiBinderTypes
@@ -146,7 +147,8 @@ to show the domain type when the product is over `Finset.univ`. -/
 
 /-- Delaborator for `Finset.prod`. The `pp.piBinderTypes` option controls whether
 to show the domain type when the sum is over `Finset.univ`. -/
-@[scoped delab app.Finset.sum] def delabFinsetSum : Delab := whenPPOption getPPNotation do
+@[scoped delab app.Finset.sum] def delabFinsetSum : Delab :=
+  whenPPOption getPPNotation <| withOverApp 5 <| do
   let #[_, _, _, s, f] := (← getExpr).getAppArgs | failure
   guard <| f.isLambda
   let ppDomain ← getPPOption getPPPiBinderTypes

Mathlib/CategoryTheory/Closed/Cartesian.lean

@@ -116,7 +116,7 @@ notation:20 A " ⟹ " B:19 => (exp A).obj B
 open Lean PrettyPrinter.Delaborator SubExpr in
 /-- Delaborator for `Prefunctor.obj` -/
 @[delab app.Prefunctor.obj]
-def delabPrefunctorObjExp : Delab := do
+def delabPrefunctorObjExp : Delab := whenPPOption getPPNotation <| withOverApp 6 <| do
   let e ← getExpr
   guard <| e.isAppOfArity' ``Prefunctor.obj 6
   let A ← withNaryArg 4 do

Mathlib/CategoryTheory/Monoidal/Category.lean

@@ -125,7 +125,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]
-def delabTensorUnit : Delab := whenPPOption getPPNotation do
+def delabTensorUnit : Delab := whenPPOption getPPNotation <| withOverApp 3 do
   let e ← getExpr
   guard <| e.isAppOfArity ``MonoidalCategoryStruct.tensorUnit 3
   let C ← withNaryArg 0 delab

Mathlib/LinearAlgebra/Matrix/PosDef.lean

@@ -143,6 +143,7 @@ open Lean PrettyPrinter.Delaborator SubExpr in
 def delabSqrt : Delab :=
   whenPPOption getPPNotation <|
   whenNotPPOption getPPAnalysisSkip <|
+  withOverApp 7 <|
   withOptionAtCurrPos `pp.analysis.skip true do
     let e ← getExpr
     guard <| e.isAppOfArity ``Matrix.PosSemidef.sqrt 7

Mathlib/Order/SetNotation.lean

@@ -101,7 +101,7 @@ open Lean Lean.PrettyPrinter.Delaborator
 
 /-- Delaborator for indexed supremum. -/
 @[delab app.iSup]
-def iSup_delab : Delab := whenPPOption Lean.getPPNotation do
+def iSup_delab : Delab := whenPPOption Lean.getPPNotation <| withOverApp 4 do
   let #[_, ι, _, f] := (← SubExpr.getExpr).getAppArgs | failure
   unless f.isLambda do failure
   let prop ← Meta.isProp ι
@@ -129,7 +129,7 @@ def iSup_delab : Delab := whenPPOption Lean.getPPNotation do
 
 /-- Delaborator for indexed infimum. -/
 @[delab app.iInf]
-def iInf_delab : Delab := whenPPOption Lean.getPPNotation do
+def iInf_delab : Delab := whenPPOption Lean.getPPNotation <| withOverApp 4 do
   let #[_, ι, _, f] := (← SubExpr.getExpr).getAppArgs | failure
   unless f.isLambda do failure
   let prop ← Meta.isProp ι
@@ -299,4 +299,3 @@ theorem iSup_eq_iUnion (s : ι → Set α) : iSup s = iUnion s :=
 theorem iInf_eq_iInter (s : ι → Set α) : iInf s = iInter s :=
   rfl
 #align set.infi_eq_Inter Set.iInf_eq_iInter
-