Is Trace Preserving iff trace choi

theorem IsTracePreserving_iff_trace_choi [DecidableEq A] (M : MatrixMap A B R) : M.IsTracePreserving    ↔ M.choi_matrix.traceLeft = 1 := by  constructor  · intro h    ext a₁ a₂    replace h := h (Matrix.single a₁ a₂ 1)    simp_rw [Matrix.trace, Matrix.diag] at h    simp only [Matrix.traceLeft, choi_matrix, Matrix.of_apply, h]    simp only [Matrix.single, Matrix.of_apply, Finset.sum_boole, Matrix.one_apply]    have : (fun x => a₁ = x ∧ a₂ = x) = (fun x => a₁ = a₂ ∧ a₂ = x) := by      funext x      rw [eq_iff_iff, and_congr_left_iff]      rintro rfl      trivial    split_ifs with h    <;> simp [this, h, Finset.filter_eq]  · intro h X    replace h := fun (a₁ a₂ : A) ↦ congrFun₂ h a₁ a₂    simp [Matrix.traceLeft, Matrix.trace] at h ⊢    rw [← M.choi_map_inv, of_choi_matrix]    dsimp    rw [Finset.sum_comm_cycle, Finset.sum_comm_cycle]    simp_rw [← Finset.mul_sum, h, Matrix.one_apply]    simp