Theorem: Matrix.det_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ (-1) ^ ↑0 * A 0 0 *
            (A (Fin.succ 0) (Fin.succAbove 0 0) * A (Fin.succ 1) (Fin.succAbove 0 1) *
                        A (Fin.succ 2) (Fin.succAbove 0 2) -
                      A (Fin.succ 0) (Fin.succAbove 0 0) * A (Fin.succ 1) (Fin.succAbove 0 2) *
                        A (Fin.succ 2) (Fin.succAbove 0 1) -
                    A (Fin.succ 0) (Fin.succAbove 0 1) * A (Fin.succ 1) (Fin.succAbove 0 0) *
                      A (Fin.succ 2) (Fin.succAbove 0 2) +
                  A (Fin.succ 0) (Fin.succAbove 0 1) * A (Fin.succ 1) (Fin.succAbove 0 2) *
                    A (Fin.succ 2) (Fin.succAbove 0 0) +
                A (Fin.succ 0) (Fin.succAbove 0 2) * A (Fin.succ 1) (Fin.succAbove 0 0) *
                  A (Fin.succ 2) (Fin.succAbove 0 1) -
              A (Fin.succ 0) (Fin.succAbove 0 2) * A (Fin.succ 1) (Fin.succAbove 0 1) *
                A (Fin.succ 2) (Fin.succAbove 0 0)) +
          (-1) ^ ↑1 * A 0 1 *
            (A (Fin.succ 0) (Fin.succAbove 1 0) * A (Fin.succ 1) (Fin.succAbove 1 1) *
                        A (Fin.succ 2) (Fin.succAbove 1 2) -
                      A (Fin.succ 0) (Fin.succAbove 1 0) * A (Fin.succ 1) (Fin.succAbove 1 2) *
                        A (Fin.succ 2) (Fin.succAbove 1 1) -
                    A (Fin.succ 0) (Fin.succAbove 1 1) * A (Fin.succ 1) (Fin.succAbove 1 0) *
                      A (Fin.succ 2) (Fin.succAbove 1 2) +
                  A (Fin.succ 0) (Fin.succAbove 1 1) * A (Fin.succ 1) (Fin.succAbove 1 2) *
                    A (Fin.succ 2) (Fin.succAbove 1 0) +
                A (Fin.succ 0) (Fin.succAbove 1 2) * A (Fin.succ 1) (Fin.succAbove 1 0) *
                  A (Fin.succ 2) (Fin.succAbove 1 1) -
              A (Fin.succ 0) (Fin.succAbove 1 2) * A (Fin.succ 1) (Fin.succAbove 1 1) *
                A (Fin.succ 2) (Fin.succAbove 1 0)) +
        (-1) ^ ↑2 * A 0 2 *
          (A (Fin.succ 0) (Fin.succAbove 2 0) * A (Fin.succ 1) (Fin.succAbove 2 1) *
                      A (Fin.succ 2) (Fin.succAbove 2 2) -
                    A (Fin.succ 0) (Fin.succAbove 2 0) * A (Fin.succ 1) (Fin.succAbove 2 2) *
                      A (Fin.succ 2) (Fin.succAbove 2 1) -
                  A (Fin.succ 0) (Fin.succAbove 2 1) * A (Fin.succ 1) (Fin.succAbove 2 0) *
                    A (Fin.succ 2) (Fin.succAbove 2 2) +
                A (Fin.succ 0) (Fin.succAbove 2 1) * A (Fin.succ 1) (Fin.succAbove 2 2) *
                  A (Fin.succ 2) (Fin.succAbove 2 0) +
              A (Fin.succ 0) (Fin.succAbove 2 2) * A (Fin.succ 1) (Fin.succAbove 2 0) *
                A (Fin.succ 2) (Fin.succAbove 2 1) -
            A (Fin.succ 0) (Fin.succAbove 2 2) * A (Fin.succ 1) (Fin.succAbove 2 1) *
              A (Fin.succ 2) (Fin.succAbove 2 0)) +
      (-1) ^ ↑3 * A 0 3 *
        (A (Fin.succ 0) (Fin.succAbove 3 0) * A (Fin.succ 1) (Fin.succAbove 3 1) * A (Fin.succ 2) (Fin.succAbove 3 2) -
                  A (Fin.succ 0) (Fin.succAbove 3 0) * A (Fin.succ 1) (Fin.succAbove 3 2) *
                    A (Fin.succ 2) (Fin.succAbove 3 1) -
                A (Fin.succ 0) (Fin.succAbove 3 1) * A (Fin.succ 1) (Fin.succAbove 3 0) *
                  A (Fin.succ 2) (Fin.succAbove 3 2) +
              A (Fin.succ 0) (Fin.succAbove 3 1) * A (Fin.succ 1) (Fin.succAbove 3 2) *
                A (Fin.succ 2) (Fin.succAbove 3 0) +
            A (Fin.succ 0) (Fin.succAbove 3 2) * A (Fin.succ 1) (Fin.succAbove 3 0) *
              A (Fin.succ 2) (Fin.succAbove 3 1) -
          A (Fin.succ 0) (Fin.succAbove 3 2) * A (Fin.succ 1) (Fin.succAbove 3 1) *
            A (Fin.succ 2) (Fin.succAbove 3 0)) =
    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
