no goals
R : Type ?u.104284
S : Type ?u.104287
i j : Fin 2
⊢ ↑(↑basisOneI.repr (Matrix.vecCons 1 ![I] i)) j = ↑(Finsupp.single i 1) j
fin_cases i <;> fin_cases j <;>
  simp [coe_basisOneI_repr, Finsupp.single_eq_of_ne, Matrix.cons_val_zero,
    Matrix.cons_val_one, Matrix.head_cons, Fin.one_eq_zero_iff, Ne.def, not_false_iff, I_re,
    Nat.succ_succ_ne_one, one_im, I_im, one_re, Finsupp.single_eq_same, Fin.zero_eq_one_iff]