Theorem: aux (LeanInRome/S5_Topology/solutions/Solutions_S03_Topological_Spaces.lean)

State before:
X✝ : Type u_1
Y✝ : Type u_2
X : Type u_3
Y : Type u_4
A : Type u_5
inst✝ : TopologicalSpace X
c : A → X
f : A → Y
x : X
F : Filter Y
h : Tendsto f (comap c (𝓝 x)) F
V' : Set Y
V'_in : V' ∈ F
⊢ ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V'
Tactic:
simpa [and_assoc] using ((nhds_basis_opens' x).comap c).tendsto_left_iff.mp h V' V'_in
State after:
no goals