lift tries to clear variables even where they are still used

[YaelDillies]

When one provides a variable in the using clause of lift, lift tries to clear that variable regardless of whether it is still used in the context or not.

Here is a MWE

import Mathlib.Tactic.Lift

set_option linter.unusedVariables false in
def foo (n : Int) (hn : 0 ≤ n) : Int := n

example (n : Int) (hn : 0 ≤ n) : foo n hn = n := by
  lift n to Nat using hn
/-
tactic 'clear' failed, target depends on 'hn'
case intro
n : Nat
hn : 0 ≤ ↑n
⊢ foo (↑n) hn = ↑n
-/

example (n : Int) (hn : 0 ≤ n) : foo n hn = n := by
  lift n to Nat using id hn -- This works because `id hn` is not a variable
  sorry