How to handle name clashes

Stream: new members

[Gabin Kolly]

I was trying to add new lemmas about equivalences between model structures ModelTheory/Basic.lean, but I realized (because some proofs in other files broke down) that a lot of these lemmas were very similar to results about equivalences between types, and had the same name. For example, I want to prove FirstOrder.Language.Equiv.symm_symm, but then Equiv.symm_symm (the one about equivalences between types) is hidden if you open FirstOrder.Language. What would be the correct way of handling this situation?
I have the impression that the problem here is that the path for Equiv.symm_symm is really just that, and so I cannot give more information to Lean so that it understands that this is really the one I want.

[Gabin Kolly]

Okay, I think that the solution is simply writing _root_.Equiv.nice_lemma when I need to use the lemma about equivalences between types :sweat_smile: