mathlib

aad14108 - refactor(linear_algebra/tensor_product): make `lift f (mk m n) = f m n` true by `rfl`