mathlib3

c819617b - feat(logic): add plift.down_inj