have and let

Stream: new members

[Joscha Mennicken]

Hello, I'm wondering about the specifics of have and let in lean4 (not the tactics). Why is have defined the way it is? And does it matter when handling variables of type Prop, since their values are irrelevant anyways?

[Joscha Mennicken]

It seems to me like let can be used everywhere have can be used and I'd like to know what scenarios have is meant for.

[Kevin Buzzard]

let just clogs things up more. If I've proved h : A = B after some long struggle then I want my local context to say h : A = B and not h : A = B := <gigantic 20 line proof which makes my proof state much harder to read>

[Joscha Mennicken]

So have is a way to explicitly throw away unnecessary information. Makes sense