theorem aux {X : Type u_3} {Y : Type u_4} {A : Type u_5} [TopologicalSpace X] {c : A → X} {f : A → Y} {x : X} {F : Filter Y} (h : Filter.Tendsto f (Filter.comap c (nhds x)) F) {V' : Set Y} (V'_in : V' ∈ F) : ∃ V ∈ nhds x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V'