Feature Request: Attribute to map rewrite rules through a functor

[kckennylau]

Zulip discussion: #Is there code for X? > Attribute to map rewrite rules through a functor?

I am requesting an attribute to tag on a lemma of the form

@[map] lemma f_comp_g : f ≫ g = h := sorry

to automatically generate a lemma of the form:

F.map f ≫ F.map g = F.map h

and potentially other similar lemmas (e.g. applying the function for concrete categories).