Of Fintype

theorem of_Fintype  {M : MatrixMap A B R} (h : IsCompletelyPositive M)    (T : Type*) [Fintype T] [DecidableEq T] :    (M.kron (LinearMap.id : MatrixMap T T R)).IsPositive := by  obtain ⟨n, ⟨e⟩⟩ : ∃ n : ℕ, Nonempty (T ≃ Fin n) :=    Finite.exists_equiv_fin T  convert h n using 1  have h_submatrix : (M ⊗ₖₘ (LinearMap.id : MatrixMap T T R)) = (MatrixMap.submatrix R (fun p : B × T => (p.1, e p.2)) ∘ₗ (M ⊗ₖₘ (LinearMap.id : MatrixMap (Fin n) (Fin n) R)) ∘ₗ MatrixMap.submatrix R (fun p : A × Fin n => (p.1, e.symm p.2))) := by    ext    simp only [submatrix, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,      Matrix.submatrix_apply]    rw [MatrixMap.kron_def, MatrixMap.kron_def]    simp only [Matrix.single, LinearMap.id_coe, id_eq, Matrix.of_apply, mul_ite, mul_one, mul_zero,      ite_mul, zero_mul, Matrix.submatrix];    congr! 4    rw [← Equiv.sum_comp e]    congr! 2    rw [← Equiv.sum_comp e]    simp only [EmbeddingLike.apply_eq_iff_eq, Equiv.symm_apply_apply]  constructor  · intro h₂    simp [MatrixMap.IsPositive]    exact h n  · intro h x hx    specialize h (hx.submatrix (fun p : A × Fin n => (p.1, e.symm p.2)))    rw [h_submatrix]    simp only [LinearMap.coe_comp, Function.comp_apply, submatrix_apply]    exact h.submatrix _