Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
This forward-ports the revert (leanprover-community/mathlib#19230) of changes that were never forward-ported (leanprover-community/mathlib#19153). Therefore only the SHA needs updating.
- Loading branch information