no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.284168
ι : Sort x
e : α ≃ β
f : Filter β
⊢ map (↑e) (map (↑e.symm) f) = map (↑e) (comap (↑e) f)
rw [map_map, e.self_comp_symm, map_id, map_comap_of_surjective e.surjective]