α β ι : Type u
f : ι → Cardinal
⊢ sum f ≤ lift (#ι) * iSup f
α β ι : Type u
f : ι → Cardinal
⊢ sum f ≤ (#ι) * iSup f
rw [← lift_id (#ι)]
no goals
α β ι : Type u
f : ι → Cardinal
⊢ sum f ≤ lift (#ι) * iSup f
exact sum_le_iSup_lift f