no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.259357
ι : Sort x
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m : α → β
m' : β → γ
s : Set α
t : Set β
f : Filter α
U : Set α
h : U ∈ f
W : Set ↑U
W_in : W ∈ comap Subtype.val f
⊢ range Subtype.val ∈ f
simp [h]