no goals
α : Type u_2
β : Type u_1
γ : Type ?u.415578
inst✝ : PseudoEMetricSpace α
l : Filter β
f : β → α
y : α
⊢ Tendsto f l (𝓝 y) ↔ Tendsto (fun x => edist (f x) y) l (𝓝 0)
simp only [EMetric.nhds_basis_eball.tendsto_right_iff, EMetric.mem_ball,
  @tendsto_order ℝ≥0∞ β _ _, forall_prop_of_false ENNReal.not_lt_zero, forall_const, true_and_iff]