mathlib3

2bd4bb69 - fix(tactic/lift): elaborate the type better (#7598)

fix(tactic/lift): elaborate the type better (#7598) * When writing `lift x to t` it will now elaborating `t` using that `t` must be a sort (inserting a coercion if needed). * Generalize `Type*` to `Sort*` in the tactic