no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.255463
ι : Sort x
f f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t : Set β
s : Set (Filter β)
m : α → β
⊢ comap m (sSup s) = ⨆ (f : Filter β) (_ : f ∈ s), comap m f
simp only [sSup_eq_iSup, comap_iSup, eq_self_iff_true]