Rewriting with have

Stream: new members

[Andre Knispel]

If I write have x := t, can I get a proof of x = t somehow? Or do I need to do something else for that?

[Heather Macbeth]

have hides this, but let (same syntax) doesn't.

[Kevin Buzzard]

even better, set x := t with hxt will give you a name for the proof. With let the equality is definitional but doesn't have a name.

[Andre Knispel]

Ah, set is perfect!