no goals
α : Type u_3
β : Type u_2
γ : Type u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
a : α
⊢ Tendsto f (comap e (𝓝 a)) (𝓝 (DenseInducing.extend (_ : DenseInducing e) f a))
simpa only [DenseInducing.extend] using
  tendsto_nhds_limUnder (uniformly_extend_exists h_e ‹_› h_f _)