case intro
α β ι : Type u
f : ι → Cardinal
i : ι
⊢ f i ≤ ?m.80685 f
α β ι : Type u
f : ι → Cardinal
⊢ ?m.80685 f ∈ upperBounds (range f)
rintro a ⟨i, rfl⟩
no goals
case intro
α β ι : Type u
f : ι → Cardinal
i : ι
⊢ f i ≤ ?m.80685 f
exact le_sum.{v,u} f i