no goals
α : Type u_2
β : Type u_1
γ : Type ?u.105898
ι : Type ?u.105901
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ (⨅ (i : Set β) (_ : i ∈ f), sSup (u '' id i)) = ⨅ (s : Set β) (_ : s ∈ f), ⨆ (a : β) (_ : a ∈ s), u a
simp only [sSup_image, id]