Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The new behavior of simp (config := {zeta := false}) is not the expected one. It seems to refuse any interaction with a variable defined using let.

Context

See discussion on Zulip.

Steps to Reproduce

axiom abs : Int → Int

axiom abs_eq_self {a : Int }: abs a = a ↔ 0 ≤ a 

example (x : Int) : False := by
  let y := x/2
  have h : 0 ≤ y := sorry
  have : abs y = y := by
    -- generalize y = z at *
    simp (config := {zeta := false}) only [abs_eq_self.mpr h]
  sorry

Expected behavior: [Clear and concise description of what you expect to happen]

The simp call closes the goal without needing the generalize line.

Actual behavior: [Clear and concise description of what actually happens]

simp makes no progress.

Versions

Lean (version 4.3.0-rc1, commit baa4b68, Release)
Ubuntu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.