feat: port simps

[fpvandoorn]

trafficstars

This is work in progress

Current status:

• initialize_simps_projections has been mostly ported and tested
• documentation is copied from Lean 3, and needs a proofread
• @[simps] has been mostly ported, but still has some missing features/bugs
• Comments about the code are welcome, but note that there it's still WIP

Known missing features:

• Interaction with HMul and friends
• Correct handling with named projections
• Eta doesn't work yet

Lean 4 questions/changes

• CoeFun regression
• There does not seem to be a scoped attribute command (scoped attribute [instance] foo)