rewrite doubly defined theorem

Stream: general

[Ashwin Iyengar]

There's a tendsto_nhds in metric_space/basic.lean and a tendsto_nhds in topology/basic.lean. I'm working with a metric space. When I do rw tendsto_nhds, it performs the topology rewrite, but I want it to do the metric space one. Is there a way to choose? This seems like a scope issue.

[Ruben Van de Velde]

Try metric.tendsto_nhds?

[Ashwin Iyengar]

Oh great thanks, I was trying metric_space.tendsto_nhds without looking at what the namespace is called!