pass between 𝟙 and ring_hom.id

Stream: Is there code for X?

[Justus Springer]

I would like to have the following rfl-lemmas to let me pass between id and comp for ring homs and the generic id and comp in category-theory.

import algebra.category.CommRing.basic

lemma ring_hom_id_eq_id (R : CommRing) : ring_hom.id R = 𝟙 R := rfl

lemma ring_hom_comp_eq_comp (R S T : CommRing) (f : R ⟶ S) (g : S ⟶ T) :
  ring_hom.comp g f = f ≫ g := rfl

Do these exist? Neither me nor library_search could find them and having to use erw and change all the time is annoying.

[Scott Morrison]

Huh! I guess these may actually be safe, because they will only fire when the sources and targets are bundled objects. It hadn't occurred to me to add these, but I like the prospect!!

[Justus Springer]

Do you think they should be simp-lemmas? I don't even know if I'd prefer one side over the other...

[Bhavik Mehta]

I think they should be simp the other way round - iirc we set up something similar for profinites too, it also has the advantage of applied version being available by simp