feat(tactic/simps): allow composite projections (#7074)
* Allows custom simps-projections that are compositions of multiple projections. This is useful when extending structures without the `old_structure_cmd`.
* Coercions that are compositions of multiple projections are *not* automatically recognized, and should be declared manually (coercions that are definitionally equal to a single projection are still automatically recognized).
* Custom simps projections should now be declared using the name used by `simps`. E.g. `equiv.simps.symm_apply` instead of `equiv.simps.inv_fun`.
* You can disable a projection `proj` being generated by default by `simps` using `initialize_simps_projections (-proj)`
