Bounded existential unexpander

Stream: mathlib4

[Patrick Massot]

Should we have an unexpander for bounded existential quantifiers? In

import Mathlib

variable (A : Set Nat) (P : Nat → Prop)

#check ∃ n ∈ A, P n

Lean understands what I mean but displays ∃ n, n ∈ A ∧ P n : Prop instead of ∃ n ∈ A, P n : Prop

[Kevin Buzzard]

import Mathlib

variable (f : ℝ → Prop)

#check ∀ ε > 0, f ε -- ∀ (ε : ℝ), ε > 0 → f ε : Prop

[Patrick Massot]

Oh, it doesn't work even for bounded foralls!

[Kevin Buzzard]

Apparently not! I only just noticed this because even though I've ported a bunch of Lean 4 code, I have still never really sat down to write new Lean 4 code from scratch, other than a few levels of NNG.

[Kevin Buzzard]

Maybe it's time to port the tutorial and try testing it on a few people

[Patrick Massot]

We could definitely port of the tutorial at this stage.

[Eric Wieser]

It might be a good testcase for demonstrating mathport on a non-mathlib project

[Patrick Massot]

That's a nice remark. Ideally someone having time should do it and write mathport doc along the way.