chore(linear_algebra/basic): simplify two proofs (#2123)
* chore(linear_algebra/basic): simplify two proofs
Also drop `linear_map.congr_right` in favor of
`linear_equiv.congr_right`. I'll restore the deleted `congr_right`
as `comp_map : (M₂ →ₗ[R] M₃) →ₗ[R] (M →ₗ[R] M₂) →ₗ[R] (M →ₗ[R] M₃)` soon.
* Fix compile
* Restore `congr_right` under the name `comp_right`.
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
