∀ {α : Type u} {ι : Type u_2} [inst : PseudoMetricSpace α] {f₁ f₂ : ι → α} {p : Filter ι} {a : α},
  Filter.Tendsto f₁ p (nhds a) → Filter.Tendsto (fun x => dist (f₁ x) (f₂ x)) p (nhds 0) → Filter.Tendsto f₂ p (nhds a)