local attribute semireducible on private defs

Stream: general

[Eric Wieser]

I've a lean3 project where I think irreducibility of ring_quot.smul is causing a problem. Unfortunately, it's private so I can't make it locally semireducible (or give a docs link!). import private seems to give me an object that can't be used with local attribute.

Is there any other way to change the reducibility besides forking mathlib3 / breaking the too-late rule?

[Scott Morrison]

Will it be a problem when ported to Lean 4?

[Eric Wieser]

I'm pretty sure the diamond I'm struggling with will still be there in Lean 4. I can certainly debug it there, but in the interest of not having to rewrite bits of my thesis it's easier to stay with lean 3; mathport can't convert latex documents!

[Eric Wieser]

I guess there's the easy option of "make a branch in mathlib3"; I'd forgotten downstream projects can depend on that and still get oleans

[Scott Morrison]

I think we can also be generous with the too-late rule here. You've contributed so much to the porting effort that I think you should feel free to unilaterally ignore the too-late rule, in fact. :-)

[Eric Wieser]

I'll confirm that it actually solves the problem in lean 4 first; it might just reveal more problems...

[Eric Wieser]

It turns out that removing irreducible was the tip of the iceberg: there's also a pile of missing nsmul/nat_cast/zsmul/int_cast fields: #6073