Theorem: Fintype.elem_le_sup (Logic/Vorspiel/Vorspiel.lean)

State before:
ι : Type u_2
inst✝² : Fintype ι
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ι → α
i : ι
⊢ i ∈ Finset.univ
Tactic:
simp
State after:
no goals