[Merged by Bors] - chore(linear_algebra/tensor_product): remove @[ext] tag from tensor_product.mk_compr₂_inj

[dupuisf]

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: 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.

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'.

---

[eric-wieser]

Can we fix this by adjusting the priority instead?

Or perhaps by locally removing the attribute where it causes timeouts?

I don't really like the idea of removing this ext lemma (which for reference was added in #6105), because the chance of someone who needs it finding it is very small.

[dupuisf]

Can we fix this by adjusting the priority instead?

Or perhaps by locally removing the attribute where it causes timeouts?

I don't really like the idea of removing this ext lemma, because the chance of someone who needs it finding it is very small.

I guess that could be another option, but my concern is that it seems to cause performance problems in fairly generic situations (i.e. calling ext on a linear map) -- this might also be hard to debug for someone who is not aware of the issue. Maybe we could rename the lemma to tensor_product.ext to make it easier to find?

[eric-wieser]

I wonder if replacing [] binders with {} binders in mk_compr₂_inj would speed things up? The statement is currently

theorem tensor_product.mk_compr₂_inj {R : Type u_1} [comm_semiring R] {M : Type u_4} {N : Type u_5} {P : Type u_6}
  [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P]
  {g h : M ⊗ N →ₗ[R] P} (H : (tensor_product.mk R M N).compr₂ g = (tensor_product.mk R M N).compr₂ h) :
g = h

but perhaps it would be faster as

theorem tensor_product.mk_compr₂_inj {R : Type u_1} {_ : comm_semiring R} {M : Type u_4} {N : Type u_5} {P : Type u_6}
  {add_comm_monoid M : _} {add_comm_monoid N : _} {add_comm_monoid P : _} {_ : module R M} {_ : module R N} {_ : module R P}
  {g h : M ⊗ N →ₗ[R] P} (H : (tensor_product.mk R M N).compr₂ g = (tensor_product.mk R M N).compr₂ h) :
g = h

I think it would be worth creating a Zulip thread about the performance here to see if anyone can work out the underlying cause. Edit: I posted in the zulip thread.

[dupuisf]

I wonder if replacing [] binders with {} binders in mk_compr₂_inj would speed things up?

I actually tried that first :-) It made no difference on the compile time.

[dupuisf]

I have now renamed tensor_product.mk_compr₂_inj to tensor_product.ext and the former tensor_product.ext to tensor_product.ext'.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests