Introducing a new variable

Stream: new members

[Frédéric Le Roux]

I have a stupid question. What is the Lean equivalent of a sentence like "Let ε =1-d" (assuming d is a variable in the current setting). Typically, in a proof where I have to show the existence of some object, I would like to name the object. Like in the tactic "use 1-d", but introducing a notation.

[Kevin Buzzard]

In tactic mode: let ε := 1 - d. But actually I prefer set ε := 1 - d with hε because then hε contains the proof that ε = 1 - d.

[Frédéric Le Roux]

Thank you!

[Kevin Buzzard]

One thing I noticed at Xena yesterday when writing a proof with an undergraduate was that after set L := factors n with hLn I was forever rewriting hLn, and at the end of it I was beginning to wish that I'd never introduced the notation at all and had just put factors n everywhere instead of L :-)