set

Stream: general

[Zhengying]

Hi there, I'm a total newbee for using Lean. Can anyone tell me how to prove (6 : ℝ) ∈ ({6} : set ℝ) ? Which tactic should I use? And in general how should I find which tactic to apply whenever I encounter a new symbol?

[Kevin Buzzard]

I would definitely try library_search but actually before that I would start guessing at names, for example this is almost certainly called set.mem_singletom or something. In particular I would use the exact tactic because exactly the result that x is in {x} is already in the library. There are not thousands of tactics, it doesn't work like that. There are probably less than 100 tactics in total. There are tens of thousands of already proven theorems and that's what you need. When encountering a new symbol you should find the files in the maths library which talk about the symbol and read the docstrings and theorem statements.

[Alex J. Best]

In this case it should be a direct application of some lemma, rather than a tactic that does many things for you. And the tactic library_search should find the lemma for you

[Kevin Buzzard]

You need to learn the API for the concept, not a new tactic

[Riccardo Brasca]

It's docs#set.mem_singleton. But I totally agree with Kevin and Alex that the most important thing to understand is that such a lemma is surely already in mathlib and that library_search will find it for you. After some time you will also be able to guess its name.