library_search on subgroup bot_le

Stream: general

[Alex J. Best]

@Scott Morrison (and everyone!) after learning about library_search! I went and looked at some situations where I'd have expected library_search to work but it didn't and still had some issues, here is a MWE: Is there a reason I shouldn't expect library search to work in the second example, despite it doing so in the first?

import tactic
import group_theory.subgroup

example {L : Type} [complete_lattice L] (a : L) : (⊥ : L) ≤ a :=
begin
  library_search, --works (bot_le)
end

example {G : Type} [group G] (a : subgroup G) : (⊥ : subgroup G) ≤ a :=
begin
  library_search!, --fails
end

[Scott Morrison]

I'm happy to call that a bug; my model of how library_search! works calls for it being strictly more successful. :-)

[Scott Morrison]

Looks like I have some library_search hacking coming up.

[Scott Morrison]

I've starred this message, but if you want to file an issue and/or anyone wants to diagnose / solve it themselves, go for it!