Finding axioms and theorems in mathlib

Stream: new members

[Victor Miller]

I'm in my fourth iteration of trying to get into Lean. I did go through the Natural Numbers Game, which was fun a challenging, though the meaning and scope of many tactics was still not clear. Right now, in trying to do the exercises from Theorem proving in Lean it seems necessary to find the axioms and theorems pertaining to a particular structure (such as Group). Is there some organized way of doing this, besides trying to guess what they might be called?

[Patrick Massot]

it seems necessary

No it isn't.

[Patrick Massot]

If you tell us about a more specific problem you have then you will get an even more useful answer.

[Alex J. Best]

In general though, the tactics apply?, rw? and exact? are good ways of finding lemmas that apply in a given goal state in some way. I would imagine that TPIL is set up so that the exercises can be done with only the lemmas introduced earlier in the same text though

[Matt Diamond]

It's also useful to just read through the docs for the particular subject you're working in... you start to pick up on naming patterns and it makes it easier to guess when searching for them.