Introduce a let in a subexpression

Stream: lean4

[Bolton Bailey]

How do I introduce i to the context here?

example : (let i := 2; i + 3) = 5 := by
  intro i -- fails

[Bolton Bailey]

I have a large number of let statements and I'd like to introduce them all

example : (let i := 2; let j := 1; let k := 2; i + j + k) = 5 := by
  intros i j k

[Richard Osborn]

Something like this?

import Mathlib

example : (let i := 2; let j := 1; let k := 2; i + j + k) = 5 := by
  lift_lets
  extract_lets i j
  dsimp [i,j]

[Leni Aniva]

Is there a way to solve this without using mathlib?

[Kyle Miller]

Not really. The lift_lets tactic is hard to reproduce with other tactics.

You can replace extract_lets i j with intro i j however.

[Leni Aniva]

I hope lift_lets can be included included in the prelude then

[Kim Morrison]

@Leni Aniva, it looks like this would be easy to do, and I agree it would be reasonable. Currently Mathlib/Tactic/LiftLets imports Mathlib/Tactic/Basic, but it seems that can be replaced with import Lean (but should be replaced with something finer).

If you wanted to make a PR moving this to the lean4 repository (I'm sure Kyle, the author, won't object), I could help clean it up and turn it into a built-in tactic. Otherwise we can try to get to it later.

[Kyle Miller]

I'd be happy to upstream these tactics myself if core wants them.

[Kim Morrison]

I think it's reasonable. They are fundamental tactics that you inevitably need once you're dealing with let, there's no need for them to be in Mathlib, and we have evidence above that they are wanted outside Mathlib.

[Kim Morrison]

I guess extract_lets uses some other stuff in Mathlib still.

[Kim Morrison]

Oh, maybe just letDepth, which is trivial to upstream.