α β ι : Type u
f : ι → Cardinal
⊢ sum f ≤ sum fun x => iSup f
α β ι : Type u
f : ι → Cardinal
⊢ sum f ≤ lift (#ι) * iSup f
rw [← (iSup f).lift_id, ← lift_umax, lift_umax.{max u v, u}, ← sum_const]
no goals
α β ι : Type u
f : ι → Cardinal
⊢ sum f ≤ sum fun x => iSup f
exact sum_le_sum _ _ (le_ciSup <| bddAbove_range.{u, v} f)