Compare `have`, `let`, `haveI`, `letI`

What question should the reference manual answer?

The difference between let and have is something that most Lean users need to learn about at some point. The constructs haveI and letI are less well-known and also much less well-understood. This is made worse by the fact that haveI meant something completely different in Lean 3 (it reset the instance cache), and so some users still use haveI today in situations where they should just be using have instead. The docstrings for haveI and letI explain what sets them apart from have and let, but they do so using very low-level language (let_fun, which the reference manual's jump-to box doesn't even find), so unless you know a lot about Lean the explanation isn't really helpful.

So the questions are

• What is the difference between have, let, haveI, letI?
• When should I use which (ideally with examples)?

Start by reading the existing docstrings for haveI and letI and the surrounding reference-manual material. Compare have, let, haveI, and letI from the user's perspective, then update the reference manual so it explains when to use each and includes examples answering both questions.