Commit 2023-03-22 20:21 1b8e1c63

feat: support and improve notation_class in simps (#2883)

• If you write @[simps] for the definition of an AddGroup, it will now generate the correct lemmas for 0, +, nsmul and zsmul using OfNat and heterogenous operations. This is needed for #2609.
  • This is a lot more flexible than the Lean 3 implementation, in order to handle nsmul, zsmul and numerals.
  • It doesn't handle the zpow and npow projections, since their argument order is different than that of HPow.pow (that was likely done for the sake of to_additive, but we can consider to revisit that choice).
• Also fixes the nvMonoid bug encountered in #2609
  • There was an issue where the wrong projection was chosen, since toDiv is a prefix of toDivInvMonoid
  • Before we were checking if _toDiv is a prefix of your projection with _ prepended (e.g. _toDivInvMonoid), now we are checking whether toDiv_ is a prefix of your projection with _ appended (which doesn't match toDivInvMonoid_).