Set-builder notation

Stream: general

[Martin Dvořák]

I have a pet peeve regarding the set-builder notation in the Infoview.
There seem to be some technical limitations that prevent Infoview from displaying more than one token on the left from | in the set definition.
For example:

import Mathlib.Algebra.Order.Monoid.Canonical.Defs
import Mathlib.Order.UpperLower.Basic

/-- A canonically ordered additive cancellative commutative monoid is
    a canonically ordered additive commutative monoid in which
    addition is cancellative. -/
class CanonicallyOrderedAddCancelCommMonoid (M : Type*)
  extends CanonicallyOrderedAddCommMonoid M, OrderedCancelAddCommMonoid M

variable {M : Type*} [CanonicallyOrderedAddCancelCommMonoid M]

def addMink (x y : UpperSet M) : UpperSet M :=
  ⟨{ a + b | (a ∈ x) (b ∈ y) }, by
    intro c d cd hc
    rw [Set.mem_setOf_eq] at hc ⊢
    obtain ⟨a, ha, b, hb, eq_c⟩ := hc
    use a, ha
    have ac : a ≤ c := le_of_add_le_left eq_c.le
    have ad : a ≤ d := ac.trans cd
    obtain ⟨b', d_eq⟩ := exists_add_of_le ad
    use b'
    have bb' : b ≤ b' := by
      rwa [←eq_c, d_eq, add_le_add_iff_left] at cd
    exact ⟨y.upper' bb' hb, d_eq.symm⟩⟩

When I click at the very beginning of the proof that { a + b | (a ∈ x) (b ∈ y) } is upper set, I get this ugly view:

M: Type u_1
inst✝ : CanonicallyOrderedAddCancelCommMonoid M
x y : UpperSet M
⊢ IsUpperSet {x_1 | ∃ a ∈ x, ∃ b ∈ y, a + b = x_1}

This is essentially written as a predicate on M but displayed in the set-builder syntax.
Instead, I would like to see one of the following (ordered by "what I would like best" first):

{ a + b | (a ∈ x) (b ∈ y) }
{ a + b | ∃ a ∈ x, ∃ b ∈ y }
{ a + b | ∃ a ∈ x, ∃ b ∈ y, }
{ a + b | ∃ a ∈ x, ∃ b ∈ y, True }
fun c => ∃ a ∈ x, ∃ b ∈ y, a + b = c
fun x_1 => ∃ a ∈ x, ∃ b ∈ y, a + b = x_1

This is the end of my rant. I'll fully understand if the answer is "things are difficult; nobody will change it".

[Kevin Buzzard]

What if the answer is "learn how to fix it and then fix it yourself" :-)

[Martin Dvořák]

Then I'll ask for study materials to learn the right toolkit!

[Martin Dvořák]

However, I will be sufficiently at peace if I just hear that somebody tried to do it but it was too hard.

[Eric Wieser]

Is there a simple example where it does do what you expect?

[Martin Dvořák]

Sure!

import Mathlib.Init.Set

example : { a : Nat | a + a = a } = {0} := by
  sorry

[Yaël Dillies]

That's normal set-builder notation, not the version with a function on the left of the |.

[Martin Dvořák]

Yes.

[Kyle Miller]

I think it would be worth taking a census of real-world set builder notations from the literature and then using this to come up with a design for the Lean notations. We cover a lot of the cases I think, but this could really add some polish to sets in mathlib.

[Martin Dvořák]

IMHO stuff like { a + b | (a ∈ x) (b ∈ y) } is what makes the set-builder notation useful.

[Eric Wieser]

It's unfortunate that {a + b | (a b : ℕ) (h : a * b < 4)} is no longer legal

[Eric Wieser]

(you have to write the types of a and b separately)