Grothendieck construction simp attributes

Stream: mathlib4

[joseph hua]

In Mathlib.CategoryTheory.Grothendieck why is Grothendieck.ι marked with @[simps obj map]while other definitions are marked with just @[simps]? I find that the simp lemmas generated for Grothendieck.ι generate really nasty goals for the user, but it does seem to at times shorten simp proofs.

[joseph hua]

I have found that sometimes I want to rewrite (ι F c).map (eqToHom h) using eqToHom_map, but simp will automatically rewrite using ι_map, which produces a nasty goal