Commit 2023-11-07 19:35 c8f6b015
View on Github →chore: remove porting notes about simp [(lemma)] (#8227)
Most (but not all) of these are now fixed, presumably due to the latest lean release.
There is still one porting note that remains, about a (Submonoid.smul_def) that cannot be un-parenthesized.