lift duplicates a hypothesis

Stream: mathlib4

[Heather Macbeth]

It seems that lift sometimes duplicates a hypothesis rather than replacing it. Is this intended, or -- if it's a bug -- has it been reported? Example:

import Mathlib.Tactic.Lift

example (k : ℕ) (x : ℤ) (h1 : x * k = 0) (h2 : 0 ≤ x * k) : False := by
  lift x * k to ℕ using h2 with z hz
  sorry

The goal state now features a duplication

h1✝ h1: ↑z = 0

Don't know if it's related, but I also noticed this happening in rw, see
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/rw.20duplicates.20a.20hypothesis

[Heather Macbeth]

I opened !4#3000 for this.