From 078d254fb1ecc6aef801d4a9d377c92ce2550e8c Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Tue, 9 Apr 2024 03:53:46 +0000
Subject: [PATCH] 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       | 6 ++++--
 Mathlib/CategoryTheory/Closed/Cartesian.lean  | 2 +-
 Mathlib/CategoryTheory/Monoidal/Category.lean | 2 +-
 Mathlib/LinearAlgebra/Matrix/PosDef.lean      | 1 +
 Mathlib/Order/SetNotation.lean                | 5 ++---
 5 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean
index 8719e5b022c268..6c01328379761a 100644
--- a/Mathlib/Algebra/BigOperators/Basic.lean
+++ b/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
diff --git a/Mathlib/CategoryTheory/Closed/Cartesian.lean b/Mathlib/CategoryTheory/Closed/Cartesian.lean
index eb73ea21bb67f1..fd59ded0434368 100644
--- a/Mathlib/CategoryTheory/Closed/Cartesian.lean
+++ b/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
diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean
index 87ae1864de3573..b0fb46d5f4b08b 100644
--- a/Mathlib/CategoryTheory/Monoidal/Category.lean
+++ b/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
diff --git a/Mathlib/LinearAlgebra/Matrix/PosDef.lean b/Mathlib/LinearAlgebra/Matrix/PosDef.lean
index 0ec89e2793c942..744a7f372a5545 100644
--- a/Mathlib/LinearAlgebra/Matrix/PosDef.lean
+++ b/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
diff --git a/Mathlib/Order/SetNotation.lean b/Mathlib/Order/SetNotation.lean
index 22417314a592fb..ef40575a35d8ab 100644
--- a/Mathlib/Order/SetNotation.lean
+++ b/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
-