Self Adjoint ext complex

lemma selfAdjoint_ext_complex {A B : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)}    (h0 : Matrix.trace (σ0 * A.1) = Matrix.trace (σ0 * B.1))    (h1 : Matrix.trace (σ1 * A.1) = Matrix.trace (σ1 * B.1))    (h2 : Matrix.trace (σ2 * A.1) = Matrix.trace (σ2 * B.1))    (h3 : Matrix.trace (σ3 * A.1) = Matrix.trace (σ3 * B.1)) : A = B := by  ext i j  rw [eta_fin_two A.1, eta_fin_two B.1] at h0 h1 h2 h3  simp only [Fin.isValue, pauliMatrix_inl_zero_eq_one, one_mul, trace_fin_two_of] at h0  simp only [pauliMatrix, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons,    head_cons, zero_smul, tail_cons, one_smul, empty_vecMul, add_zero, zero_add, empty_mul,    Equiv.symm_apply_apply, trace_fin_two_of] at h1  simp only [pauliMatrix, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons,    head_cons, zero_smul, tail_cons, neg_smul, smul_cons, smul_eq_mul, smul_empty, neg_cons,    neg_empty, empty_vecMul, add_zero, zero_add, empty_mul, Equiv.symm_apply_apply,    trace_fin_two_of] at h2  simp only [pauliMatrix, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons,    head_cons, one_smul, tail_cons, zero_smul, empty_vecMul, add_zero, neg_smul, neg_cons,    neg_empty, zero_add, empty_mul, Equiv.symm_apply_apply, trace_fin_two_of] at h3  match i, j with  | 0, 0 =>    linear_combination (norm := ring_nf) (h0 + h3) / 2  | 0, 1 =>    linear_combination (norm := ring_nf) (h1 - I * h2) / 2    simp  | 1, 0 =>    linear_combination (norm := ring_nf) (h1 + I * h2) / 2    simp  | 1, 1 =>    linear_combination (norm := ring_nf) (h0 - h3) / 2