lift tactic does not respect abbreviations

[jcommelin]

import Mathlib.Tactic.Lift

abbrev MyNat := ℕ

example (n : ℤ) (hn : n ≥ 0) : True := by
  lift n to MyNat using hn
  -- type of `n` is `ℕ` instead of `MyNat`, in the goal state
  trivial

This means that we can not use dot-notation on n for all the juicy decls in the MyNat namespace.

A concrete example of this is LieIdeal K L which is an abbreviation of LieSubmodule K L L.

[mattrobball]

lift seems to explicitly hard code use of Type. How is this being used for universe polymorphic types like LieSubmodule?

[mattrobball]

Similar problem with ENat, WithTop, and Option.

[urkud]

ENat and WithTop aren't abbrevs, so lift shouldn't see through it.

[urkud]

lift seems to explicitly hard code use of Type. How is this being used for universe polymorphic types like LieSubmodule?

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Submonoid/Membership.html#list_prod_mem uses lift but is universe polymorphic