Alignment not firing

Stream: mathlib4

[Patrick Massot]

Despite https://github.com/leanprover-community/mathlib4/blob/c8da4dbf7ff19167b9e9b2c268b187f0494ef4c5/Mathlib/Logic/Function/Basic.lean#L82, the name isn't aligned at in unop_injective.Ne https://github.com/leanprover-community/mathlib3port/blob/25aba9a00dd0c7af7df362a275829ce34ac8dd48/Mathbin/Algebra/Ring/Opposite.lean#L92. Is this a known issue because of dot notation?

[Chris Hughes]

I've seen this a lot

[Kevin Buzzard]

Yes I've seen this quite a bit too. My memory is that Mario just said that the autoporter didn't have enough information so we had to just fix this stuff manually.

[Mario Carneiro]

yes, there is no easy fix. If it becomes a sufficiently high priority I can try for the hard fix though

[Floris van Doorn]

I think it's quite high priority, it happens quite a lot.

Luckily there is a workaround that is not too bad. If you see (someDef : SomeType).some_lemma you can search all files / grep for SomeType.some_lemma, and you'll likely find the #align SomeType.some_lemma SomeType.some_other_lemma_name line.

[Chris Hughes]

Align seems to have a lot of problems with namespaces. I was porting a file with a lot of lemmas starting with equiv.set and in the Mathlib3port file when the Equiv namespace was open, all the lemmas that started equiv.set, and referred to as set._ because the equiv namespace was open were still set._ with uncapitalised set.

[Chris Hughes]

To be honest, I'm not sure align fires at all on lemmas inside a namespace when they're referred to without the namespace because the namespace is open.