no goals
F : Type ?u.436212
α : Type u_1
β : Type u_2
γ : Type ?u.436221
ι : Type ?u.436224
κ : Type ?u.436227
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
⊢ (⨆ (x : α) (_ : x ∈ s ∪ t), f x) = (⨆ (x : α) (_ : x ∈ s), f x) ⊔ ⨆ (x : α) (_ : x ∈ t), f x
simp [iSup_or, iSup_sup_eq]