feat(set_theory/*) `cardinal.min` → `Inf` (#13410)
We discard `cardinal.min` in favor of `Inf` (the original definition is really just `infi`).
Note: `lift_min'` is renamed to `lift_min`, as the name clash no longer exists. For consistency, `lift_max'` is renamed to `lift_max` and `lift_max` is renamed to `lift_umax_eq`.
