## Stream: general

### Topic: unfold local definitions

#### Reid Barton (May 10 2018 at 16:35):

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

#### Reid Barton (May 10 2018 at 16:45):

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 (May 10 2018 at 16:50):

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

#### Gabriel Ebner (May 10 2018 at 16:51):

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


#### Reid Barton (May 10 2018 at 17:36):

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

Last updated: May 12 2021 at 04:19 UTC