Commit 2021-04-22 14:56 e5e0ae74
View on Github →chore(data/set/intervals/image_preimage): remove unnecessary add_comm in lemmas (#7276) These lemmas introduce an unexpected flip of the addition, whereas without these lemmas the simplification occurs as you might expect. Since these lemmas aren't otherwise used in mathlib, it seems simplest to just remove them. Let me know if I'm missing something, or some reason to prefer flipping the addition.