no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.224114
ι : Sort x
f : α → β
l : Filter β
p : α → Prop
s : Set α
x✝ : s ∈ comap f l
t : Set β
ht : t ∈ l
hts : f ⁻¹' t ⊆ s
y : β
hy : y ∈ t
x : α
hx : f x = y
⊢ f x ∈ t
rwa [hx]