no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.318879
ι : Sort x
f : α → β
s : Set β
l : Filter α
t : Set β
⊢ t ∈ map f (l ⊓ 𝓟 (f ⁻¹' s)) ↔ t ∈ map f l ⊓ 𝓟 s
simp only [mem_map', mem_inf_principal, mem_setOf_eq, mem_preimage]