Pure of constant spectrum

theorem pure_of_constant_spectrum (h : ∃ i, ρ.spectrum = ProbDistribution.constant i) :    ∃ ψ, ρ = pure ψ := by  obtain ⟨i, h'⟩ := h  -- Translate assumption to eigenvalues being (1,0,0,...)  have hEig : ρ.M.H.eigenvalues = fun x => if x = i then 1 else 0 := by    ext x    simp [spectrum, ProbDistribution.constant, ProbDistribution.mk'] at h'    rw [Subtype.mk.injEq] at h'    have h'x := congr_fun h' x    rw [if_congr (Eq.comm) (Eq.refl 1) (Eq.refl 0)]    rw [Prob.ext_iff] at h'x    dsimp at h'x    rw [h'x]    split_ifs    case pos => rfl    case neg => rfl  -- Choose the eigenvector v of ρ with eigenvalue 1 to make ψ  let ⟨u, huUni⟩ := ρ.M.H.eigenvectorUnitary -- Diagonalizing unitary of ρ  let D : Matrix d d ℂ := Matrix.diagonal (RCLike.ofReal ∘ ρ.M.H.eigenvalues) -- Diagonal matrix of ρ  let v : EuclideanSpace ℂ d := ρ.M.H.eigenvectorBasis i  -- Prove v is normalized  have hUvNorm : ∑ x, ‖v x‖^2 = 1 := by    have hinnerv : Inner.inner ℂ v v = 1 := by      have := ρ.M.H.eigenvectorBasis.orthonormal      rw [orthonormal_iff_ite] at this      convert this i i      simp    simp only [PiLp.inner_apply, RCLike.inner_apply, Complex.mul_conj'] at hinnerv    rw [← Fintype.sum_equiv (Equiv.refl d) _ (fun x => (Complex.ofReal ‖v x‖) ^ 2) (fun x => Complex.ofReal_pow ‖v x‖ 2)] at hinnerv    rw [← Complex.ofReal_sum Finset.univ (fun x => ‖v x‖ ^ 2), Complex.ofReal_eq_one] at hinnerv    exact hinnerv  let ψ : Ket d := ⟨v, hUvNorm⟩ -- Construct ψ  use ψ  ext j k  -- Use spectral theorem to prove that ρ = pure ψ  rw [Matrix.IsHermitian.spectral_theorem ρ.M.H, Unitary.conjStarAlgAut_apply, Matrix.mul_apply]  simp [ψ, v, hEig]  have hsum : ∀ x ∈ Finset.univ, x ∉ ({i} : Finset d) → (ρ.M.H.eigenvectorBasis x j) * (↑(if x = i then 1 else 0) : ℝ) * (starRingEnd ℂ) (ρ.Hermitian.eigenvectorBasis x k) = 0 := by    intros x hx hxnoti    rw [Finset.mem_singleton] at hxnoti    rw [if_neg hxnoti, Complex.ofReal_zero]    ring  simp_rw [←Finset.sum_subset (Finset.subset_univ {i}) hsum, Finset.sum_singleton, reduceIte, Complex.ofReal_one, mul_one]  rfl