no goals
α : Type u_2
β : Type ?u.103547
β₂ : Type ?u.103550
γ : Type ?u.103553
ι : Sort u_1
ι' : Sort ?u.103559
κ : ι → Sort ?u.103564
κ' : ι' → Sort ?u.103569
inst✝ : CompleteLattice α
f✝ g s t : ι → α
a✝ b : α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
⊢ (a ⊔ ⨆ (i : ι) (h : p i), f i h) = ⨆ (i : ι) (h : p i), a ⊔ f i h
simpa only [sup_comm] using @biSup_sup α _ _ p _ _ h