Lean way to write {(x₁, x₂, 0) | x₁, x₂ ∈ F}

Stream: new members

[Martin C. Martin]

How can I write {(x₁, x₂, 0) | x₁, x₂ : F} in Lean? {v : (F × F × F) | v.3 = 0} gets the job done, but isn't similar to the original form.

I guess I can phrase it as, given f : F → F → F × F × F, is there a syntactic sugar for {v ∈ F × F × F | ∃ x₁ x₂ : F, f(x₁, x₂) = v}?

Possibly related, what's this and how do I use it?

[Kyle Miller]

The syntax is more restrictive than you might want, but you can do

example (F : Type) := {(x₁, x₂, 0) | (x₁ : F) (x₂ : F)}

[Martin C. Martin]

Thanks! I feel like I tried that and just got errors, but perhaps I got the syntax wrong.

[Martin C. Martin]

Where can I read about the syntax that's accepted? For example, why {(x₁, x₂, 0) | (x₁ x₂ : F)} doesn't work.

[Eric Wieser]

import Mathlib.Data.Set.Basic fixes it

[Eric Wieser]

#8425 adds documentation

[Martin C. Martin]

It doesn't work for me:

import Mathlib.Data.Set.Basic

variable {F : Type _}

def firstTwo : (Set (F × F × F)) := {(x₁, x₂, 0)| (x₁ x₂ : F)}

On x₂, I get unexpected identifier; expected ')'.

[Eric Wieser]

(x₁ x₂ : F) isn't allowed, you have to write (x₁ : F) (x₂ : F)

[Martin C. Martin]

Ok, thanks. Where can I learn more about why, and what syntax is allowed and what isn't?

[Eric Wieser]

If you write a version that's legal, you can goto definition on the |

[Martin C. Martin]

Thanks. So it turns into ∃ᵉ, good to know.

[Martin C. Martin]

Is there a way to add a constraint to that? The equivalent of {(x₁, x₂, x₃, x₄)| x₃ = 5x₄ + b} ?

[Kyle Miller]

It's not pretty, but you can do {(x₁, x₂, x₃, x₄) | (_ : x₃ = 5*x₄ + b)}, since a constraint is the same as saying that there exists a proof that the constraint is satisfied.

[Kyle Miller]

Eric added such an example in the documentation in this change: https://github.com/leanprover-community/mathlib4/pull/8425/files