exact? doesn't seem to work

Stream: lean4

[A.]

import Mathlib

open scoped Topology

example {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y]
    {f : X → Y} {x : X} {y : Y} : Filter.Tendsto f (𝓝 x) (𝓝 y) → f x = y := by
  exact?

example {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y]
    {f : X → Y} {x : X} {y : Y} : Filter.Tendsto f (𝓝 x) (𝓝 y) → f x = y :=
  eq_of_tendsto_nhds

[A.]

exact? could not close the goal.

[Robin Arnez]

exact? first runs intros; then the goal is f x = y which is too generic for exact? (since it doesn't contain any constants except equality)

[A.]

Oh OK

[Robin Arnez]

In general, tools like loogle.lean-lang.org might be more useful. You can find the same lemma using
@loogle Filter.Tendsto _ (nhds _) (nhds _) -> _ = _

[loogle]

:search: eq_of_tendsto_nhds, IsDenseInducing.extend_eq_at'

[Robin Arnez]

(#loogle Filter.Tendsto _ (nhds _) (nhds _) -> _ = _ within Lean)