Came up in [this discussion](https://github.com/leanprover-community/mathlib4/pull/5602#discussion_r1282466562) about #5602