What's the difference between the have tactic and the haveI?

Stream: lean4

[张守信(Shouxin Zhang)]

Hi everyone! I'm collecting examples of how to use have in Lean 4 to compile into a tutorial for our Lean 4 tactics repository. While I often see tactics like haveI and letI in others' proofs, I still don't understand the fundamental differences between them and have and let. Are there any examples that highlight the advantages of using haveI?

[Kevin Buzzard]

The difference between have and let: this is what I tell beginners. Everything in lean is a universe, a type or a term. There are two universes, Type and Prop (this is a lie, but mathematician beginners don't need to know about higher type universes). The types in Type correspond to sets, and the terms of those types correspond to the elements of the sets. The types in Prop are the theorem statements, and the terms of those types are the proofs of the statements. You use let if you're working in the Type universe and have if you're working in the Prop universe

[Kevin Buzzard]

I would not tell beginners about the difference between have and haveI, or between let and letI. I'm not sure I know a single example that a beginner would see where these things aren't completely interchangeable

[Kyle Miller]

(I suspect many uses of haveI and letI are mistakes, unless they appear in a type signature. In Lean 3 they were completely different tactics and were for resetting the instance cache. Nowadays they zeta reduce themselves immediately.)

[Patrick Massot]

Yes, I think a overwhelming majority of uses are confusing coming from their Lean 3 homonyms. It’s sad because many people doing this mistake have never used Lean 3 but they are misled by examples written by people who used Lean 3.