Dual Right Right To Matrix ρ

lemma dualRightRightToMatrix_ρ (v : (DualRightHandedWeyl ⊗[ℂ] RightHandedWeyl)) (M : SL(2,ℂ)) :    dualRightRightToMatrix (TensorProduct.map (DualRightHandedWeyl.rep M)      (RightHandedWeyl.rep M) v) =    ((M.1⁻¹).conjTranspose) * dualRightRightToMatrix v * (M.1.map star)ᵀ := by  nth_rewrite 1 [dualRightRightToMatrix]  simp only [LinearEquiv.trans_apply]  trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix      (DualRightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis)        (DualRightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis)      (TensorProduct.map (DualRightHandedWeyl.rep M) (RightHandedWeyl.rep M)))      *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))      ((DualRightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis).repr (v))))  · apply congrArg    have h1 := (LinearMap.toMatrix_mulVec_repr      (DualRightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis)      (DualRightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis)      (TensorProduct.map (DualRightHandedWeyl.rep M) (RightHandedWeyl.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 DualRightHandedWeyl.basis DualRightHandedWeyl.basis)          (DualRightHandedWeyl.rep M))        ((LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis)          (RightHandedWeyl.rep M)) (i, j) k)        * dualRightRightToMatrix v k.1 k.2) = _  rw [Fintype.sum_prod_type]  simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]  have h1 : ∑ x : Fin 2, (∑ x1 : Fin 2,      (↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x) * (M.1.map star) j x      = ∑ x : Fin 2, ∑ x1 : Fin 2, ((↑M)⁻¹ᴴ i x1 * dualRightRightToMatrix v x1 x) *      (M.1.map star) j x := by    congr    funext x    rw [Finset.sum_mul]  rw [h1]  rw [Finset.sum_comm]  congr  funext x  congr  funext x1  simp only [DualRightHandedWeyl.rep_toMatrix, RightHandedWeyl.rep_toMatrix]  ring