# Zulip Chat Archive

## Stream: general

### Topic: a tactic for copying lemmas when using old_structure_cmd

#### Scott Morrison (Apr 14 2021 at 10:22):

Do we have some automation available for copying lemmas from `X`

to `Y`

, when `Y extends X`

with `old_structure_cmd`

.

#### Scott Morrison (Apr 14 2021 at 10:23):

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 (Apr 14 2021 at 10:25):

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 (Apr 14 2021 at 10:34):

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 (Apr 14 2021 at 10:35):

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

?

#### Eric Wieser (Apr 14 2021 at 10:56):

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

?

#### Eric Wieser (Apr 14 2021 at 10:57):

But then that statement is about `F.to_functor`

not `F`

, so while defeq won't work for rewrites

#### Scott Morrison (Apr 14 2021 at 11:39):

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

.

Last updated: May 13 2021 at 17:42 UTC