feat: pretty print as ↥S instead of { x // x ∈ S } for SetLike (#…

…7927)

Adds a delaborator detecting `{ x // x ∈ S }` where the membership uses `SetLike.instMembership`, since then this matches the `CoeSort` instance for `SetLike`.

Mathlib/Data/SetLike/Basic.lean

@@ -108,12 +108,29 @@ variable {A : Type*} {B : Type*} [i : SetLike A B]
 
 instance : CoeTC A (Set B) where coe := SetLike.coe
 
-instance (priority := 100) : Membership B A :=
+instance (priority := 100) instMembership : Membership B A :=
   ⟨fun x p => x ∈ (p : Set B)⟩
 
 instance (priority := 100) : CoeSort A (Type _) :=
   ⟨fun p => { x : B // x ∈ p }⟩
 
+section Delab
+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]
+def delabSubtypeSetLike : Delab := whenPPOption getPPNotation do
+  let #[_, .lam n _ body _] := (← getExpr).getAppArgs | failure
+  guard <| body.isAppOf ``Membership.mem
+  let #[_, _, inst, .bvar 0, _] := body.getAppArgs | failure
+  guard <| inst.isAppOfArity ``instMembership 3
+  let S ← withAppArg <| withBindingBody n <| withNaryArg 4 delab
+  `(↥$S)
+
+end Delab
+
 variable (p q : A)
 
 @[simp, norm_cast]

test/set_like.lean

@@ -5,6 +5,20 @@ import Mathlib.FieldTheory.Subfield
 
 set_option autoImplicit true
 
+section Delab
+variable {M : Type u} [Monoid M] (S S' : Submonoid M)
+
+/-- info: ↥S → ↥S' : Type u -/
+#guard_msgs in #check S → S'
+
+/-- info: ↥S : Type u -/
+#guard_msgs in #check {x // x ∈ S}
+
+/-- info: { x // 1 * x ∈ S } : Type u -/
+#guard_msgs in #check {x // 1 * x ∈ S}
+
+end Delab
+
 example [Ring R] (S : Subring R) (hx : x ∈ S) (hy : y ∈ S) (hz : z ∈ S) (n m : ℕ) :
     n • x ^ 3 - 2 • y + z ^ m ∈ S := by
   aesop