Choi map inv

@[simp]theorem choi_map_inv (M : MatrixMap A B R) : of_choi_matrix (choi_matrix M) = M := by  -- By definition of `MatrixMap.of_choi_matrix`, we know that applying it to the Choi matrix of `M` reconstructs `M`.  ext X b₁ b₂; simp [MatrixMap.of_choi_matrix, MatrixMap.choi_matrix];  -- By linearity of $M$, we can distribute $M$ over the sum.  have h_linear : M X = ∑ x : A, ∑ x_1 : A, X x x_1 • M (Matrix.single x x_1 1) := by    have h_linear : M X = M (∑ x : A, ∑ x_1 : A, X x x_1 • Matrix.single x x_1 1) := by      congr with i j ; simp ( config := { decide := Bool.true } ) [ Matrix.sum_apply ];      simp ( config := { decide := Bool.true } ) [ Matrix.single ];      rw [ Finset.sum_eq_single i ] <;> aesop;    simp +decide only [h_linear, map_sum, LinearMap.map_smulₛₗ];    simp +zetaDelta at *;  -- By linearity of $M$, we can distribute $M$ over the sum and then apply it to each term.  simp [h_linear, Matrix.sum_apply]