no goals
α : Type u_1
β : Type u_2
β₂ : Type ?u.116340
γ : Type ?u.116343
ι : Sort ?u.116346
ι' : Sort ?u.116349
κ : ι → Sort ?u.116354
κ' : ι' → Sort ?u.116359
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a b : α
f : β → α
p : β → Prop
⊢ (⨆ (i : β), f i) = (⨆ (i : β) (_ : p i), f i) ⊔ ⨆ (i : β) (_ : ¬p i), f i
simpa [Classical.em] using @iSup_union _ _ _ f { i | p i } { i | ¬p i }