no goals
ι : Sort ?u.94817
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ sSup s ⊓ a = ⨆ (b : α) (_ : b ∈ s), b ⊓ a
simp_rw [@inf_comm _ _ _ a, h.inf_sSup_eq]