unfold local definitions

Stream: general

[Reid Barton]

Is there a way in tactic mode to unfold something bound by a surrounding let?

[Reid Barton]

I guess I also want to do a beta reduction, since the thing I want to unfold is a function whose definition is assume x, ...

[Gabriel Ebner]

You can do dsimp [x] if x is the let-binding in the local context.

[Gabriel Ebner]

example : let x := 5 in x + x > 0 :=
begin
intro x,
dsimp [x],
-- 5 + 5 > 0
end

[Reid Barton]

Oh. Thanks!
I guess I never tried precisely this, but only unfold and rw.