fix: respect pp options in delaboration of max/min notation (#29312)

This fixes an issue where `⊔` and `⊓` notation did not respect `pp.explicit` and `pp.notation`.
As discussed [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60pp.2Eexplicit.60.20in.20.60rw.60.20error.20message), this implements the fix suggested by @kmill.

Author: marcusrossel

Mathlib/Order/Notation.lean

@@ -100,7 +100,7 @@ private def hasLinearOrder (u : Level) (α : Q(Type u)) (cls : Q(Type u → Type
 
 /-- Delaborate `max x y` into `x ⊔ y` if the type is not a linear order. -/
 @[delab app.Max.max]
-def delabSup : Delab := do
+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
@@ -112,7 +112,7 @@ def delabSup : Delab := do
 
 /-- Delaborate `min x y` into `x ⊓ y` if the type is not a linear order. -/
 @[delab app.Min.min]
-def delabInf : Delab := do
+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

MathlibTest/Delab/SupInf.lean

@@ -13,7 +13,6 @@ import Mathlib
 #guard_msgs in
 #check (max (min (max (max {0} {1}) (max {2} {3})) (max {4} {5})) (min (min {6} {7}) (min {8} {9})) : Set ℕ)
 
-
 section
 
 variable {α : Type*} (a b : α)
@@ -62,3 +61,24 @@ info: fun α [ConditionallyCompleteLinearOrder α] a b =>
 -/
 #guard_msgs in
 #check fun (α : Type u) [ConditionallyCompleteLinearOrder α] (a b : α) => max a b
+
+-- In this section we check that the delaborator respects the options `pp.explicit` and `pp.notation`.
+section
+
+variable [Min α] [Max α] (a b c : α)
+
+/-- info: (a ⊔ b) ⊓ c : α -/
+#guard_msgs in
+#check min (max a b) c
+
+set_option pp.notation false in
+/-- info: min (max a b) c : α -/
+#guard_msgs in
+#check min (max a b) c
+
+set_option pp.explicit true in
+/-- info: @min α inst✝¹ (@max α inst✝ a b) c : α -/
+#guard_msgs in
+#check min (max a b) c
+
+end