mathlib3

c8ab806e - feat(tactic/alias.lean): use current namespace in alias (#14961)

feat(tactic/alias.lean): use current namespace in alias (#14961) This makes `alias foo <- bar` use the current namespace to resolve the new alias name `bar`, for consistency with `def bar := foo` and leanprover-community/mathlib4#293.