chore(LinearAlgebra/DirectSum/TensorProduct): missing lemma

We had the lemma about how the forward direction of this equivalence behaves, but not the reverse direction.

src/linear_algebra/direct_sum/tensor_product.lean

@@ -83,6 +83,12 @@ variables {M₁ M₁' M₂ M₂'}
     direct_sum.lof R (ι₁ × ι₂) (λ i, M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂) (m₁ ⊗ₜ m₂) :=
 by simp [tensor_product.direct_sum]
 
+@[simp] theorem directSum_symm_lof_tmul (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) :
+    (TensorProduct.directSum R M₁ M₂).symm
+      (DirectSum.lof R (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂) (m₁ ⊗ₜ m₂)) =
+      (DirectSum.lof R ι₁ M₁ i₁ m₁ ⊗ₜ DirectSum.lof R ι₂ M₂ i₂ m₂) := by
+  rw [LinearEquiv.symm_apply_eq, directSum_lof_tmul_lof]
+
 @[simp] lemma direct_sum_left_tmul_lof (i : ι₁) (x : M₁ i) (y : M₂') :
   direct_sum_left R M₁ M₂' (direct_sum.lof R _ _ i x ⊗ₜ[R] y)
     = direct_sum.lof R _ _ i (x ⊗ₜ[R] y) :=