no goals
α : Type u_2
β : Type u_1
β₂ : Type ?u.114350
γ : Type ?u.114353
ι : Sort ?u.114356
ι' : Sort ?u.114359
κ : ι → Sort ?u.114364
κ' : ι' → Sort ?u.114369
inst✝ : CompleteLattice α
f✝ g s✝ t✝ : ι → α
a b : α
f : β → α
s t : Set β
⊢ (⨆ (x : β) (_ : x ∈ s ∪ t), f x) = (⨆ (x : β) (_ : x ∈ s), f x) ⊔ ⨆ (x : β) (_ : x ∈ t), f x
simp_rw [mem_union, iSup_or, iSup_sup_eq]