Choi id is PSD

theorem choi_id_is_PSD {A R : Type*} [Fintype A] [DecidableEq A] [RCLike R] :    (MatrixMap.id A R).choi_matrix.PosSemidef := by  -- Let $v$ be the vector with $v_{(a,b)} = \delta_{ab}$.  set v : A × A → R := fun p => if p.1 = p.2 then 1 else 0;  -- By definition of $C$, we know that $C = v v^*$.  have hC : (MatrixMap.id A R).choi_matrix = Matrix.of (fun (i j : A × A) => v i * star (v j)) := by    ext ⟨ i, j ⟩ ⟨ k, l ⟩ ; simp [ MatrixMap.choi_matrix, Matrix.single ] ; aesop;  rw [Matrix.posSemidef_iff_dotProduct_mulVec]  refine' ⟨ _, fun x => _ ⟩;  · ext i j; aesop;  · -- By definition of $v$, we know that $star x ⬝ᵥ v v^* x = |star x ⬝ᵥ v|^2$.    have h_inner : star x ⬝ᵥ (MatrixMap.id A R).choi_matrix.mulVec x = star (star x ⬝ᵥ v) * (star x ⬝ᵥ v) := by      simp [ hC, Matrix.mulVec, dotProduct ];      simp [ Finset.mul_sum, mul_comm, v]      exact Finset.sum_congr rfl fun i hi => by split_ifs <;> simp [ * ] ;    rw [ h_inner, mul_comm ];    exact mul_star_self_nonneg (star x ⬝ᵥ v)