chore(category_theory/monoidal): golf some proofs (#6894)
Golfs proofs of `tensor_left_iff`, `tensor_right_iff`, `left_unitor_tensor'`, `right_unitor_tensor` and `unitors_equal` - in particular removes the file `monoidal/unitors` as all it contained was a proof of `unitors_equal` which is a two line proof.
