library_search returning non-working suggestion

Stream: new members

[Carl Friedrich Bolz-Tereick]

Is it expected that library_search sometimes returns a suggestion that only almost works? Here's an example that I ran into today:

import data.fintype.basic

lemma surprising_library_search_result (T : Type) (s t : finset T) (a : T) (ha : a ∈ t) (hsub : t ⊆ s) : a ∈ s :=
begin
    library_search -- this suggests "exact hsub a ha", which doesn't work, needs to be "hsub ha" or "@hsub a ha"
end

[Kevin Buzzard]

That's probably a bug. There might be a library search issue on GitHub, you could add your example to that or, if there isn't, you can open a new issue. Otherwise your comment might just get lost in general Zulip noise

[Shing Tak Lam]

#3093 . I found this same issue a few days ago.

[Carl Friedrich Bolz-Tereick]

right, thank you, @Shing Tak Lam seems you found the exact same example even :-)

[Shing Tak Lam]

Your example is the exact same (modulo variable names) as mine from the GitHub error lol.

https://github.com/leanprover-community/mathlib/issues/3093#issuecomment-645238764

I think this is with how how library_search deals with ∀ ⦃a⦄, but I'm not sure. I tried debugging the issue with some help from Gabriel, but to no avail (see the comment in the thread).

[Carl Friedrich Bolz-Tereick]

right

[Carl Friedrich Bolz-Tereick]

it wasn't a big problem to still use the result, I was just surprised

[Jannis Limperg]

[Sorry, wrong thread, I'm too stupid for Zulip.]