fix(linear_algebra/subtype): simplify lifted operations by using projections instead of match
fix(linear_algebra/subtype): simplify lifted operations by using projections instead of match

leanprover-community/mathlib,leanprover-community/mathlib