Commit 2024-05-21 04:23 f8b56ceb

feat: simp lemma for coercions in TopCat (#12956) This lemma doesn't have much effect right now in Mathlib, although it makes an example I'm writing for a tutorial go more smoothly. I could add that example in test/ or even doc/ if preferred, but maybe easiest not to? I'm also looking at the simp lemmas around coercions and of in other bundled categories, and hoping to make them more uniform (e.g. coe_of sometimes is and sometimes isn't a simp lemma, mostly according to the vagaries of the porting process, I think!). The equivalent of this lemma in some other bundled categories seems helpful, but I'm still investigating.