mathlib3

8927a02c - chore(tactic/lift): move a proof to `subtype.exists_pi_extension` (#15098)

chore(tactic/lift): move a proof to `subtype.exists_pi_extension` (#15098) * Move `_can_lift` attr to the bottom of the file, just before the rest of meta code. * Use `ι → Sort*` instead of `Π i : ι, Sort*`. * Move `pi_subtype.can_lift.prf` to a separate lemma.