mathlib

fa514687 - feat(tactic/lift): elaborate proof with the expected type (#7739)

feat(tactic/lift): elaborate proof with the expected type (#7739) * also slightly refactor the corresponding function a bit * add some tests * move all tests to `tests/lift.lean`