Commit 2023-05-16 18:39 46235134
View on Github →chore: forward-port mathlib#18554 (#3982) Match [#18554](https://github.com/leanprover-community/mathlib/pull/18554)
chore: forward-port mathlib#18554 (#3982) Match [#18554](https://github.com/leanprover-community/mathlib/pull/18554)