ExistsUnique.unique

Stream: mathlib4

[Dan Velleman]

The statement of ExistsUnique.unique (in Mathlib.Init.Logic) is:

theorem ExistsUnique.unique {α : Sort u} {p : α → Prop}
    (h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂

Wouldn't it be better to use {{y₁ y₂ : α}} rather than {y₁ y₂ : α}? At the moment, the following example produces a "don't know how to synthesize implicit argument" error:

example (α : Type) (p : α → Prop) (h : ∃! (x : α), p x) : True := by
  have h2 := ExistsUnique.unique h

With {{y₁ y₂ : α}}, there would be no error.

[Yaël Dillies]

Is there a lemma with implicit arguments your argument does not apply to?

[Dan Velleman]

Perhaps not. I guess I was just thinking of ExistsUnique.unique as a way of extracting the uniqueness half from a statement that starts with ∃!. But it doesn't work that way--it lets you use the uniqueness half, but it doesn't let you extract the uniqueness half as a new hypothesis.

[Dan Velleman]

Probably not important.