mathlib bump

Stream: Infinity-Cosmos

[Kevin Buzzard]

Just flagging this one-line PR which caused a huge speed-up in mathlib's homotopy category theory files: https://github.com/leanprover-community/mathlib4/pull/21329#issuecomment-2629108863

If this affects your work here, you might want to bump mathlib :-)

[Nick Ward]

@Kevin Buzzard do you happen to know where I could learn more about this "unfavourable discrimination tree key"?

[Nick Ward]

Nevermind, I have found your explanation in the "bad simp discrimination tree keys" channel. Thanks!

[Kevin Buzzard]

I wish I understood it better myself. I think the idea is that even though the lemma in question looks naively like a good simp lemma in the sense that the RHS is simpler than the LHS, it turns out to be hugely disruptive to add it to the simp set because it always looks like it might apply but basically never works and it's costly to check