Substitute away let binding in tactic mode

Stream: new members

[Donald Sebastian Leung]

Suppose I have a context of the following form (not sure how to type the turnstile in Lean):

x := <some_term>
|- <some_goal_involving_x>

How do I substitute the value of x into the goal (or hypotheses mentioning x)? rw x does not seem to work.

[Kevin Buzzard]

If you defined x using let then you might be able to write change [what you want the goal to be]. If you have defined it using set x := blah using hx then you can probably just rw hx.

[Donald Sebastian Leung]

So would set x := <some_term> be a better option here?

[Kevin Buzzard]

PS turnstile is \|-. If you copy and paste a turnstile into a Lean file and then hover over it then there's a high chance that it will tell you the keyboard shortcut.

[Kevin Buzzard]

I always use set rather than let but then again I find let quite confusing and I always work in tactic mode.

[Kevin Buzzard]

The change tactic changes a goal to a defeq goal

[Kevin Buzzard]

example : true :=
begin
  let n := 3,
  have h : n = 4,
  change 3 = 4,
  -- works
end

So n is definitionally equal to 3 and so the change tactic works.

[Donald Sebastian Leung]

Kevin Buzzard said:

If you defined x using let then you might be able to write change [what you want the goal to be]. If you have defined it using set x := blah using hx then you can probably just rw hx.

Thank you - set x := <some_term> with hx (and then rw hx later on) worked for me

[Gabriel Ebner]

Another way to rewrite a let definition x by its value is dsimp [x].