no goals
α : Type u_1
β : Type u_2
β₂ : Type ?u.111941
γ : Type ?u.111944
ι : Sort ?u.111947
ι' : Sort ?u.111950
κ : ι → Sort ?u.111955
κ' : ι' → Sort ?u.111960
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : β → α
⊢ (⨆ (x : β) (_ : x ∈ ∅), f x) = ⊥
simp