Exists Unique

Stream: mathlib4

[Dan Velleman]

If I state the theorem ∃! (x : nat), x = 0 in Lean 3 and prove it in tactic mode, then in the tactic state the goal is listed as ∃! (x : ℕ), x = 0. If I state the same theorem in Lean 4, then in the tactic state the goal is listed as ExistsUnique fun x => x = 0. Not wrong, but not nearly as good as Lean 3.

[Henrik Böving]

This could be fixed with an application unexpander for ExistsUnique I think?