mathlib

mathlib copied to clipboard

The @[elementwise] attribute creates a copy of a category-theory lemma which essentially applies (forget C).map to both sides of an equation, then applies it to an arbitrary element.

This gives an equation where each morphism has been replaced with its coercion to a function.

Unfortunately, if we then happen to specialize from C to Type, we get a lemma we can't rewrite by, because it has superfluous coercions in it.

I can't think of a fix besides generating both an _apply lemma and an _apply_in_Type lemma separately. This would require some rearranging of the internals of elementwise, so I'm not going to do it now.

(Discovered in #7092.)