mathlib

5b29630d - chore(linear_algebra/tensor_product): remove `@[ext]` tag from `tensor_product.mk_compr₂_inj` (#8868)

chore(linear_algebra/tensor_product): remove `@[ext]` tag from `tensor_product.mk_compr₂_inj` (#8868) This PR removes the `@[ext]` tag from `tensor_product.mk_compr₂_inj` and readds it locally only where it is needed. This is a workaround for the issue discussed [in this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/odd.20repeated.20type.20class.20search): basically, when `ext` tries to apply this lemma to linear maps, it fails only after a very long typeclass search. While this problem is already present to some extent in current mathlib, it is exacerbated by the [upcoming generalization of linear maps to semilinear maps](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Semilinear.20maps). In addition to this change, a few individual uses of `ext` have been replaced by a manual application of the relevant ext lemma(s) for performance reasons. For discoverability, the lemma `tensor_product.mk_compr₂_inj` is renamed to `tensor_product.ext` and the former `tensor_product.ext` to `tensor_product.ext'`.