fix: (f ⊔ g) i isn't pretty-printed (leanprover-community#34670)

To see; [`Pi.sup_apply`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Lattice.html#Pi.sup_apply)
This can be easily fixed by `withOverApp`. On the way, I minimized imports of the test.

Co-authored-by: Komyyy <pol_tta@outlook.jp>

Author: Komyyy

Mathlib/Order/Notation.lean

@@ -113,27 +113,33 @@ private meta def hasLinearOrder (u : Level) (α : Q(Type u)) (cls : Q(Type u →
 
 /-- Delaborate `max x y` into `x ⊔ y` if the type is not a linear order. -/
 @[delab app.Max.max]
-meta def delabSup : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do
-  let_expr f@Max.max α inst _ _ := ← getExpr | failure
-  have u := f.constLevels![0]!
-  if ← hasLinearOrder u α q(Max) q($(linearOrderToMax u)) inst then
-    failure -- use the default delaborator
-  let x ← withNaryArg 2 delab
-  let y ← withNaryArg 3 delab
-  let stx ← `($x ⊔ $y)
-  annotateGoToSyntaxDef stx
+meta def delabSup : Delab :=
+  whenNotPPOption getPPExplicit <|
+  whenPPOption getPPNotation <|
+  withOverApp 4 do
+    let_expr f@Max.max α inst _ _ := ← getExpr | failure
+    have u := f.constLevels![0]!
+    if ← hasLinearOrder u α q(Max) q($(linearOrderToMax u)) inst then
+      failure -- use the default delaborator
+    let x ← withNaryArg 2 delab
+    let y ← withNaryArg 3 delab
+    let stx ← `($x ⊔ $y)
+    annotateGoToSyntaxDef stx
 
 /-- Delaborate `min x y` into `x ⊓ y` if the type is not a linear order. -/
 @[delab app.Min.min]
-meta def delabInf : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do
-  let_expr f@Min.min α inst _ _ := ← getExpr | failure
-  have u := f.constLevels![0]!
-  if ← hasLinearOrder u α q(Min) q($(linearOrderToMin u)) inst then
-    failure -- use the default delaborator
-  let x ← withNaryArg 2 delab
-  let y ← withNaryArg 3 delab
-  let stx ← `($x ⊓ $y)
-  annotateGoToSyntaxDef stx
+meta def delabInf : Delab :=
+  whenNotPPOption getPPExplicit <|
+  whenPPOption getPPNotation <|
+  withOverApp 4 do
+    let_expr f@Min.min α inst _ _ := ← getExpr | failure
+    have u := f.constLevels![0]!
+    if ← hasLinearOrder u α q(Min) q($(linearOrderToMin u)) inst then
+      failure -- use the default delaborator
+    let x ← withNaryArg 2 delab
+    let y ← withNaryArg 3 delab
+    let stx ← `($x ⊓ $y)
+    annotateGoToSyntaxDef stx
 
 end Mathlib.Meta
 

MathlibTest/Delab/SupInf.lean

@@ -1,5 +1,5 @@
-import Mathlib
-
+module
+import Mathlib.Data.Real.Archimedean
 
 /-- info: max 1 2 : ℕ -/
 #guard_msgs in
@@ -82,3 +82,25 @@ set_option pp.explicit true in
 #check min (max a b) c
 
 end
+
+section Apply
+
+variable {ι α : Type*} [Lattice α] (f g : ι → α) (i : ι)
+
+/-- info: (f ⊔ g) i : α -/
+#guard_msgs in
+#check (f ⊔ g) i
+
+/-- info: (f ⊔ g) i : α -/
+#guard_msgs in
+#check max f g i
+
+/-- info: (f ⊓ g) i : α -/
+#guard_msgs in
+#check (f ⊓ g) i
+
+/-- info: (f ⊓ g) i : α -/
+#guard_msgs in
+#check min f g i
+
+end Apply