no goals
α : Type u_1
β : Type u_2
β₂ : Type ?u.138634
γ : Type ?u.138637
ι : Sort ?u.138640
ι' : Sort ?u.138643
κ : ι → Sort ?u.138648
κ' : ι' → Sort ?u.138653
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b✝ : α
f : β → α
b : β
⊢ (⨆ (x : β) (_ : x ∈ {b}), f x) = f b
simp