no goals
α : Type u_2
β : Type ?u.101691
β₂ : Type ?u.101694
γ : Type ?u.101697
ι : Sort u_1
ι' : Sort ?u.101703
κ : ι → Sort ?u.101708
κ' : ι' → Sort ?u.101713
inst✝¹ : CompleteLattice α
f✝ g s t : ι → α
a✝ b : α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ (⨆ (x : ι), f x) ⊔ a = ⨆ (x : ι), f x ⊔ a
rw [iSup_sup_eq, iSup_const]