Commit 2025-03-06 15:01 31cd88d0
View on Github →perf: avoid proofs on rhs of simp lemmas (#22160) Some simp rewrite lemmas create large proof terms, causing significant slowdowns. This fix helps avoid a slowdown in [lean4#6973](https://github.com/leanprover/lean4/pull/6973).