Spectrum pure eq constant

theorem spectrum_pure_eq_constant :    ∃ i, (pure ψ).spectrum = ProbDistribution.constant i := by  let ρ := pure ψ  -- Prove 1 is in the spectrum of pure ψ by exhibiting an eigenvector with value 1.  have : ∃i, (pure ψ).spectrum i = 1 := by    simp [spectrum, ProbDistribution.mk']    have hEig : ∃i, (pure ψ).M.H.eigenvalues i = 1 := by      -- Prove ψ is an eigenvector of ρ = pure ψ      have hv : ρ.M *ᵥ ψ = ψ := by        ext        simp_rw [ρ, pure, Matrix.mulVec, mat, Matrix.vecMulVec_apply, dotProduct,        Bra.apply', Ket.apply, mul_assoc, ← Finset.mul_sum, ← Complex.normSq_eq_conj_mul_self,        ← Complex.ofReal_sum, ← Ket.apply, ψ.normalized, Complex.ofReal_one, mul_one]      let U : Matrix.unitaryGroup d ℂ := star ρ.M.H.eigenvectorUnitary -- Diagonalizing unitary of ρ      let w : d → ℂ := U *ᵥ ψ      -- Prove w = U ψ is an eigenvector of the diagonalized matrix of ρ = pure ψ      have hDiag : Matrix.diagonal (RCLike.ofReal ∘ ρ.M.H.eigenvalues) *ᵥ w = w := by        simp_rw [← Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary,        eq_comm, Unitary.conjStarAlgAut_apply,        ← Matrix.mulVec_mulVec, w, U, Matrix.mulVec_mulVec] -- Uses spectral theorem        simp_all        rw [←Matrix.mulVec_mulVec, hv]      -- Prove w = U ψ is nonzero by contradiction      have hwNonZero : ∃j, w j ≠ 0 := by        by_contra hwZero        simp at hwZero        rw [←funext_iff] at hwZero        -- If w is zero, then ψ is zero, since U is invertible        have hψZero : ∀x, ψ x = 0 := by          apply congr_fun          -- Prove U is invertible          have hUdetNonZero : (U : Matrix d d ℂ).det ≠ 0 := by            by_contra hDetZero            obtain ⟨u, huUni⟩ := U            have h0uni: 0 ∈ unitary ℂ := by              rw [←hDetZero]              simp              exact Matrix.det_of_mem_unitary huUni            rw [Unitary.mem_iff] at h0uni            simp_all          exact Matrix.eq_zero_of_mulVec_eq_zero hUdetNonZero hwZero        -- Reach an contradiction that ψ has norm 0        have hψn := Ket.normalized ψ        have hnormZero : ∀ x : d, Complex.normSq (ψ x) = 0 := fun x => by          rw [hψZero x, Complex.normSq_zero]        have hsumZero : ∑ x : d, Complex.normSq (ψ x) = 0 := by          apply Finset.sum_eq_zero          intros x _          exact hnormZero x        simp_all      obtain ⟨j, hwNonZero'⟩ := hwNonZero      have hDiagj := congr_fun hDiag j      rw [Matrix.mulVec_diagonal, mul_eq_right₀ hwNonZero'] at hDiagj      use j      simp_all    obtain ⟨i, hEig'⟩ := hEig    use i    ext    exact hEig'  --If 1 is in a distribution, the distribution is a constant.  obtain ⟨i, hi⟩ := this  use i  exact ProbDistribution.constant_of_exists_one hi