unfolding definitions made with let

Stream: new members

[Simon Jacobsson]

In Theorem Proving In Lean (Release 3.23.0), it is stated that the let tactic is used to introduce local definitions and that these can be unfolded. I haven't found how to unfold them, though. I tried the following

 example : exists x, x + 2 = 8 :=
  begin
    let a := 3 * 2,
    have h : a = 6,
      unfold a,
  end

but I got the error unfold tactic failed, a does not have equational lemmas nor is a projection. How can I interpret this error message? Is it possible to do what I'm trying to do, to unfold a definition made with let in tactic mode?

[Markus Himmel]

unfold only really works for things defined with def. You could try

 example : exists x, x + 2 = 8 :=
  begin
    let a := 3 * 2,
    have h : a = 6,
      simp only [a],
  end

or

import tactic

 example : exists x, x + 2 = 8 :=
  begin
    set a := 3 * 2 with ha,
    have h : a = 6,
      rw ha,
  end

[Simon Jacobsson]

Okay thanks that works!

[Simon Jacobsson]

I think it is reasonable to use this workflow rather than def because I need to make definitions that use many local variables.

[Alex J. Best]

If you use tactic#set instead of let there is an option to create the hypothesis h automatically