issue !4#11039: Porting note: broken proof was

Stream: triage

[Random Issue Bot]

Today I chose issue 11039 for discussion!

Porting note: broken proof was
Created by @Pietro Monticone (@pitmonticone) on 2024-02-28
Labels: porting-notes

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue 11039 for discussion!

Porting note: broken proof was
Created by @Pietro Monticone (@pitmonticone) on 2024-02-28
Labels: porting-notes

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue #11039 for discussion!

Porting note: broken proof was
Created by @Pietro Monticone (@pitmonticone) on 2024-02-28
Labels: porting-notes

Is this issue still relevant? Any recent updates? Anyone making progress?

[Violeta Hernández]

This seems to be localized to some representation theory files, perhaps someone knowledgeable can perform some cleanup?

[Johan Commelin]

I took a look at this, but the problems seem to be quite intricate. Partial progress at #22712
One of the issues seems to be that the cartesian monoidal structure on Type is sometimes used, and sometimes it is just \prod (ie $\times$), and now the two don't match up without erw...