`dsimp` regression: `Iff.rfl` proofs are not used by `dsimp`

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

Users of Lean 3 and mathlib3 are used to seeing dsimp make use of proofs of Iff consisting of Iff.rfl. For example, in Lean 3,

def w : Prop → Prop := fun p, p

@[simp] theorem iff_thm (a : Prop) : w a ↔ a := iff.rfl

example (a : Prop) : w a := by dsimp -- rewrites `w a` to `a`

Whereas in Lean 4,

def w : Prop → Prop | p => p

@[simp] theorem iff_thm : w a ↔ a := Iff.rfl

example : w a := by dsimp -- dsimp made no progress

Ideally, dsimp should be able to rewrite the goal using iff_thm in Lean 4 as well.

Context

This issue first arose in March 2023 on Zulip, where the notion of being able to use Iff.rfl proofs with dsimp in Lean 4 was met with support. No issue was filed at the time.

Presently (October 2023), a different case of dsimp not working as expected for the same reason arose on Zulip. (Note: the linked thread also addresses other issues.)

Steps to Reproduce

1. Create a @[simp] theorem iff_thm whose proof consists of Iff.rfl
2. Use dsimp on a goal which includes a match of the lhs or rhs of that lemma

Expected behavior: dsimp rewrites the goal via iff_thm

Actual behavior: dsimp does not use iff_thm

Versions

Lean (version 4.0.0-nightly-2023-08-18, commit 9d05b5f081c2, Release)
macOS Ventura 13.4

Impact

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

Start by reproducing the minimal dsimp example with an @[simp] theorem proved by Iff.rfl on the stated Lean version. Trace the dsimp tactic and its handling of Iff proofs, then add coverage showing that the goal is rewritten as expected. Done means the reproduction succeeds without mathlib4 or std4 dependencies.