Commit 2024-10-25 08:30 1232423b

chore: re-add @[simp] attribute lost in the port (#18121) This PR re-adds the @[simp] attributes that had a porting note that they could be proved by @[simp], but where that does not appear to be the case currently. Of course, the simp set may have changed sufficiently to require un@[simp]ing some of these anyway, but we should add a more up to date comment in that case.