mathlib

f2b108e8 - refactor(set_theory/cardinal/*): `cardinal.sup` → `supr` (#14569)

refactor(set_theory/cardinal/*): `cardinal.sup` → `supr` (#14569) We remove `cardinal.sup` in favor of `supr`. We tweak many other theorems relating to cardinal suprema in the process. A noteworthy consequence is that there's no longer universe constraints on the domain and codomain of the functions one takes the supremum of. When one does still have this constraint, one can use `bdd_above_range` to immediately prove their range is bounded above. <!-- Lemmas `lift_sup_le`, `lift_sup_le_iff`, `lift_sup_le_lift_sup`, and `lift_sup_le_lift_sup'` have been removed by virtue of being trivial consequences of basic lemmas on suprema and `lift_supr`. --> The result of this PR is the following replacements: * `cardinal.sup` → `supr` * `cardinal.le_sup` → `le_csupr` * `cardinal.sup_le` → `csupr_le'` * `cardinal.sup_le_sup` → `csupr_mono` * `cardinal.sup_le_sum` → `cardinal.supr_le_sum` * `cardinal.sum_le_sup` → `cardinal.sum_le_supr` * `cardinal.sum_le_sup_lift` → `cardinal.sum_le_supr_lift` * `cardinal.sup_eq_zero` → `cardinal.supr_of_empty` * `cardinal.le_sup_iff` → `le_csupr_iff'` * `cardinal.lift_sup` → `cardinal.lift_supr` * `cardinal.lift_sup_le` → `cardinal.lift_supr` + `csupr_le'` * `cardinal.lift_sup_le_iff` → `cardinal.lift_supr` + `csupr_le_iff` * `cardinal.lift_sup_le_lift_sup` → `cardinal.lift_supr` + `csupr_le_iff'` * `cardinal.lift_sup_le_lift_sup'` → `cardinal.lift_supr` + `csupr_mono'` * `cardinal.sup_lt_lift` → `cardinal.supr_lt_lift` * `cardinal.sup_lt` → `cardinal.supr_lt`