Should I add lemmas for more specific types?

Stream: mathlib4

[Jakub Nowak]

I want to create a PR that adds Colorable.of_hom to Mathlib.Combinatorics.SimpleGraph.Coloring. There's already Colorable.of_embedding, but the embedding assumption is unnecessary, just the same proof works for any homomorphism.

I think of two options, and I don't know what is preferred in mathlib?

1. Keep Colorable.of_embedding, and also add Colorable.of_iso for completeness.
2. Deprecate Colorable.of_embedding in favor of Colorable.of_hom.

I only consider the first option as this might make it easier to find the lemma on loogle or with tactics like apply?, but maybe it's unnecessary? My experience is that sometimes I struggled with finding theorem I needed, because it was for more generic type than what I had (e.g. theorem was for embedding while I had an iso).

[Ruben Van de Velde]

I suggest (2)

[Violeta Hernández]

I'm not sure what hom and embedding mean here, but presumably every embedding is trivially a hom? In which case there's no need to have duplicate theorems.

[Jakub Nowak]

Violeta Hernández said:

I'm not sure what hom and embedding mean here, but presumably every embedding is trivially a hom? In which case there's no need to have duplicate theorems.

It's those definitions https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/Maps.html#SimpleGraph.Hom.
Embdedding is coercible to Hom.

[Jakub Nowak]

I've made PR with second option then. https://github.com/leanprover-community/mathlib4/pull/29194