mathlib3

9f19686c - feat(logic/small): generalize + golf (#14584)

feat(logic/small): generalize + golf (#14584) This PR does the following: - add a lemma `small_lift` - generalize the lemma `small_ulift` - golf `small_self` and `small_max`