Left Dual Left To Matrix ρ

lemma leftDualLeftToMatrix_ρ (v : (LeftHandedWeyl ⊗[ℂ] DualLeftHandedWeyl)) (M : SL(2,ℂ)) :    leftDualLeftToMatrix (TensorProduct.map (LeftHandedWeyl.rep M) (DualLeftHandedWeyl.rep M) v) =    M.1 * leftDualLeftToMatrix v * (M.1⁻¹) := by  nth_rewrite 1 [leftDualLeftToMatrix]  simp only [LinearEquiv.trans_apply]  trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix      (LeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis)        (LeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis)      (TensorProduct.map (LeftHandedWeyl.rep M) (DualLeftHandedWeyl.rep M)))      *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))      ((LeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis).repr (v))))  · apply congrArg    have h1 := (LinearMap.toMatrix_mulVec_repr (LeftHandedWeyl.basis.tensorProduct        DualLeftHandedWeyl.basis)      (LeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis)      (TensorProduct.map (LeftHandedWeyl.rep M) (DualLeftHandedWeyl.rep M)) v)    simp only [coe_linearEquivFunOnFinite]    rw [h1]  rw [TensorProduct.toMatrix_map]  funext i j  change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)        ((LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis) (LeftHandedWeyl.rep M))        ((LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis)          (DualLeftHandedWeyl.rep M)) (i, j) k)        * leftDualLeftToMatrix v k.1 k.2) = _  rw [Fintype.sum_prod_type]  simp_rw [kroneckerMap_apply, Matrix.mul_apply]  have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2, M.1 i x1 * leftDualLeftToMatrix v x1 x) * (M.1⁻¹) x j    = ∑ x : Fin 2, ∑ x1 : Fin 2, (M.1 i x1 * leftDualLeftToMatrix v x1 x) * (M.1⁻¹) x j := by    congr    funext x    rw [Finset.sum_mul]  rw [h1]  rw [Finset.sum_comm]  congr  funext x  congr  funext x1  simp only [LeftHandedWeyl.rep_toMatrix, DualLeftHandedWeyl.rep_toMatrix, transpose_apply]  ring