no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.258805
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s✝ : Set α
t : Set β
s : Set α
f : Filter α
⊢ map Subtype.val (comap Subtype.val f) = f ⊓ 𝓟 s
rw [map_comap, Subtype.range_coe]