Theorem: Matrix.det_fin_four (MatrixCookbook/ForMathlib/Data/Matrix.lean)

State before:
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
Tactic:
rw [Matrix.det_succ_row_zero]
State after:
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

State before:
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
Tactic:
simp_rw [det_fin_three, submatrix_apply, Fin.sum_univ_four]
State after:
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

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
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

State before:
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
Tactic:
have h11 : (1 : Fin 4).succAbove 1 = 2 := rfl
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
⊢ (-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

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
⊢ (-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 h12 : (1 : Fin 4).succAbove 2 = 3 := rfl
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
⊢ (-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

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
⊢ (-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 h20 : (2 : Fin 4).succAbove 0 = 0 := rfl
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
⊢ (-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

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
⊢ (-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 h21 : (2 : Fin 4).succAbove 1 = 1 := rfl
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
⊢ (-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

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
⊢ (-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 h22 : (2 : Fin 4).succAbove 2 = 3 := rfl
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
⊢ (-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

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
⊢ (-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 h30 : (3 : Fin 4).succAbove 0 = 0 := rfl
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
⊢ (-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

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
⊢ (-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 h31 : (3 : Fin 4).succAbove 1 = 1 := rfl
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
⊢ (-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

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
⊢ (-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 h32 : (3 : Fin 4).succAbove 2 = 2 := rfl
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
⊢ (-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

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
⊢ (-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:
simp_rw [h10, h11, h12, h20, h21, h22, h30, h31, h32, Fin.zero_succAbove]
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
⊢ (-1) ^ ↑0 * A 0 0 *
            (A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 2) -
                      A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 1) -
                    A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 2) +
                  A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 0) +
                A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 1) -
              A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 0)) +
          (-1) ^ ↑1 * A 0 1 *
            (A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 3 -
                      A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 2 -
                    A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                  A (Fin.succ 0) 2 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
                A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 -
              A (Fin.succ 0) 3 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0) +
        (-1) ^ ↑2 * A 0 2 *
          (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 3 -
                    A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 1 -
                  A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                A (Fin.succ 0) 1 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
              A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
            A (Fin.succ 0) 3 * A (Fin.succ 1) 1 * A (Fin.succ 2) 0) +
      (-1) ^ ↑3 * A 0 3 *
        (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 2 -
                  A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 1 -
                A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 +
              A (Fin.succ 0) 1 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0 +
            A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
          A (Fin.succ 0) 2 * A (Fin.succ 1) 1 * A (Fin.succ 2) 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

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
⊢ (-1) ^ ↑0 * A 0 0 *
            (A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 2) -
                      A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 1) -
                    A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 2) +
                  A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 0) +
                A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 1) -
              A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 0)) +
          (-1) ^ ↑1 * A 0 1 *
            (A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 3 -
                      A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 2 -
                    A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                  A (Fin.succ 0) 2 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
                A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 -
              A (Fin.succ 0) 3 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0) +
        (-1) ^ ↑2 * A 0 2 *
          (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 3 -
                    A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 1 -
                  A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                A (Fin.succ 0) 1 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
              A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
            A (Fin.succ 0) 3 * A (Fin.succ 1) 1 * A (Fin.succ 2) 0) +
      (-1) ^ ↑3 * A 0 3 *
        (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 2 -
                  A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 1 -
                A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 +
              A (Fin.succ 0) 1 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0 +
            A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
          A (Fin.succ 0) 2 * A (Fin.succ 1) 1 * A (Fin.succ 2) 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 s0 : (0 : Fin 3).succ = 1 := rfl
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
⊢ (-1) ^ ↑0 * A 0 0 *
            (A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 2) -
                      A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 1) -
                    A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 2) +
                  A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 0) +
                A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 1) -
              A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 0)) +
          (-1) ^ ↑1 * A 0 1 *
            (A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 3 -
                      A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 2 -
                    A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                  A (Fin.succ 0) 2 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
                A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 -
              A (Fin.succ 0) 3 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0) +
        (-1) ^ ↑2 * A 0 2 *
          (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 3 -
                    A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 1 -
                  A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                A (Fin.succ 0) 1 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
              A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
            A (Fin.succ 0) 3 * A (Fin.succ 1) 1 * A (Fin.succ 2) 0) +
      (-1) ^ ↑3 * A 0 3 *
        (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 2 -
                  A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 1 -
                A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 +
              A (Fin.succ 0) 1 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0 +
            A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
          A (Fin.succ 0) 2 * A (Fin.succ 1) 1 * A (Fin.succ 2) 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

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
⊢ (-1) ^ ↑0 * A 0 0 *
            (A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 2) -
                      A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 1) -
                    A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 2) +
                  A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 0) +
                A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 1) -
              A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 0)) +
          (-1) ^ ↑1 * A 0 1 *
            (A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 3 -
                      A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 2 -
                    A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                  A (Fin.succ 0) 2 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
                A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 -
              A (Fin.succ 0) 3 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0) +
        (-1) ^ ↑2 * A 0 2 *
          (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 3 -
                    A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 1 -
                  A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                A (Fin.succ 0) 1 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
              A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
            A (Fin.succ 0) 3 * A (Fin.succ 1) 1 * A (Fin.succ 2) 0) +
      (-1) ^ ↑3 * A 0 3 *
        (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 2 -
                  A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 1 -
                A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 +
              A (Fin.succ 0) 1 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0 +
            A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
          A (Fin.succ 0) 2 * A (Fin.succ 1) 1 * A (Fin.succ 2) 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 s1 : (1 : Fin 3).succ = 2 := rfl
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
⊢ (-1) ^ ↑0 * A 0 0 *
            (A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 2) -
                      A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 1) -
                    A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 2) +
                  A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 0) +
                A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 1) -
              A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 0)) +
          (-1) ^ ↑1 * A 0 1 *
            (A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 3 -
                      A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 2 -
                    A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                  A (Fin.succ 0) 2 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
                A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 -
              A (Fin.succ 0) 3 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0) +
        (-1) ^ ↑2 * A 0 2 *
          (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 3 -
                    A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 1 -
                  A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                A (Fin.succ 0) 1 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
              A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
            A (Fin.succ 0) 3 * A (Fin.succ 1) 1 * A (Fin.succ 2) 0) +
      (-1) ^ ↑3 * A 0 3 *
        (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 2 -
                  A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 1 -
                A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 +
              A (Fin.succ 0) 1 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0 +
            A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
          A (Fin.succ 0) 2 * A (Fin.succ 1) 1 * A (Fin.succ 2) 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

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
⊢ (-1) ^ ↑0 * A 0 0 *
            (A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 2) -
                      A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 1) -
                    A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 2) +
                  A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 0) +
                A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 1) -
              A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 0)) +
          (-1) ^ ↑1 * A 0 1 *
            (A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 3 -
                      A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 2 -
                    A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                  A (Fin.succ 0) 2 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
                A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 -
              A (Fin.succ 0) 3 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0) +
        (-1) ^ ↑2 * A 0 2 *
          (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 3 -
                    A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 1 -
                  A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                A (Fin.succ 0) 1 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
              A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
            A (Fin.succ 0) 3 * A (Fin.succ 1) 1 * A (Fin.succ 2) 0) +
      (-1) ^ ↑3 * A 0 3 *
        (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 2 -
                  A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 1 -
                A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 +
              A (Fin.succ 0) 1 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0 +
            A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
          A (Fin.succ 0) 2 * A (Fin.succ 1) 1 * A (Fin.succ 2) 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 s2 : (2 : Fin 3).succ = 3 := rfl
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
⊢ (-1) ^ ↑0 * A 0 0 *
            (A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 2) -
                      A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 1) -
                    A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 2) +
                  A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 0) +
                A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 1) -
              A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 0)) +
          (-1) ^ ↑1 * A 0 1 *
            (A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 3 -
                      A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 2 -
                    A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                  A (Fin.succ 0) 2 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
                A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 -
              A (Fin.succ 0) 3 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0) +
        (-1) ^ ↑2 * A 0 2 *
          (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 3 -
                    A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 1 -
                  A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                A (Fin.succ 0) 1 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
              A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
            A (Fin.succ 0) 3 * A (Fin.succ 1) 1 * A (Fin.succ 2) 0) +
      (-1) ^ ↑3 * A 0 3 *
        (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 2 -
                  A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 1 -
                A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 +
              A (Fin.succ 0) 1 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0 +
            A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
          A (Fin.succ 0) 2 * A (Fin.succ 1) 1 * A (Fin.succ 2) 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

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
⊢ (-1) ^ ↑0 * A 0 0 *
            (A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 2) -
                      A (Fin.succ 0) (Fin.succ 0) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 1) -
                    A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 2) +
                  A (Fin.succ 0) (Fin.succ 1) * A (Fin.succ 1) (Fin.succ 2) * A (Fin.succ 2) (Fin.succ 0) +
                A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 0) * A (Fin.succ 2) (Fin.succ 1) -
              A (Fin.succ 0) (Fin.succ 2) * A (Fin.succ 1) (Fin.succ 1) * A (Fin.succ 2) (Fin.succ 0)) +
          (-1) ^ ↑1 * A 0 1 *
            (A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 3 -
                      A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 2 -
                    A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                  A (Fin.succ 0) 2 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
                A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 -
              A (Fin.succ 0) 3 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0) +
        (-1) ^ ↑2 * A 0 2 *
          (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 3 -
                    A (Fin.succ 0) 0 * A (Fin.succ 1) 3 * A (Fin.succ 2) 1 -
                  A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 3 +
                A (Fin.succ 0) 1 * A (Fin.succ 1) 3 * A (Fin.succ 2) 0 +
              A (Fin.succ 0) 3 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
            A (Fin.succ 0) 3 * A (Fin.succ 1) 1 * A (Fin.succ 2) 0) +
      (-1) ^ ↑3 * A 0 3 *
        (A (Fin.succ 0) 0 * A (Fin.succ 1) 1 * A (Fin.succ 2) 2 -
                  A (Fin.succ 0) 0 * A (Fin.succ 1) 2 * A (Fin.succ 2) 1 -
                A (Fin.succ 0) 1 * A (Fin.succ 1) 0 * A (Fin.succ 2) 2 +
              A (Fin.succ 0) 1 * A (Fin.succ 1) 2 * A (Fin.succ 2) 0 +
            A (Fin.succ 0) 2 * A (Fin.succ 1) 0 * A (Fin.succ 2) 1 -
          A (Fin.succ 0) 2 * A (Fin.succ 1) 1 * A (Fin.succ 2) 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:
simp_rw [s0, s1, s2]
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
⊢ (-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

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
⊢ (-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 a0 : (-1 : R) ^ ((0 : Fin 4) : ℕ) = 1 := Even.neg_one_pow (by decide)
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
⊢ (-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

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
⊢ (-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 a1 : (-1 : R) ^ ((1 : Fin 4) : ℕ) = -1 := Odd.neg_one_pow (by decide)
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
⊢ (-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

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)
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

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
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
Tactic:
have a3 : (-1 : R) ^ ((3 : Fin 4) : ℕ) = -1 := Odd.neg_one_pow (by decide)
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
a3 : (-1) ^ ↑3 = -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

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
a2 : (-1) ^ ↑2 = 1
a3 : (-1) ^ ↑3 = -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:
simp_rw [a0, a1, a2, a3]
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
a3 : (-1) ^ ↑3 = -1
⊢ 1 * 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 * 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 * 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 * 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

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
a2 : (-1) ^ ↑2 = 1
a3 : (-1) ^ ↑3 = -1
⊢ 1 * 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 * 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 * 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 * 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:
ring
State after:
no goals

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
⊢ Even ↑0
Tactic:
decide
State after:
no goals

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
⊢ Odd ↑1
Tactic:
decide
State after:
no goals

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
⊢ Even ↑2
Tactic:
decide
State after:
no goals

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
a2 : (-1) ^ ↑2 = 1
⊢ Odd ↑3
Tactic:
decide
State after:
no goals