Generalizing let statement

Stream: lean4

[Jad Ghalayini]

I have some code of the form

let x := some complicated expr;
y

and would like to pattern match on the value of x. Is there a nice shorthand to use generalize or some other tactic for this, as I'm struggling to just get it to match the LHS of the let-statement

[Jad Ghalayini]

Note that y depends on x here

[Alexander Bentkamp]

Can you give a concrete example? Do you mean something like this?

example : let x := 0; x + 5 = 5 := by
  intro x
  generalize h : x = x'
  cases x'
  · exact Nat.zero_add 5
  · exact Nat.noConfusion h

[Jad Ghalayini]

I didn't know you could use intro that way; but I was thinking more

(let x := 0; ...) = y

[Alexander Bentkamp]

Ok, so like this?

example : (let x := 42; x + 5) = 47 := by
  generalize h : 42 = x'
  show x' + 5 = 47
  sorry

I don't know any way to avoid repeating the "complicated expr" (in my example 42). Is that what you are asking?

[Jad Ghalayini]

@Alexander Bentkamp yep; in this case it's this massive abomination post-simp

[Sebastian Ullrich]

Do you know about simp (config := { zeta := false })?

[Jad Ghalayini]

@Sebastian Ullrich no; but it didn't help; the LHS of the let-statement is obtained by dsimp which for some reason doesn't seem to zeta-expand anyways

[Leonardo de Moura]

dsimp which for some reason doesn't seem to zeta-expand anyways

I fixed this issue https://github.com/leanprover/lean4/commit/a639eb185cab63adac2616486c2239a796b7b066

@Jad Ghalayini Could you please post a #mwe?