simp [*] regression

[PatrickMassot]

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 Lean 4 simp [*] is less powerful than the Lean 3 version.

Context

This was reported on Zulip.

The following works in Lean 3 but not in Lean 4:

example (α : Type) (y : α) (P : α → Prop) (y) (h : P (y,y).1) : P y := by
  simp only [h]

Expected behavior:

The proof works.

Actual behavior:

In Lean 4, you need to first use dsimp only at h.

Versions

Lean (version 4.2.0-rc1, commit a62d2fd, Release)
Ubuntu 22.04

Impact

This example is probably not crucial, but I'm trying to collect minimized examples of all simp regressions compared to Lean 3, where regression is defined strictly as "a proof needs more work in Lean 4", it does not mean the Lean 3 behavior was correct and should be restored at all cost.

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

[leodemoura]

Same as #2670

[leodemoura]

Fixed. See fix for #2670