nonempty_of_nonempty_subtype

Stream: Is there code for X?

[Yaël Dillies]

Does this exist? And is there a problem with making it an instance?

instance nonempty_of_nonempty_subtype {α : Type*} {p : α → Prop} [h : nonempty (subtype p)] :
  nonempty α :=
h.elim (λ x, ⟨x.val⟩)

[Eric Wieser]

I think that's nonempty.map subtype.val?

[Gabriel Ebner]

And is there a problem with making it an instance?

Yes, it will cause type class search to go through nonempty nat, nonempty (subtype ?m_1), nonempty (subtype ?m_2), ...