Tactic:
have h10 : (1 : Fin 4).succAbove 0 = 0 := rfl
Proof state after:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
h10 : Fin.succAbove 1 0 = 0
⊢ (-1) ^ ↑0 * A 0 0 *
            (A (Fin.succ 0) (Fin.succAbove 0 0) * A (Fin.succ 1) (Fin.succAbove 0 1) *
                        A (Fin.succ 2) (Fin.succAbove 0 2) -
                      A (Fin.succ 0) (Fin.succAbove 0 0) * A (Fin.succ 1) (Fin.succAbove 0 2) *
                        A (Fin.succ 2) (Fin.succAbove 0 1) -
                    A (Fin.succ 0) (Fin.succAbove 0 1) * A (Fin.succ 1) (Fin.succAbove 0 0) *
                      A (Fin.succ 2) (Fin.succAbove 0 2) +
                  A (Fin.succ 0) (Fin.succAbove 0 1) * A (Fin.succ 1) (Fin.succAbove 0 2) *
                    A (Fin.succ 2) (Fin.succAbove 0 0) +
                A (Fin.succ 0) (Fin.succAbove 0 2) * A (Fin.succ 1) (Fin.succAbove 0 0) *
                  A (Fin.succ 2) (Fin.succAbove 0 1) -
              A (Fin.succ 0) (Fin.succAbove 0 2) * A (Fin.succ 1) (Fin.succAbove 0 1) *
                A (Fin.succ 2) (Fin.succAbove 0 0)) +
          (-1) ^ ↑1 * A 0 1 *
            (A (Fin.succ 0) (Fin.succAbove 1 0) * A (Fin.succ 1) (Fin.succAbove 1 1) *
                        A (Fin.succ 2) (Fin.succAbove 1 2) -
                      A (Fin.succ 0) (Fin.succAbove 1 0) * A (Fin.succ 1) (Fin.succAbove 1 2) *
                        A (Fin.succ 2) (Fin.succAbove 1 1) -
                    A (Fin.succ 0) (Fin.succAbove 1 1) * A (Fin.succ 1) (Fin.succAbove 1 0) *
                      A (Fin.succ 2) (Fin.succAbove 1 2) +
                  A (Fin.succ 0) (Fin.succAbove 1 1) * A (Fin.succ 1) (Fin.succAbove 1 2) *
                    A (Fin.succ 2) (Fin.succAbove 1 0) +
                A (Fin.succ 0) (Fin.succAbove 1 2) * A (Fin.succ 1) (Fin.succAbove 1 0) *
                  A (Fin.succ 2) (Fin.succAbove 1 1) -
              A (Fin.succ 0) (Fin.succAbove 1 2) * A (Fin.succ 1) (Fin.succAbove 1 1) *
                A (Fin.succ 2) (Fin.succAbove 1 0)) +
        (-1) ^ ↑2 * A 0 2 *
          (A (Fin.succ 0) (Fin.succAbove 2 0) * A (Fin.succ 1) (Fin.succAbove 2 1) *
                      A (Fin.succ 2) (Fin.succAbove 2 2) -
                    A (Fin.succ 0) (Fin.succAbove 2 0) * A (Fin.succ 1) (Fin.succAbove 2 2) *
                      A (Fin.succ 2) (Fin.succAbove 2 1) -
                  A (Fin.succ 0) (Fin.succAbove 2 1) * A (Fin.succ 1) (Fin.succAbove 2 0) *
                    A (Fin.succ 2) (Fin.succAbove 2 2) +
                A (Fin.succ 0) (Fin.succAbove 2 1) * A (Fin.succ 1) (Fin.succAbove 2 2) *
                  A (Fin.succ 2) (Fin.succAbove 2 0) +
              A (Fin.succ 0) (Fin.succAbove 2 2) * A (Fin.succ 1) (Fin.succAbove 2 0) *
                A (Fin.succ 2) (Fin.succAbove 2 1) -
            A (Fin.succ 0) (Fin.succAbove 2 2) * A (Fin.succ 1) (Fin.succAbove 2 1) *
              A (Fin.succ 2) (Fin.succAbove 2 0)) +
      (-1) ^ ↑3 * A 0 3 *
        (A (Fin.succ 0) (Fin.succAbove 3 0) * A (Fin.succ 1) (Fin.succAbove 3 1) * A (Fin.succ 2) (Fin.succAbove 3 2) -
                  A (Fin.succ 0) (Fin.succAbove 3 0) * A (Fin.succ 1) (Fin.succAbove 3 2) *
                    A (Fin.succ 2) (Fin.succAbove 3 1) -
                A (Fin.succ 0) (Fin.succAbove 3 1) * A (Fin.succ 1) (Fin.succAbove 3 0) *
                  A (Fin.succ 2) (Fin.succAbove 3 2) +
              A (Fin.succ 0) (Fin.succAbove 3 1) * A (Fin.succ 1) (Fin.succAbove 3 2) *
                A (Fin.succ 2) (Fin.succAbove 3 0) +
            A (Fin.succ 0) (Fin.succAbove 3 2) * A (Fin.succ 1) (Fin.succAbove 3 0) *
              A (Fin.succ 2) (Fin.succAbove 3 1) -
          A (Fin.succ 0) (Fin.succAbove 3 2) * A (Fin.succ 1) (Fin.succAbove 3 1) *
            A (Fin.succ 2) (Fin.succAbove 3 0)) =
    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