Making this issue so I don't forget to do this. We have these instances: https://github.com/cs-lean/cslib/blob/0b5679294dbaf83a2a59e172687c88ccc0a5749d/Cslib/Semantics/ReductionSystem/Basic.lean#L46-L57 This was upstreamed in leanprover-community/mathlib4#27240, so we should remove these when updating Mathlib.