apply? not giving obvious short outputs

Stream: mathlib4

[Bolton Bailey]

In the file below, I want to use apply to find the name of the lemma IsClosed.union/see if it exists. In fact this lemma does exist, and works perfectly, and intuitively it feels like the first thing I should try in this situation.

import Mathlib

example (a b : Set ℝ) : IsClosed (a ∪ b) := by
  apply?
  -- apply IsClosed.union

How should I think about the way apply? chooses to order its outputs?

(Edited to be more minimal, the lemma shows up now, but not as the first option)

[Martin Dvořák]

Afaik ordering of the outputs of apply? is a very hard problem that we haven't tackled yet.

[Kim Morrison]

Well, rather I would say we have tackled it, and despite a lot of thought going into it (by both me and Joe Hendrix when preparing std_exact?) the results still leave a lot to be desired. It's not for lack of trying. :-)