Theorem: Matrix.det_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
h10 : Fin.succAbove 1 0 = 0
h11 : Fin.succAbove 1 1 = 2
h12 : Fin.succAbove 1 2 = 3
h20 : Fin.succAbove 2 0 = 0
h21 : Fin.succAbove 2 1 = 1
h22 : Fin.succAbove 2 2 = 3
h30 : Fin.succAbove 3 0 = 0
h31 : Fin.succAbove 3 1 = 1
h32 : Fin.succAbove 3 2 = 2
s0 : Fin.succ 0 = 1
s1 : Fin.succ 1 = 2
s2 : Fin.succ 2 = 3
a0 : (-1) ^ ↑0 = 1
a1 : (-1) ^ ↑1 = -1
⊢ (-1) ^ ↑0 * A 0 0 *
            (A 1 1 * A 2 2 * A 3 3 - A 1 1 * A 2 3 * A 3 2 - A 1 2 * A 2 1 * A 3 3 + A 1 2 * A 2 3 * A 3 1 +
                A 1 3 * A 2 1 * A 3 2 -
              A 1 3 * A 2 2 * A 3 1) +
          (-1) ^ ↑1 * A 0 1 *
            (A 1 0 * A 2 2 * A 3 3 - A 1 0 * A 2 3 * A 3 2 - A 1 2 * A 2 0 * A 3 3 + A 1 2 * A 2 3 * A 3 0 +
                A 1 3 * A 2 0 * A 3 2 -
              A 1 3 * A 2 2 * A 3 0) +
        (-1) ^ ↑2 * A 0 2 *
          (A 1 0 * A 2 1 * A 3 3 - A 1 0 * A 2 3 * A 3 1 - A 1 1 * A 2 0 * A 3 3 + A 1 1 * A 2 3 * A 3 0 +
              A 1 3 * A 2 0 * A 3 1 -
            A 1 3 * A 2 1 * A 3 0) +
      (-1) ^ ↑3 * A 0 3 *
        (A 1 0 * A 2 1 * A 3 2 - A 1 0 * A 2 2 * A 3 1 - A 1 1 * A 2 0 * A 3 2 + A 1 1 * A 2 2 * A 3 0 +
            A 1 2 * A 2 0 * A 3 1 -
          A 1 2 * A 2 1 * A 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 a2 : (-1 : R) ^ ((2 : Fin 4) : ℕ) = 1 := Even.neg_one_pow (by decide)
Proof state after:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
h10 : Fin.succAbove 1 0 = 0
h11 : Fin.succAbove 1 1 = 2
h12 : Fin.succAbove 1 2 = 3
h20 : Fin.succAbove 2 0 = 0
h21 : Fin.succAbove 2 1 = 1
h22 : Fin.succAbove 2 2 = 3
h30 : Fin.succAbove 3 0 = 0
h31 : Fin.succAbove 3 1 = 1
h32 : Fin.succAbove 3 2 = 2
s0 : Fin.succ 0 = 1
s1 : Fin.succ 1 = 2
s2 : Fin.succ 2 = 3
a0 : (-1) ^ ↑0 = 1
a1 : (-1) ^ ↑1 = -1
a2 : (-1) ^ ↑2 = 1
⊢ (-1) ^ ↑0 * A 0 0 *
            (A 1 1 * A 2 2 * A 3 3 - A 1 1 * A 2 3 * A 3 2 - A 1 2 * A 2 1 * A 3 3 + A 1 2 * A 2 3 * A 3 1 +
                A 1 3 * A 2 1 * A 3 2 -
              A 1 3 * A 2 2 * A 3 1) +
          (-1) ^ ↑1 * A 0 1 *
            (A 1 0 * A 2 2 * A 3 3 - A 1 0 * A 2 3 * A 3 2 - A 1 2 * A 2 0 * A 3 3 + A 1 2 * A 2 3 * A 3 0 +
                A 1 3 * A 2 0 * A 3 2 -
              A 1 3 * A 2 2 * A 3 0) +
        (-1) ^ ↑2 * A 0 2 *
          (A 1 0 * A 2 1 * A 3 3 - A 1 0 * A 2 3 * A 3 1 - A 1 1 * A 2 0 * A 3 3 + A 1 1 * A 2 3 * A 3 0 +
              A 1 3 * A 2 0 * A 3 1 -
            A 1 3 * A 2 1 * A 3 0) +
      (-1) ^ ↑3 * A 0 3 *
        (A 1 0 * A 2 1 * A 3 2 - A 1 0 * A 2 2 * A 3 1 - A 1 1 * A 2 0 * A 3 2 + A 1 1 * A 2 2 * A 3 0 +
            A 1 2 * A 2 0 * A 3 1 -
          A 1 2 * A 2 1 * A 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