a tactic for copying lemmas when using old_structure_cmd

Stream: general

[Scott Morrison]

Do we have some automation available for copying lemmas from X to Y, when Y extends X with old_structure_cmd.

[Scott Morrison]

I'd like to be able to list (or even collect automatically?) lemmas about X, and have corresponding lemmas about Y be built for me.

[Scott Morrison]

At the moment, e.g. with monoidal_functor, we have lots of annoying F.to_functor.map_comp. map_comp isn't a structure field of functor, it's a lemma in terms of the actual field map_comp', so I don't automatically get a version of it for monoidal_functor.

[Mario Carneiro]

It seems like a better solution here would be to register that dot notation should look in the functor namespace for lemmas if monoidal_functor doesn't have it

[Mario Carneiro]

Does the lemma apply if you write functor.map_comp F?

[Eric Wieser]

Doesn't it need to do functor.map_comp F.to_functor?

[Eric Wieser]

But then that statement is about F.to_functor not F, so while defeq won't work for rewrites

[Scott Morrison]

No, it doesn't work with just functor.map_comp F.