Searching proofs

Stream: new members

[Xavier Généreux]

Hey all! Currently my strategy to get a feel of how things work is to find a pre-existing proof in mathlib that resembles what I am trying to do and adapt it.

That being said, I would much prefer seeing examples of the lemmas that seem like they could do the trick in action. E. g. is there any way to find proofs that use, say, le_Sup? This would help me understand how it is used.

[Riccardo Brasca]

In VS Code you can use ctrl+shift+f to search in a whole project (mathlib for example). You will find all occurrences of le_Sup.

[Yakov Pechersky]

However, lemmas that are very "simple" like inf_le_sup could be occurring more often than a Ctrl-F finds, because it might be part of a simp step.

[Johan Commelin]

Related: the suggest tactic.

[Xavier Généreux]

Thanks!