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

State before:
ι : Type u_1
inst✝³ : Fintype ι
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : IsEmpty ι
f : ι → α
⊢ sup f = ⊥
Tactic:
simp[sup]
State after:
no goals