`simp` unable to rewrite seemingly identical terms

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Hello, I'm new to Lean so I'm not sure whether this is an expected behavior:

def f.{u, v} {T : Type u} {U : Type v} (x : T) (y : U) : T := z
  where z := x

theorem test (h₁ : f x y = 0) : true := by
  generalize h₂ : f.z x = w
  simp only [f] at h₁
  simp only [h₁] at h₂ -- This fails
  -- This works: rw [h₁] at h₂
  sorry

At simp only [h₁] at h₂, the proof state is

x : ℕ
U : Type u_1
y : U
h₁ : f.z x = 0
w : ℕ
h₂ : f.z x = w
⊢ true = true

So the simp should work there right?
I suspect it's because of the definition of f.z somehow captures the unused universe v.
This could also be related to #4613

With set_option trace.Meta.Tactic.simp true enabled, I also got this confusing trace

[Meta.Tactic.simp.unify] h₁:1000, failed to unify
      f.z x
    with
      f.z x

Related Issues

Potentially related to #4613 but not sure.

Versions

I'm using Lean version 4.23.0-rc2

Start by running the minimal reproducer from the issue against the latest nightly release, then inspect the simp trace produced by set_option trace.Meta.Tactic.simp true. Investigate why simp only [h₁] at h₂ fails despite the displayed terms matching, and consider the connection to issue #4613. Done means the reproducer has an explained and tested outcome.