When writing this answer, I had a hard time finding the lemma I needed to prove
2 ≤ 3. In Agda, when I have a goal, I can press
refine and Agda will either insert a constructor or tell me she doesn't know which constructor to use, so I can pick one from the list. In Lean4 if I place a metavariable in the goal, she simply say "don't know how to synthesize this" (I'm paraphrasing, but it's something like that). Even without these error messages, I can click in the IDE to jump to the definition of the type, and I can read the definition to know the available constructors.
In Lean4 the situation is totally different. I looked up the definition of
< and it's a macro or a notation definition, which I cannot jump to further definition (I tried clicking but it doesn't do anything). I looked around the code and found the definition -- it's
LT, a class. So, to work with it, I need to know which instance I'm using in order to find the available constructors. However, I didn't find an easy way to lookup the instance used in my incomplete proof.
I guess this is probably not the preferred way of programming in Lean4. I guess Lean4 wants me to work with mathematics abstractly, but I am unfamiliar with the Lean4 library and the Lean4 best practices. I can work pretty well with Cubical Agda library without prior knowledge to it by using the IDE extensively, and I wish to learn how can I do similar things in Lean4.
Please tell me anything I can do, even a bunch of keyboard shortcuts will help me a lot.