Commit 2025-03-31 05:22 65b3f7dc

refactor(MeasureTheory): fix simp not applying measurableSet_inf (#23270) Apparently this theorem is sensitive to the order in which its parameters are given, since it calls typeclass synthesis to find them rather than unification for some reason. In this case, we want m_1 to be found, so we should order it after m_2 which has the same type.