get a specific lemma out of several with the same name

Stream: general

[Rémy Degenne]

The proof I am currently editing is inside the nnreal namespace. I want to use inv_mul_cancel for a real argument, but nnreal.inv_mul_cancel exists as well and is the lemma that lean tries to apply when I write inv_mul_cancel. How do I use the non-nnreal lemma?

[Riccardo Brasca]

You can try _root_.inv_mul_cancel

[Rémy Degenne]

thanks, it worked.

[Riccardo Brasca]

It just means "do not put anything before ..