`simp` unable to rewrite seemingly identical terms

[zhengyao-lin]

Prerequisites

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

• [X] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [X] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [X] 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

[Kha]

Yes, if you add set_option pp.all true, the context is

h₁ : @Eq.{1} Nat (@f.z.{0, u_1} Nat x) (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))
w : Nat
h₂ : @Eq.{1} Nat (@f.z.{0, ?u.123} Nat x) w

I don't think simp should let h1 instantiate the mvar of h2 here so this is likely working as intended, though the error message could be improved

[zhengyao-lin]

Thanks for the confirmation! Is there a reason why z has to capture the unused universe?