Consistent naming scheme in Data/Set/Card

Stream: mathlib4

[metakuntyyy]

Take a look at the following two theorems https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Card.html#Set.InjOn.encard_image and https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Card.html#Set.ncard_image_of_injOn. It would be good if we could have a consistent naming scheme. I barely found the second one.

Or https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Card.html#Function.Injective.encard_image and https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Card.html#Set.ncard_image_of_injective. This is very confusing.

How should we rename those?

[metakuntyyy]

Regarding the first, I'd prefer Set.InjOn.encard_image and the second I'd prefer Function.Injective.encard_image. I think those are nicer to type.

[metakuntyyy]

#34589 opened for the first one.