let

Stream: general

[Michael Beeson]

Once I have used let X:= something
and then I have a goal involving X, how do I get X replaced by the original something?

[Scott Morrison]

dsimp [X]

[Michael Beeson]

Yes, that worked! TYVM!

[Michael Beeson]

Was there a way other than Zulip for me to have learned that? Not mentioned in the manual where "let" is briefly discussed.

[Niels Voss]

There was a thread on this somewhat recently: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/How.20to.20unwrap.20a.20let.20expression
There isn't really a good way to have found this information, but dsimp is not the only way to unfold the let expression

[Niels Voss]

The main difference between let and have is that when you do let X := something now X is definitionally equal to something so you can prove X = something with only rfl

[Niels Voss]

Sometimes you don't even need to unfold X, since if the goal is something = 37 then Lean will accept instead a proof that X = 37 (in practice unfolding X often makes things simpler). I do wish this was documented somewhere though.

[Sophie Morel]

You can also use set, as in set X := something with hX, then you will have a hypothesis hX in your context that says X = something and you can feed it to rw. In most cases simp and its friends will do the job, but this is still a useful trick sometimes.

[Sophie Morel]

Oops, this was already mentioned by Kevin in the linked thread. My bad.

[Kyle Miller]

If #5717 gets merged, then you'll be able to do unfold_let X (docstring in PR)

This is like dsimp but it unfolds X without touching anything else. dsimp can do other reductions too.