finding lemmas efficiently

Stream: new members

[Răzvan Flavius Panda]

I'm looking to find the lemma for ~a = a -> a = 0 but did not manage to do it using autocomplete guessing or searching in the mathlib github
what are the best ways to find lemmas? anything like hoogle for Haskell?

[Hanting Zhang]

docs#library_search will try to close goals by searching the library.

[Răzvan Flavius Panda]

oh, I forgot about that. thank you

[Bryan Gin-ge Chen]

tactic#library_search is a working link :wink:

[Bryan Gin-ge Chen]

Assuming the ~ in your message is supposed to be a minus, if this exact result is in mathlib, the type and the #naming conventions tell us that the lemma name must start with eq_zero_of, and then neg should appear in some form in what follows. And indeed, docs#eq_zero_of_neg_eq has type -a = a -> a = 0.

Note that it was also possible that this implication only appears in an iff lemma, so sometimes that's another thing to guess.

[Răzvan Flavius Panda]

yeah, - I'm too tired to type