feat(set_theory/cardinal): sum_le_sup_lift (#12513)

This is a universe-polymorphic version of `sum_le_sup`.

Author: vihdzp

src/set_theory/cardinal.lean

@@ -622,6 +622,13 @@ sup_le.2 $ le_sum _
 theorem sum_le_sup {ι : Type u} (f : ι → cardinal.{u}) : sum f ≤ #ι * sup.{u u} f :=
 by rw ← sum_const'; exact sum_le_sum _ _ (le_sup _)
 
+theorem sum_le_sup_lift {ι : Type u} (f : ι → cardinal.{max u v}) :
+  sum f ≤ (#ι).lift * sup.{u v} f :=
+begin
+  rw [←(sup f).lift_id, ←lift_umax, lift_umax.{(max u v) u}, ←sum_const],
+  exact sum_le_sum _ _ (le_sup _)
+end
+
 theorem sup_eq_zero {ι} {f : ι → cardinal} [is_empty ι] : sup f = 0 :=
 by { rw [← nonpos_iff_eq_zero, sup_le], exact is_empty_elim }