Kron kronecker const

theorem kron_kronecker_const {C : Matrix d d R} (h : C.PosSemidef) {h₁ h₂ : _} : IsCompletelyPositive    (⟨⟨fun M => M ⊗ₖ C, h₁⟩, h₂⟩ : MatrixMap A (A × d) R) := by  intros n x hx  have h_kronecker_pos : (x ⊗ₖ C).PosSemidef := by    -- Since $x$ and $C$ are positive semidefinite, there exist matrices $U$ and $V$ such that $x = U^*U$ and $C = V^*V$.    obtain ⟨U, hU⟩ : ∃ U : Matrix (A × Fin n) (A × Fin n) R, x = star U * U :=      Matrix.posSemidef_iff_eq_conjTranspose_mul_self.mp hx    obtain ⟨V, hV⟩ : ∃ V : Matrix d d R, C = star V * V :=      Matrix.posSemidef_iff_eq_conjTranspose_mul_self.mp h    -- $W = (U \otimes V)^* (U \otimes V)$ is positive semidefinite.    have hW_pos : (U ⊗ₖ V).conjTranspose * (U ⊗ₖ V) = x ⊗ₖ C := by      rw [Matrix.kroneckerMap_conjTranspose, ← Matrix.mul_kronecker_mul]      rw [hU, hV, Matrix.star_eq_conjTranspose, Matrix.star_eq_conjTranspose]    rw [ ← hW_pos ]    exact Matrix.posSemidef_conjTranspose_mul_self (U ⊗ₖ V)  --TODO clean up this mess (but, thanks Aristotle)  convert h_kronecker_pos.submatrix (fun (⟨ ⟨ a, d' ⟩, n' ⟩ : (A × d) × Fin n) => ⟨ ⟨ a, n' ⟩, d' ⟩) using 1;  ext ⟨⟨a, d⟩, n⟩ ⟨⟨a', d'⟩, n'⟩  simp [Matrix.kroneckerMap_apply, Matrix.submatrix_apply]  erw [MatrixMap.kron_def]  simp [Matrix.single, Matrix.kroneckerMap_apply]  simp [Finset.sum_ite, Finset.filter_eq', Finset.filter_and]  rw [ Finset.sum_eq_single a ]  · simp_all only [RingHom.id_apply, ↓reduceIte, Finset.mem_univ, Finset.inter_singleton_of_mem, Finset.sum_singleton]    simp_all only    rw [ Finset.sum_eq_single n ]    · simp_all only [↓reduceIte, Finset.mem_univ, Finset.inter_singleton_of_mem, Finset.sum_singleton]      ring    · intro b a_1 a_2      simp_all only [Finset.mem_univ, ne_eq, ↓reduceIte, Finset.notMem_empty, not_false_eq_true,        Finset.inter_singleton_of_notMem, Finset.sum_empty]    · intro a_1      simp_all only [Finset.mem_univ, not_true_eq_false]  · intro b a_1 a_2    simp_all only [RingHom.id_apply, Finset.mem_univ, ne_eq, ↓reduceIte, Finset.notMem_empty, not_false_eq_true,      Finset.inter_singleton_of_notMem, Finset.sum_empty]  · intro a_1    simp_all only [RingHom.id_apply, Finset.mem_univ, not_true_eq_false]