chore: update mathlib 2024-10-19

[tobiasgrosser]

error: ././././SSA/Projects/Scf/ScfFunctor.lean:491:2: failed to construct new type correct motive for Eq.ndrec while creating splitter/eliminator theorem for ScfFunctor.Scf.instDialectDenoteOfMonadM.match_1

There seems to be a regression in lean? @bollu is this sth worth reporting?

[github-actions[bot]]

Alive Statistics: 87 / 93 (6 failed)

[luisacicolini]

@tobiasgrosser thank you for this! should I continue with the latest update on this branch if this builds?

[tobiasgrosser]

Let's just merge this and create an issue that maybe @bollu or @alexkeizer can help us reduce?

[tobiasgrosser]

@tobiasgrosser thank you for this! should I continue with the latest update on this branch if this builds?

If you could then do another update to the latest version, that would be great.

[tobiasgrosser]

It seems our scaling tests also fail. 😢

[luisacicolini]

do we have any idea why is that? is it something I could look into?

[tobiasgrosser]

This is a significant pain. 😢 Let's discuss with Sid and alex today.

[tobiasgrosser]

I don't think you can debug this effectively.

[github-actions[bot]]

Alive Statistics: 87 / 93 (6 failed)