open `bar` in namespace `foo` when `foo.bar` exists

Stream: lean4

[Kevin Buzzard]

What's the trick to give me access to lemma2 within the foo namespace?

namespace foo

namespace bar

theorem lemma1 : 2+2=4 := rfl

end bar

end foo

namespace bar

theorem lemma2 : 3+3=6 := rfl

end bar

namespace foo

open bar

#check lemma1 -- fine
#check lemma2 -- not fine

open _root_.bar -- no

-- gaargh

end foo

In the real world example !4#4522 , foo := AlgebraicGeometry and bar := PrimeSpectrum. Is the only option to open bar before namespace foo?

[Michael Stoll]

That probably won't work when there is also bar.foo ...

[Adam Topaz]

The only way I could find to do this is the ridiculous

end foo open bar namespace foo open bar

instead of open bar on line 19 :-/

[Adam Topaz]

How common in this in practice?

[Adam Topaz]

Presumably it's not too common, and using bar.lemma2 would be reasonable?

[James Gallicchio]

I'm surprised open _root_.bar doesn't work. That might be a bug, since I think it is intended to work.

[Mario Carneiro]

open _root_.bar is a late lean 3 addition, it might need to be added to lean 4 as well

[Kevin Buzzard]

How common is this in practice?

If you look at the diff (autoporter v HEAD) in the PR I linked to you'll see that PrimeSpectrum.lemma2 is all over it :-( Somehow solving the problem now would mean that Jujian has to revert a bunch of changes but maybe in the long term that's ok ...