chore: forward-port leanprover-community/mathlib3#18616 (#3574)

Author: eric-wieser

Mathlib/LinearAlgebra/TensorProductBasis.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jakob von Raumer
 
 ! This file was ported from Lean 3 source module linear_algebra.tensor_product_basis
-! leanprover-community/mathlib commit 4977fd9da637b6e0a805c1cf460c3a6b8df3f556
+! leanprover-community/mathlib commit f784cc6142443d9ee623a20788c282112c322081
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -54,5 +54,13 @@ theorem Basis.tensorProduct_apply' (b : Basis ι R M) (c : Basis κ R N) (i : ι
     Basis.tensorProduct b c i = b i.1 ⊗ₜ c i.2 := by simp [Basis.tensorProduct]
 #align basis.tensor_product_apply' Basis.tensorProduct_apply'
 
-end CommRing
+-- Porting note: resolved diamond
+set_option synthInstance.etaExperiment true in
+@[simp]
+theorem Basis.tensorProduct_repr_tmul_apply (b : Basis ι R M) (c : Basis κ R N) (m : M) (n : N)
+    (i : ι) (j : κ) :
+    (Basis.tensorProduct b c).repr (m ⊗ₜ n) (i, j) = b.repr m i * c.repr n j := by
+  simp [Basis.tensorProduct]
+#align basis.tensor_product_repr_tmul_apply Basis.tensorProduct_repr_tmul_apply
 
+end CommRing