Bug in `lift` tactic?

Stream: mathlib4

[David Loeffler]

The following came up in reviewing #23362: when using lift ... with, some auxiliary hypotheses are getting repeatedly copied:

import Mathlib

example {x : WithTop ℤ} (hx : x ≠ ⊤) (h : 0 < x) : False := by
  lift x to ℤ using hx with u hu
  sorry

After the lift, there are not one but two hypotheses in the context stating that 0 < ↑u (inequality in WithTop ℤ), both of them called h. This is probably harmless, but clearly points to something being not quite right.

(There could also be a danger that the extra hypothesis might cause issues with tactics like wlog or induction ... generalizing, where it matters which variables get mentioned in which hypotheses.)

[Vasilii Nesterov]

I investigated this issue and found that the reason for this behavior is that lift calls something like simp [h1] at h2 h2 when rewriting hypotheses:

example (x : Nat) (y : Nat) (h1 : y = x) (h2 : y = 0) : True := by
  simp [h1] at h2 h2
  -- h2✝ h2 : x = 0
  sorry

I would consider this a simp bug. In #23437, I removed the second h2 from the simp call inside lift, so the original issue should now be fixed.