Lean4 tutorials : What is the difference between have & let

Stream: new members

[Shubham Kumar]

Syntactically have and let seem similar where have h : <some type> := <some expr> and let h : <some type> := <some expr> .
Is there any semantic difference and can I use them interchangeably in a proof?

[Adam Topaz]

have is for props and let is for data. At least that's the quick answer.
If you use have to "define" something like a natural number or a function, then lean will only remember that it's a term of the given type without actually remembering the definition you give. In those cases you should use let (or better, mathlib's set)

[Mario Carneiro]

The difference is that after a let, the value of the declaration is interchangeable with the introduced name (they are definitionally equal), while in a have the name is opaque