Pure iff rank eq one

theorem pure_iff_rank_eq_one {d : Type*} [Fintype d] [DecidableEq d] (ρ : MState d) :    (∃ ψ, ρ = pure ψ) ↔ ρ.m.rank = 1 := by  constructor <;> intro h;  · obtain ⟨w, rfl⟩ := h    -- The rank of the outer product of a vector with itself is 1.    have h_rank : ∀ (v : d → ℂ), v ≠ 0 → Matrix.rank (Matrix.vecMulVec v (conj v)) = 1 := by      intro v hv_ne_zero      have h_outer_product : ∀ (u : d → ℂ), ∃ (c : ℂ), Matrix.mulVec (Matrix.vecMulVec v (conj v)) u = c • v := by        intro u        use ∑ i, (starRingEnd ℂ (v i)) * (u i);        ext i; simp [ Matrix.vecMulVec, Matrix.mulVec, dotProduct, mul_comm, mul_left_comm, Finset.mul_sum _ _ _ ] ;      apply le_antisymm      · have h_outer_product : LinearMap.range (Matrix.mulVecLin (Matrix.vecMulVec v (conj v))) ≤ Submodule.span ℂ {v} := by          rintro x ⟨ u, rfl ⟩ ; obtain ⟨ c, hc ⟩ := h_outer_product u; aesop;        exact le_trans ( Submodule.finrank_mono h_outer_product ) ( finrank_span_le_card _ ) |> le_trans <| by simp ;      · contrapose! hv_ne_zero; simp_all [ Matrix.rank, Submodule.eq_bot_iff ] ;        ext i; specialize hv_ne_zero ( Pi.single i 1 ) ; simp_all [ Matrix.vecMulVec ] ;        simpa using congr_fun hv_ne_zero i;    exact h_rank _ ( fun h => by simpa [ h ] using w.exists_ne_zero );  · -- Since ρ is Hermitian and has rank 1, it must be of the form |ψ⟩⟨ψ| for some ket ψ.    obtain ⟨ψ, hψ⟩ : ∃ ψ : d → ℂ, ρ.m = Matrix.of (fun i j => ψ i * star (ψ j)) := by      -- Since ρ is Hermitian and has rank 1, it must be of the form |ψ⟩⟨ψ| for some ket ψ. Use this fact.      have h_pure : ∃ ψ : d → ℂ, ρ.m = Matrix.of (fun i j => ψ i * star (ψ j)) := by        have h_rank : ρ.m.rank = 1 := h        have h_herm : ρ.m.IsHermitian := by          exact ρ.M.property        have := h_herm.spectral_theorem;        -- Since the rank of ρ.m is 1, the diagonal matrix in the spectral theorem must have exactly one non-zero entry.        obtain ⟨i, hi⟩ : ∃ i : d, h_herm.eigenvalues i ≠ 0 ∧ ∀ j : d, j ≠ i → h_herm.eigenvalues j = 0 := by          have h_diag : ∑ i : d, (if h_herm.eigenvalues i = 0 then 0 else 1) = 1 := by            have h_diag : Matrix.rank (Matrix.diagonal (h_herm.eigenvalues)) = 1 := by              have h_diag : Matrix.rank (Matrix.diagonal (h_herm.eigenvalues)) = Matrix.rank (ρ.m) := by                exact Eq.symm (Matrix.IsHermitian.rank_eq_rank_diagonal h_herm);              exact h_diag.trans h_rank;            rw [ Matrix.rank_diagonal ] at h_diag;            simp [ Finset.sum_ite ];            rw [ Fintype.card_subtype ] at h_diag ; exact h_diag;          obtain ⟨i, hi⟩ : ∃ i : d, h_herm.eigenvalues i ≠ 0 := by            exact not_forall.mp fun h => by simp [ h ] at h_diag;          rw [ Finset.sum_eq_add_sum_diff_singleton ( Finset.mem_univ i ) ] at h_diag;          exact ⟨ i, hi, fun j hj => Classical.not_not.1 fun hj' => absurd h_diag ( by rw [ if_neg hi ] ; exact ne_of_gt ( lt_add_of_pos_right _ ( lt_of_lt_of_le ( by simp [ hj' ] ) ( Finset.single_le_sum ( fun x _ => by positivity ) ( Finset.mem_sdiff.2 ⟨ Finset.mem_univ j, by simp [ hj ] ⟩ ) ) ) ) ) ⟩;        -- Since the diagonal matrix in the spectral theorem has exactly one non-zero entry, we can write ρ.m as |ψ⟩⟨ψ| for some ket ψ.        use fun j => (h_herm.eigenvectorUnitary : Matrix d d ℂ) j i * Real.sqrt (h_herm.eigenvalues i);        convert this using 1        ext j k; simp [ Matrix.mul_apply, Matrix.diagonal ]        ring_nf        rw [ Finset.sum_eq_single i ] <;> simp +contextual [ hi ];        exact Or.inl <| Or.inl <| mod_cast Real.sq_sqrt <| by          have := ρ.psd.eigenvalues_nonneg i;          exact this      exact h_pure;    have h_norm : ∑ x, Complex.normSq (ψ x) = 1 := by      have := ρ.tr';      simp_all [ Complex.ext_iff, Matrix.trace ];      simpa only [ Complex.normSq_apply, mul_comm ] using this.1;    use ⟨ψ, by      simpa [ Complex.normSq_eq_norm_sq ] using h_norm⟩    generalize_proofs at *;    refine' MState.ext_m _ ; aesop