chore(Algebra/Category): make coe_of a simp lemma in CommGroupCat

[kim-em]

This tried to make the concrete category developments more uniform: whether coe_of was a simp lemma or not seems to have been decided differently in different files during porting.

Also adds some lemmas to improve confluence.