rw [Matrix.det_succ_row_zero]
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ A.det =
    A 0 0 * A 1 1 * A 2 2 * A 3 3 - A 0 0 * A 1 1 * A 2 3 * A 3 2 - A 0 0 * A 1 2 * A 2 1 * A 3 3 +
                                              A 0 0 * A 1 2 * A 2 3 * A 3 1 +
                                            A 0 0 * A 1 3 * A 2 1 * A 3 2 -
                                          A 0 0 * A 1 3 * A 2 2 * A 3 1 -
                                        A 0 1 * A 1 0 * A 2 2 * A 3 3 +
                                      A 0 1 * A 1 0 * A 2 3 * A 3 2 +
                                    A 0 1 * A 1 2 * A 2 0 * A 3 3 -
                                  A 0 1 * A 1 2 * A 2 3 * A 3 0 -
                                A 0 1 * A 1 3 * A 2 0 * A 3 2 +
                              A 0 1 * A 1 3 * A 2 2 * A 3 0 +
                            A 0 2 * A 1 0 * A 2 1 * A 3 3 -
                          A 0 2 * A 1 0 * A 2 3 * A 3 1 -
                        A 0 2 * A 1 1 * A 2 0 * A 3 3 +
                      A 0 2 * A 1 1 * A 2 3 * A 3 0 +
                    A 0 2 * A 1 3 * A 2 0 * A 3 1 -
                  A 0 2 * A 1 3 * A 2 1 * A 3 0 -
                A 0 3 * A 1 0 * A 2 1 * A 3 2 +
              A 0 3 * A 1 0 * A 2 2 * A 3 1 +
            A 0 3 * A 1 1 * A 2 0 * A 3 2 -
          A 0 3 * A 1 1 * A 2 2 * A 3 0 -
        A 0 3 * A 1 2 * A 2 0 * A 3 1 +
      A 0 3 * A 1 2 * A 2 1 * A 3 0
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ ∑ j : Fin (Nat.succ 3), (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det =
    A 0 0 * A 1 1 * A 2 2 * A 3 3 - A 0 0 * A 1 1 * A 2 3 * A 3 2 - A 0 0 * A 1 2 * A 2 1 * A 3 3 +
                                              A 0 0 * A 1 2 * A 2 3 * A 3 1 +
                                            A 0 0 * A 1 3 * A 2 1 * A 3 2 -
                                          A 0 0 * A 1 3 * A 2 2 * A 3 1 -
                                        A 0 1 * A 1 0 * A 2 2 * A 3 3 +
                                      A 0 1 * A 1 0 * A 2 3 * A 3 2 +
                                    A 0 1 * A 1 2 * A 2 0 * A 3 3 -
                                  A 0 1 * A 1 2 * A 2 3 * A 3 0 -
                                A 0 1 * A 1 3 * A 2 0 * A 3 2 +
                              A 0 1 * A 1 3 * A 2 2 * A 3 0 +
                            A 0 2 * A 1 0 * A 2 1 * A 3 3 -
                          A 0 2 * A 1 0 * A 2 3 * A 3 1 -
                        A 0 2 * A 1 1 * A 2 0 * A 3 3 +
                      A 0 2 * A 1 1 * A 2 3 * A 3 0 +
                    A 0 2 * A 1 3 * A 2 0 * A 3 1 -
                  A 0 2 * A 1 3 * A 2 1 * A 3 0 -
                A 0 3 * A 1 0 * A 2 1 * A 3 2 +
              A 0 3 * A 1 0 * A 2 2 * A 3 1 +
            A 0 3 * A 1 1 * A 2 0 * A 3 2 -
          A 0 3 * A 1 1 * A 2 2 * A 3 0 -
        A 0 3 * A 1 2 * A 2 0 * A 3 1 +
      A 0 3 * A 1 2 * A 2 1 * A 3 0