let or def inside a proof

Stream: new members

[Michael Beeson]

I am trying to introduce a new variable and its definition in tactic mode in a proof, for example if c:M is already in the environment then

let f:M := c,

(which is wrong); it's wrong because it doesn't mention any hypothesis. After the correct line of code, which I want to know,
I should see

h: f = c

in my environment. I don't find an example of how to do this.

[Kevin Buzzard]

set f : M := c with h,

[Michael Beeson]

Thanks!

[Kevin Buzzard]

Note that after let f : M := c,, f = c is true by definition (so it can be proved with refl).

[Michael Beeson]

That command is nowhere mentioned in the Lean Reference Manual Release 3.3.0, by the way.

[Michael Beeson]

I tried a let command and then my environment contains f:M but I don't have a way to rewrite f as c. I guess set will do what I want.

[Kevin Buzzard]

set? Oh -- it might be a mathlib tactic. Mathlib is nowhere mentioned in the Lean Reference Manual

[Kevin Buzzard]

If you use let then f = c is true by definition so you can change between f's and c's using the change tactic.

[Michael Beeson]

Is there a document that I can read, of the same level of detail as the Lean Reference Manual, that does describe mathlib and all its useful tactics?

[Michael Beeson]

It's nice of you to explain set and change and let to me here, but it's surely not the most efficient use of your time.

[Kevin Buzzard]

Not really. Mathlib is too new. When I was learning Lean I used to occasionally look through the 2018/19 analogue of this page which lists all mathlib tactics.

[Michael Beeson]

OK, well then, thanks for that link and for your time and energy and especially quick response here on Zulip.