Ket Is Prod iff rank eq one

theorem Ket.IsProd_iff_rank_eq_one {d₁ d₂ : Type*} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂]    (ψ : Ket (d₁ × d₂)) :    ψ.IsProd ↔ (Matrix.of (fun i j => ψ (i, j))).rank = 1 := by  rw [ Ket.IsProd_iff_mul_eq_mul ];  constructor;  · intro h;    obtain ⟨ξ, ψ', hξψ'⟩ : ∃ ξ : d₁ → ℂ, ∃ ψ' : d₂ → ℂ, ∀ i j, ψ (i, j) = ξ i * ψ' j := by      -- Let's choose any $j₀$ such that $\psi(i, j₀) \neq 0$ for some $i$.      obtain ⟨j₀, hj₀⟩ : ∃ j₀ : d₂, ∃ i₀ : d₁, ψ (i₀, j₀) ≠ 0 := by        have := ψ.exists_ne_zero;        exact ⟨ this.choose.2, this.choose.1, this.choose_spec ⟩;      choose i₀ hi₀ using hj₀;      exact ⟨ fun i => ψ ( i, j₀ ) / ψ ( i₀, j₀ ), fun j => ψ ( i₀, j ), fun i j => by rw [ div_mul_eq_mul_div, eq_div_iff hi₀ ] ; linear_combination h i i₀ j j₀ ⟩;    -- Since the matrix is a product of two vectors, its rank is 1.    have h_rank : Matrix.rank (Matrix.of (fun i j => ξ i * ψ' j)) ≤ 1 := by      -- The range of the matrix is spanned by the single vector ξ.      have h_range : LinearMap.range (Matrix.mulVecLin (Matrix.of (fun i j => ξ i * ψ' j))) ≤ Submodule.span ℂ {ξ} := by        rintro x ⟨ y, rfl ⟩;        rw [ Submodule.mem_span_singleton ];        exact ⟨ ∑ j, ψ' j * y j, by ext i; simp [ Matrix.mulVec, dotProduct, mul_comm, mul_left_comm, Finset.mul_sum _ _ _ ] ⟩;      exact le_trans ( Submodule.finrank_mono h_range ) ( finrank_span_le_card _ ) |> le_trans <| by norm_num;    cases h_rank.eq_or_lt <;> simp_all [ Matrix.rank, Submodule.eq_bot_iff ];    · convert ‹Module.finrank ℂ ( LinearMap.range ( Matrix.mulVecLin ( Matrix.of fun i j => ξ i * ψ' j ) ) ) = 1› using 3 ; aesop;      · aesop;      · ext; simp [hξψ'];    · have := ψ.exists_ne_zero      simp_all only [ne_eq, mul_eq_zero, not_or, Prod.exists, exists_and_left, exists_and_right]      obtain ⟨left, right⟩ := this      obtain ⟨w, h_2⟩ := left      obtain ⟨w_1, h_3⟩ := right      rename_i h_1      specialize h_1 ( Pi.single w_1 1 )      simp_all [ funext_iff]  · rw [ Matrix.rank ];    rw [ finrank_eq_one_iff' ]    intro a i₁ i₂ j₁ j₂    simp_all only [ne_eq, Subtype.forall, LinearMap.mem_range, Matrix.mulVecBilin_apply, forall_exists_index,      Subtype.exists, Submodule.mk_eq_zero, SetLike.mk_smul_mk, Subtype.mk.injEq, forall_apply_eq_imp_iff,      exists_and_left, exists_prop]    obtain ⟨w, h⟩ := a    obtain ⟨left, right⟩ := h    obtain ⟨left_1, right⟩ := right    obtain ⟨w_1, h⟩ := left_1    subst h    obtain ⟨ c, hc ⟩ := right ( Pi.single j₁ 1 ) ;    obtain ⟨ d, hd ⟩ := right ( Pi.single j₂ 1 ) ;    simp_all only [funext_iff, Matrix.mulVec, Matrix.of_apply, Pi.zero_apply, not_forall,      Pi.smul_apply, smul_eq_mul, Matrix.mulVec_single, MulOpposite.op_one, one_smul,      Matrix.col_apply]    rw [ ← hc i₁, ← hd i₁, ← hc i₂, ← hd i₂ ] ; ring