Pauli Co contr pauli Contr

lemma pauliCo_contr_pauliContr :    {σ_^^ | ν α β ⊗ σ^^^ | ν α' β' = (2 : ℂ) •ₜ εL | α α' ⊗ εR | β β'}ᵀ := by  apply (Tensor.basis _).repr.injective  ext b  conv_rhs =>    rw [permT_basis_repr_symm_apply]    rw [_root_.map_smul]    simp only [Nat.reduceAdd, Nat.succ_eq_add_one, Fin.isValue, Fin.succAbove_zero,      Function.comp_apply, Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul]    rw (transparency := .instances) [prodT_basis_repr_apply]    simp only [Nat.reduceAdd, Nat.succ_eq_add_one, Fin.isValue, Fin.succAbove_zero,      Function.comp_apply]    rw [leftMetric_eq_ofRat, rightMetric_eq_ofRat]    simp only [Nat.reduceAdd, Nat.succ_eq_add_one, Fin.isValue, Fin.succAbove_zero,      Function.comp_apply, cons_val_zero, cons_val_one, head_cons, ofRat_basis_repr_apply]    rw [← Physlib.RatComplexNum.toComplexNum.map_mul]    change (2 : ℕ) * _    rw [Physlib.RatComplexNum.ofNat_mul_toComplexNum 2]  rw [contrT_basis_repr_apply]  conv_lhs =>    enter [2, x]    rw [prodT_basis_repr_apply]    simp only [pauliCo_eq_ofRat, toTensor_eq_ofRat]    simp only [Fin.isValue, Fin.cast_eq_self, ofRat_basis_repr_apply]    left    rw [← Physlib.RatComplexNum.toComplexNum.map_mul]  conv_lhs =>    enter [2, x]    right    rw (transparency := .instances) [contr_basis_ratComplexNum]  conv_lhs =>    enter [2, x]    rw [← Physlib.RatComplexNum.toComplexNum.map_mul]  rw [← map_sum Physlib.RatComplexNum.toComplexNum]  apply (Function.Injective.eq_iff Physlib.RatComplexNum.toComplexNum_injective).mpr  revert b  decide +kernel