Ket Is Prod iff mul eq mul

theorem Ket.IsProd_iff_mul_eq_mul (ψ : Ket (d₁ × d₂)) : ψ.IsProd ↔    ∀ i₁ i₂ j₁ j₂, ψ (i₁,j₁)  * ψ (i₂,j₂) = ψ (i₁,j₂) * ψ (i₂,j₁) := by  constructor  · rintro ⟨ξ,φ,rfl⟩ i₁ i₂ j₁ j₂    simp only [prod, apply]    ring_nf  · intro hcrossm    obtain ⟨⟨a, b⟩, hψnonZero⟩ := Ket.exists_ne_zero ψ    -- May be able to simplify proof below by using Ket.normalize    let v₁ : d₁ → ℂ := fun x => ‖ψ (a, b)‖ / (ψ (a, b)) * ((ψ (x, b)) / √(∑ i : d₁, ‖ψ (i, b)‖^2))    let v₂ : d₂ → ℂ := fun y => ψ (a, y) / √(∑ j : d₂, ‖ψ (a, j)‖^2)    have hv1Norm : ∑ x, ‖v₁ x‖^2 = 1 := by      simp only [← Complex.normSq_eq_norm_sq, v₁, Complex.normSq_mul, Complex.normSq_div,      Complex.normSq_ofReal, ← sq]      rw [div_self _]      have hnonneg : ∑ i : d₁, Complex.normSq (ψ (i, b)) ≥ 0 := Fintype.sum_nonneg (fun i => Complex.normSq_nonneg (ψ (i, b)))      · simp_rw [Real.sq_sqrt hnonneg, one_mul, div_eq_inv_mul, ←Finset.mul_sum]        apply inv_mul_cancel₀        by_contra hzero        rw [Fintype.sum_eq_zero_iff_of_nonneg (fun i => Complex.normSq_nonneg (ψ (i, b)))] at hzero        have h₁ : (fun i => Complex.normSq (ψ (i,b))) a ≠ 0 := by simp only [ne_eq, map_eq_zero]; exact hψnonZero        rw [hzero, Pi.zero_apply, ne_eq, eq_self, not_true_eq_false] at h₁        exact h₁      · simp_all only [ne_eq, map_eq_zero, not_false_eq_true]    have hv2Norm : ∑ x, ‖v₂ x‖^2 = 1 := by      simp only [← Complex.normSq_eq_norm_sq, v₂, Complex.normSq_div,      Complex.normSq_ofReal, ← sq]      have hnonneg : ∑ j : d₂, Complex.normSq (ψ (a, j)) ≥ 0 := Fintype.sum_nonneg (fun j => Complex.normSq_nonneg (ψ (a, j)))      simp_rw [Real.sq_sqrt hnonneg, div_eq_inv_mul, ←Finset.mul_sum]      apply inv_mul_cancel₀      by_contra hzero      rw [Fintype.sum_eq_zero_iff_of_nonneg (fun j => Complex.normSq_nonneg (ψ (a, j)))] at hzero      have h₁ : (fun j => Complex.normSq (ψ (a, j))) b ≠ 0 := by simp only [ne_eq, map_eq_zero]; exact hψnonZero      rw [hzero, Pi.zero_apply, ne_eq, eq_self, not_true_eq_false] at h₁      exact h₁    let ψ₁ : Ket d₁ := ⟨v₁, hv1Norm⟩    let ψ₂ : Ket d₂ := ⟨v₂, hv2Norm⟩    use ψ₁, ψ₂    ext ⟨x, y⟩    have hψfun : ψ (x, y) = (ψ (x, b) * ψ (a, y)) / ψ (a, b) := eq_div_of_mul_eq hψnonZero (hcrossm x a y b)    have hψnorm : (∑ z : d₁ × d₂, Complex.normSq (ψ.vec (z.1, b) * ψ.vec (a, z.2))) = Complex.normSq (ψ (a, b)) :=    calc      ∑ z : d₁ × d₂, Complex.normSq (ψ.vec (z.1, b) * ψ.vec (a, z.2)) =        ∑ z : d₁ × d₂, Complex.normSq (ψ.vec (a, b) * ψ.vec (z.1, z.2)) := by simp only [← apply, hcrossm, mul_comm]      _ = ∑ z : d₁ × d₂, Complex.normSq (ψ.vec (a, b)) * Complex.normSq (ψ.vec (z.1, z.2)) := by simp only [Complex.normSq_mul]      _ = Complex.normSq (ψ.vec (a, b)) * ∑ z : d₁ × d₂, Complex.normSq (ψ.vec z) := by rw [←Finset.mul_sum]      _ = Complex.normSq (ψ.vec (a, b)) := by simp only [← apply, ψ.normalized, mul_one]    simp [prod, apply, ψ₁, ψ₂, v₁, v₂]    rw [mul_assoc, ←mul_div_mul_comm, ←Complex.ofReal_mul, ←Real.sqrt_mul (Finset.sum_nonneg _)]    ·      simp_rw [Fintype.sum_mul_sum, ←Fintype.sum_prod_type']      simp only [← Complex.normSq_eq_norm_sq]      simp_rw [Fintype.sum_congr _ _ (fun z : d₁ × d₂ => (Complex.normSq_mul (ψ.vec (z.1, b)) (ψ.vec (a, z.2))).symm)]      simp_rw [hψnorm, Complex.normSq_eq_norm_sq, Real.sqrt_sq_eq_abs, abs_norm, apply]      ring_nf      rw [mul_comm, ←mul_assoc, ←mul_assoc, ←mul_assoc]      nth_rw 2 [←inv_inv (Complex.ofReal (‖ψ.vec (a, b)‖))]      rw [Complex.mul_inv_cancel _]      · rw [one_mul]        ring_nf at hψfun        simp_rw [Ket.apply, mul_comm, mul_comm (ψ.vec (a, y)) _, ←mul_assoc] at hψfun        exact hψfun      · simp_all [Ket.apply]    · simp