no goals
X : Type u_1
Y : Type ?u.101522
Z : Type ?u.101525
α : Type u_2
ι : Type ?u.101531
π : ι → Type ?u.101536
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y z : X
s : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → α
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
x : X
l : Filter α
⊢ Tendsto (lift f hf) (𝓝 (mk x)) l ↔ Tendsto f (𝓝 x) l
simp only [← map_mk_nhds, tendsto_map'_iff, lift_comp_mk]