refactor: Add Contractions in terms of representations

[jstoobysmith]

Add contraction of Lorentz vectors and covectors in terms of representations. This replaces #1221.

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[morrison-daniel]

Generally looks good but I got a little cleanup. I like to avoid grind when I can because it can be a performance hit and it obfuscates the actual proof steps if used too liberally. Usually it can be replaced by less expensive tactics. Also, I think it may be helpful to write some of this in terms of more general objects like MulAction and BilinMap which would help deal with some of the linearity problems. Not necessary to add here, but something to consider for future PRs.

[jstoobysmith]

The reason I'm using rep here rather then MulAction is because it will create a future diamond if MulAction is used. Applied your suggestions here.

-awaiting-author