SetLike.coe_set_eq

Stream: mathlib4

[Kenny Lau]

SetLike.coe_set_eq:

{A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A} : ↑p = ↑q ↔ p = q

Should we name this SetLike.coe_inj instead? I had a hard time discovering this. (Again, discoverability issues)

[Kenny Lau]

DFunLike.coe_fn_eq also

[Robin Arnez]

Yeah, coe_set_eq sounds like a bad name. The first thing I would've thought of there would be ↑(_ : Set _) = _ which is totally different to what it really is. Also, the declaration being talked about (docs#SetLike.coe) is already in the same namespace and no parameter (not even an implicit one) is Set _ in the applications of docs#SetLike.coe in the theorem statement, so the _set part is also unnecessary and confusing. coe_inj is in this case non-ambiguous though (again since the coe declaration is in the same namespace) and follows the naming convention well so yeah it would probably make sense to change.

[Kevin Buzzard]

FWIW I had a hard time today trying to find Units.coe_inj until I discovered that it was docs#Units.val_inj

[Kenny Lau]

that trips me up too, because val sounds too much like Subtype.val which is sometimes coe in names