Feat: add isLeast_univ_iff etc (#1549) This is a forward-port of leanprover-community/mathlib#18162
isLeast_univ_iff