no goals
α : Type u_1
β : Type u_2
β₂ : Type ?u.170514
γ : Type ?u.170517
ι : Sort ?u.170520
ι' : Sort ?u.170523
κ : ι → Sort ?u.170528
κ' : ι' → Sort ?u.170533
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a✝ b a : α
f : β → α
⊢ (⨆ (o : Option β), Option.elim o a f) = a ⊔ ⨆ (b : β), f b
simp [iSup_option]