no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.260618
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t : Set β
f : Filter β
m : α → β
inj : Injective m
large : range m ∈ f
S : Set α
⊢ S ∈ comap m f ↔ m '' S ∈ f
rw [← image_mem_map_iff inj, map_comap_of_mem large]