Commit 2024-09-05 00:27 77f1a316

refactor: remove simp priority from theorem (#16429) The simplifier used to always unfold the definition of the function List.modifyHead because it had the simp attribute. This behavior hindered the simplifier from using lemmas about the function. To fix this issue, I opened leanprover-community/batteries#790 and it was merged on May 10. Now, the simp priority in the theorem List.modifyHead_modifyHead is no longer needed. leanprover-community/batteries#756 was supposed to remove the priority from it while also moving it from Mathlib to Batteries. But the pull request hasn't been merged for almost five months, hence this PR.