SetLike coe to type display

Stream: mathlib4

[Patrick Massot]

Do we use the SubType pretty-printer on purpose when using the coercion to type of SetLike?

import Mathlib.GroupTheory.Subgroup.Basic

example {G : Type} [Group G] (H : Subgroup G) : H := by
  -- goal is now { x // x ∈ H } instead of ↥H
  use 1
  exact Subgroup.one_mem H

I would really like to get back the ↥H that we had in Lean 3. In the above #mwe it isn't too bad but in actual example it really blows up the tactic state complexity.

[Yaël Dillies]

What about we make SetLike.coe semireducible, the same way as FunLike.coeFn is?

[Patrick Massot]

@Eric Wieser

[Eric Wieser]

I don't think making types semireducible is a good idea, it's caused us problems in lots of places (eg docs#Module.Dual)

[Eric Wieser]

But we could certainly write a custom pretty printer that shows the output you want

[Eric Wieser]

Or maybe even just custom notation, where ↥H is notation for { x // x ∈ H } for any Membership operation

[Patrick Massot]

I tried but, unsurprisingly, I wasn't able to figure out the incantation. Help from an expert delaborator/unexpander writer would be very welcome.

[Patrick Massot]

This issue makes it really hard to write any exercise about subgroups or submodules. It would be really nice to get help from people who can write delaborators. @Mario Carneiro @Kyle Miller @Wojciech Nawrocki

[Kyle Miller]

@Patrick Massot I just made a delaborator for SetLike's CoeSort. I've only tested it on your example:

import Mathlib.GroupTheory.Subgroup.Basic

namespace SetLike
open Lean.PrettyPrinter.Delaborator

@[delab app.Subtype]
def delabSubtypeSetLike : Delab := whenPPOption Lean.getPPNotation do
  let #[_α, .lam n _ body _] := (← SubExpr.getExpr).getAppArgs | failure
  let (``Membership.mem, #[_, _, inst, _, _S]) := body.getAppFnArgs | failure
  guard <| inst.isAppOfArity ``SetLike.instMembership 3
  SubExpr.withAppArg <| SubExpr.withBindingBody n <| SubExpr.withNaryArg 4 do
    let S ← delab
    `(↥ $S)

end SetLike

example {G : Type} [Group G] (H : Subgroup G) : H := by
  -- goal is now ↥H instead of { x // x ∈ H }
  use 1
  exact Subgroup.one_mem H

[Patrick Massot]

Awesome! Are you PRing it already or should I do it?

[Eric Wieser]

The above misfires on

example {G : Type} [Group G] (H : Subgroup G) : { x // 1 * x ∈ H } := by

[Eric Wieser]

I think this might be correct?

@[delab app.Subtype]
def delabSubtypeSetLike : Delab := whenPPOption Lean.getPPNotation do
  let #[_α, .lam n _ body _] := (← SubExpr.getExpr).getAppArgs | failure
  let (``Membership.mem, #[_, _, inst, .bvar 0, _S]) := body.getAppFnArgs | failure
  guard <| inst.isAppOfArity ``SetLike.instMembership 3
  SubExpr.withAppArg <| SubExpr.withBindingBody n <| SubExpr.withNaryArg 4 do
    let S ← delab
    `(↥ $S)

[Kyle Miller]

I've made #7927. I'll add a test that it actually pretty prints as advertised before marking it awaiting-review