no goals
ι : Sort u_2
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : Directed (fun x x_1 => x ≤ x_1) f
⊢ (a ⊓ ⨆ (i : ι), f i) = ⨆ (i : ι), a ⊓ f i
rw [iSup, h.directedOn_range.inf_sSup_eq, iSup_range]