Purify spec

@[simp]theorem purify_spec (ρ : MState d) : (pure ρ.purify).traceRight = ρ := by  ext i j  simp_rw [purify, traceRight, HermitianMat.traceRight, Matrix.traceRight]  simp only [Matrix.IsHermitian.eigenvectorUnitary_apply, mat_M, pure_apply,    mat_mk, Matrix.of_apply]  simp only [Ket.apply]  simp only [map_mul]  simp_rw [mul_assoc, mul_comm, ← mul_assoc (Complex.ofReal _), Complex.mul_conj]  -- By definition of eigenvectorUnitary and the properties of the unitary matrix and the eigenvalues, we can show that the matrix constructed from the purification is equal to ρ.  have h_eigenvectorUnitary : ∀ i j, ∑ x, ρ.Hermitian.eigenvectorUnitary i x * ((ρ.Hermitian.eigenvalues x).sqrt ^ 2) * starRingEnd ℂ (ρ.Hermitian.eigenvectorUnitary j x) = ρ.M i j := by    intro i j    have h_eigenvectorUnitary : ρ.M = Matrix.of (fun i j => ∑ x, ρ.Hermitian.eigenvectorUnitary i x * ρ.Hermitian.eigenvalues x * starRingEnd ℂ (ρ.Hermitian.eigenvectorUnitary j x)) := by      have := ρ.Hermitian.spectral_theorem;      convert this using 1;      ext i j; simp [ Matrix.mul_apply, Matrix.diagonal ] ;    replace h_eigenvectorUnitary := congr_fun ( congr_fun h_eigenvectorUnitary i ) j    simp_all only [mat_apply, Matrix.IsHermitian.eigenvectorUnitary_apply, Matrix.of_apply]    congr! 2;    norm_num [ Complex.ext_iff, sq ];    exact Or.inl (Real.mul_self_sqrt (ρ.psd.eigenvalues_nonneg _))  simp_all [ Complex.normSq, sq ];  simpa only [ mul_assoc ] using h_eigenvectorUnitary i j