mathlib3

feat(tactic/lift): prevent `lift` from failing if goal contains the hypothesis used to `lift`

#17869

Open