Duplicate `Subtype.ext_val_iff` in Mathlib

Stream: lean4

[Thomas Zhu]

Both Mathlib.Algebra.Category.Grp.Images and Mathlib.Algebra.Category.ModuleCat.Images have a constant called Subtype.ext_val_iff. They are both introduced by this line:

attribute [local ext] Subtype.ext_val

They are shown in generated documentations for both modules: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/ModuleCat/Images.html and https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/Grp/Images.html, although the former is not (easily?) accessible. (Moreover, it seems neither of them are actually used by the two modules, but that is beside the point).

Is this intended behavior? I think this should be a bug of @[ext]. This problem came up in an extraction of all constants defined in Mathlib, identified by their names.

[Ruben Van de Velde]

Sort of, the attribute is supposed to create an ext_iff lemma

[Yaël Dillies]

but maybe the local attribute shouldn't

[Thomas Zhu]

Yes, here because of this line, even if Mathlib.Algebra.Category.Grp.Images is imported in a separate file, you can still access the lemma Subtype.ext_val_iff:

import Mathlib.Algebra.Category.Grp.Images
#check Subtype.ext_val_iff

[Thomas Zhu]

I guess this still conforms to what the ext attribute description says, but I find it quite weird

[Thomas Zhu]

Also, I don't quite understand why

import Mathlib.Algebra.Category.Grp.Images
import Mathlib.Algebra.Category.ModuleCat.Images

doesn't trigger a name clash ("import failed, environment already contains ...")?

[Kim Morrison]

Identical theorems no longer cause clashes!

[Kim Morrison]

Yaël Dillies said:

but maybe the local attribute shouldn't

This seems like a good idea. Issue or PR welcome?

[Eric Wieser]

Kim Morrison said:

Identical theorems no longer cause clashes!

But are still banned within modules that import each other?

[Kim Morrison]

Sorry, I got this wrong. This is only for (some class of?) automatically generated lemmas.

[Thomas Zhu]

I dug around the code and found the PR that introduces this behavior is lean4#3668

[Thomas Zhu]

Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).

[Yaël Dillies]

Kim Morrison said:

Yaël Dillies said:

but maybe the local attribute shouldn't

This seems like a good idea. Issue or PR welcome?

lean4#5978

[Damiano Testa]

I commented about lean4#3643 on GitHub, but linkfiers do not work there and I'm on mobile!

[Damiano Testa]

Is this a resurgence of the issue or a new one?