## Stream: new members

### Topic: let or def inside a proof

#### Michael Beeson (Sep 09 2020 at 21:55):

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 (Sep 09 2020 at 21:56):

set f : M := c with h,

Thanks!

#### Kevin Buzzard (Sep 09 2020 at 21:57):

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

#### Michael Beeson (Sep 09 2020 at 21:59):

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

#### Michael Beeson (Sep 09 2020 at 22:01):

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 (Sep 09 2020 at 22:02):

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

#### Kevin Buzzard (Sep 09 2020 at 22:02):

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 (Sep 09 2020 at 22:03):

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 (Sep 09 2020 at 22:04):

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 (Sep 09 2020 at 22:04):

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 (Sep 09 2020 at 22:05):

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

Last updated: Dec 20 2023 at 11:08 UTC