Commit 2026-05-13 15:45 3f909cb6

feat(Logic): declare optional simprocs for commuting equality and iff (#37850) This PR introduces two simprocs eqComm and iffComm that can use @[simp] lemmas on symmetrical forms of an expression: if we have a simp lemma saying f a = b ↔ a = g b and the goal contains b = f a, then we would end up with g b = a. I developed these in #36534. Enabling them globally proved to be quite slow (+0,44% overall build time, which corresponds to +5% simping time), so this PR only declares them (and enables them locally, using e.g. simp [eqComm], when we see that it pays off in the proof).