Theorem: det_one_add_fin_four
Proof state before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ (1 + A 0 0) * (1 + A 1 1) * (1 + A 2 2) * (1 + A 3 3) -
                                                  (1 + A 0 0) * (1 + A 1 1) * (OfNat.ofNat 1 2 3 + A 2 3) *
                                                    (OfNat.ofNat 1 3 2 + A 3 2) -
                                                (1 + A 0 0) * (OfNat.ofNat 1 1 2 + A 1 2) *
                                                    (OfNat.ofNat 1 2 1 + A 2 1) *
                                                  (1 + A 3 3) +
                                              (1 + A 0 0) * (OfNat.ofNat 1 1 2 + A 1 2) * (OfNat.ofNat 1 2 3 + A 2 3) *
                                                (OfNat.ofNat 1 3 1 + A 3 1) +
                                            (1 + A 0 0) * (OfNat.ofNat 1 1 3 + A 1 3) * (OfNat.ofNat 1 2 1 + A 2 1) *
                                              (OfNat.ofNat 1 3 2 + A 3 2) -
                                          (1 + A 0 0) * (OfNat.ofNat 1 1 3 + A 1 3) * (1 + A 2 2) *
                                            (OfNat.ofNat 1 3 1 + A 3 1) -
                                        (OfNat.ofNat 1 0 1 + A 0 1) * (OfNat.ofNat 1 1 0 + A 1 0) * (1 + A 2 2) *
                                          (1 + A 3 3) +
                                      (OfNat.ofNat 1 0 1 + A 0 1) * (OfNat.ofNat 1 1 0 + A 1 0) *
                                          (OfNat.ofNat 1 2 3 + A 2 3) *
                                        (OfNat.ofNat 1 3 2 + A 3 2) +
                                    (OfNat.ofNat 1 0 1 + A 0 1) * (OfNat.ofNat 1 1 2 + A 1 2) *
                                        (OfNat.ofNat 1 2 0 + A 2 0) *
                                      (1 + A 3 3) -
                                  (OfNat.ofNat 1 0 1 + A 0 1) * (OfNat.ofNat 1 1 2 + A 1 2) *
                                      (OfNat.ofNat 1 2 3 + A 2 3) *
                                    (OfNat.ofNat 1 3 0 + A 3 0) -
                                (OfNat.ofNat 1 0 1 + A 0 1) * (OfNat.ofNat 1 1 3 + A 1 3) *
                                    (OfNat.ofNat 1 2 0 + A 2 0) *
                                  (OfNat.ofNat 1 3 2 + A 3 2) +
                              (OfNat.ofNat 1 0 1 + A 0 1) * (OfNat.ofNat 1 1 3 + A 1 3) * (1 + A 2 2) *
                                (OfNat.ofNat 1 3 0 + A 3 0) +
                            (OfNat.ofNat 1 0 2 + A 0 2) * (OfNat.ofNat 1 1 0 + A 1 0) * (OfNat.ofNat 1 2 1 + A 2 1) *
                              (1 + A 3 3) -
                          (OfNat.ofNat 1 0 2 + A 0 2) * (OfNat.ofNat 1 1 0 + A 1 0) * (OfNat.ofNat 1 2 3 + A 2 3) *
                            (OfNat.ofNat 1 3 1 + A 3 1) -
                        (OfNat.ofNat 1 0 2 + A 0 2) * (1 + A 1 1) * (OfNat.ofNat 1 2 0 + A 2 0) * (1 + A 3 3) +
                      (OfNat.ofNat 1 0 2 + A 0 2) * (1 + A 1 1) * (OfNat.ofNat 1 2 3 + A 2 3) *
                        (OfNat.ofNat 1 3 0 + A 3 0) +
                    (OfNat.ofNat 1 0 2 + A 0 2) * (OfNat.ofNat 1 1 3 + A 1 3) * (OfNat.ofNat 1 2 0 + A 2 0) *
                      (OfNat.ofNat 1 3 1 + A 3 1) -
                  (OfNat.ofNat 1 0 2 + A 0 2) * (OfNat.ofNat 1 1 3 + A 1 3) * (OfNat.ofNat 1 2 1 + A 2 1) *
                    (OfNat.ofNat 1 3 0 + A 3 0) -
                (OfNat.ofNat 1 0 3 + A 0 3) * (OfNat.ofNat 1 1 0 + A 1 0) * (OfNat.ofNat 1 2 1 + A 2 1) *
                  (OfNat.ofNat 1 3 2 + A 3 2) +
              (OfNat.ofNat 1 0 3 + A 0 3) * (OfNat.ofNat 1 1 0 + A 1 0) * (1 + A 2 2) * (OfNat.ofNat 1 3 1 + A 3 1) +
            (OfNat.ofNat 1 0 3 + A 0 3) * (1 + A 1 1) * (OfNat.ofNat 1 2 0 + A 2 0) * (OfNat.ofNat 1 3 2 + A 3 2) -
          (OfNat.ofNat 1 0 3 + A 0 3) * (1 + A 1 1) * (1 + A 2 2) * (OfNat.ofNat 1 3 0 + A 3 0) -
        (OfNat.ofNat 1 0 3 + A 0 3) * (OfNat.ofNat 1 1 2 + A 1 2) * (OfNat.ofNat 1 2 0 + A 2 0) *
          (OfNat.ofNat 1 3 1 + A 3 1) +
      (OfNat.ofNat 1 0 3 + A 0 3) * (OfNat.ofNat 1 1 2 + A 1 2) * (OfNat.ofNat 1 2 1 + A 2 1) *
        (OfNat.ofNat 1 3 0 + A 3 0) =
    A 0 0 + A 1 1 + A 2 2 + A 3 3 + A 0 0 * A 1 1 - A 0 1 * A 1 0 + A 0 0 * A 2 2 - A 0 2 * A 2 0 + A 0 0 * A 3 3 -
                                                                                                                    A 0
                                                                                                                        3 *
                                                                                                                      A
                                                                                                                        3
                                                                                                                        0 +
                                                                                                                  A 1
                                                                                                                      1 *
                                                                                                                    A 2
                                                                                                                      2 -
                                                                                                                A 1 2 *
                                                                                                                  A 2
                                                                                                                    1 +
                                                                                                              A 1 1 *
                                                                                                                A 3 3 -
                                                                                                            A 1 3 *
                                                                                                              A 3 1 +
                                                                                                          A 2 2 *
                                                                                                            A 3 3 -
                                                                                                        A 2 3 * A 3 2 +
                                                                                                      A 0 0 * A 1 1 *
                                                                                                        A 2 2 -
                                                                                                    A 0 0 * A 1 2 *
                                                                                                      A 2 1 -
                                                                                                  A 0 1 * A 1 0 *
                                                                                                    A 2 2 +
                                                                                                A 0 1 * A 1 2 * A 2 0 +
                                                                                              A 0 2 * A 1 0 * A 2 1 -
                                                                                            A 0 2 * A 1 1 * A 2 0 +
                                                                                          A 0 0 * A 1 1 * A 3 3 -
                                                                                        A 0 0 * A 1 3 * A 3 1 -
                                                                                      A 0 1 * A 1 0 * A 3 3 +
                                                                                    A 0 1 * A 1 3 * A 3 0 +
                                                                                  A 0 3 * A 1 0 * A 3 1 -
                                                                                A 0 3 * A 1 1 * A 3 0 +
                                                                              A 0 0 * A 2 2 * A 3 3 -
                                                                            A 0 0 * A 2 3 * A 3 2 -
                                                                          A 0 2 * A 2 0 * A 3 3 +
                                                                        A 0 2 * A 2 3 * A 3 0 +
                                                                      A 0 3 * A 2 0 * A 3 2 -
                                                                    A 0 3 * A 2 2 * A 3 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 +
                                                      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 +
      1
Tactic:
simp (disch := decide) only [one_apply_ne]
Proof state after:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ (1 + A 0 0) * (1 + A 1 1) * (1 + A 2 2) * (1 + A 3 3) - (1 + A 0 0) * (1 + A 1 1) * (0 + A 2 3) * (0 + A 3 2) -
                                                (1 + A 0 0) * (0 + A 1 2) * (0 + A 2 1) * (1 + A 3 3) +
                                              (1 + A 0 0) * (0 + A 1 2) * (0 + A 2 3) * (0 + A 3 1) +
                                            (1 + A 0 0) * (0 + A 1 3) * (0 + A 2 1) * (0 + A 3 2) -
                                          (1 + A 0 0) * (0 + A 1 3) * (1 + A 2 2) * (0 + A 3 1) -
                                        (0 + A 0 1) * (0 + A 1 0) * (1 + A 2 2) * (1 + A 3 3) +
                                      (0 + A 0 1) * (0 + A 1 0) * (0 + A 2 3) * (0 + A 3 2) +
                                    (0 + A 0 1) * (0 + A 1 2) * (0 + A 2 0) * (1 + A 3 3) -
                                  (0 + A 0 1) * (0 + A 1 2) * (0 + A 2 3) * (0 + A 3 0) -
                                (0 + A 0 1) * (0 + A 1 3) * (0 + A 2 0) * (0 + A 3 2) +
                              (0 + A 0 1) * (0 + A 1 3) * (1 + A 2 2) * (0 + A 3 0) +
                            (0 + A 0 2) * (0 + A 1 0) * (0 + A 2 1) * (1 + A 3 3) -
                          (0 + A 0 2) * (0 + A 1 0) * (0 + A 2 3) * (0 + A 3 1) -
                        (0 + A 0 2) * (1 + A 1 1) * (0 + A 2 0) * (1 + A 3 3) +
                      (0 + A 0 2) * (1 + A 1 1) * (0 + A 2 3) * (0 + A 3 0) +
                    (0 + A 0 2) * (0 + A 1 3) * (0 + A 2 0) * (0 + A 3 1) -
                  (0 + A 0 2) * (0 + A 1 3) * (0 + A 2 1) * (0 + A 3 0) -
                (0 + A 0 3) * (0 + A 1 0) * (0 + A 2 1) * (0 + A 3 2) +
              (0 + A 0 3) * (0 + A 1 0) * (1 + A 2 2) * (0 + A 3 1) +
            (0 + A 0 3) * (1 + A 1 1) * (0 + A 2 0) * (0 + A 3 2) -
          (0 + A 0 3) * (1 + A 1 1) * (1 + A 2 2) * (0 + A 3 0) -
        (0 + A 0 3) * (0 + A 1 2) * (0 + A 2 0) * (0 + A 3 1) +
      (0 + A 0 3) * (0 + A 1 2) * (0 + A 2 1) * (0 + A 3 0) =
    A 0 0 + A 1 1 + A 2 2 + A 3 3 + A 0 0 * A 1 1 - A 0 1 * A 1 0 + A 0 0 * A 2 2 - A 0 2 * A 2 0 + A 0 0 * A 3 3 -
                                                                                                                    A 0
                                                                                                                        3 *
                                                                                                                      A
                                                                                                                        3
                                                                                                                        0 +
                                                                                                                  A 1
                                                                                                                      1 *
                                                                                                                    A 2
                                                                                                                      2 -
                                                                                                                A 1 2 *
                                                                                                                  A 2
                                                                                                                    1 +
                                                                                                              A 1 1 *
                                                                                                                A 3 3 -
                                                                                                            A 1 3 *
                                                                                                              A 3 1 +
                                                                                                          A 2 2 *
                                                                                                            A 3 3 -
                                                                                                        A 2 3 * A 3 2 +
                                                                                                      A 0 0 * A 1 1 *
                                                                                                        A 2 2 -
                                                                                                    A 0 0 * A 1 2 *
                                                                                                      A 2 1 -
                                                                                                  A 0 1 * A 1 0 *
                                                                                                    A 2 2 +
                                                                                                A 0 1 * A 1 2 * A 2 0 +
                                                                                              A 0 2 * A 1 0 * A 2 1 -
                                                                                            A 0 2 * A 1 1 * A 2 0 +
                                                                                          A 0 0 * A 1 1 * A 3 3 -
                                                                                        A 0 0 * A 1 3 * A 3 1 -
                                                                                      A 0 1 * A 1 0 * A 3 3 +
                                                                                    A 0 1 * A 1 3 * A 3 0 +
                                                                                  A 0 3 * A 1 0 * A 3 1 -
                                                                                A 0 3 * A 1 1 * A 3 0 +
                                                                              A 0 0 * A 2 2 * A 3 3 -
                                                                            A 0 0 * A 2 3 * A 3 2 -
                                                                          A 0 2 * A 2 0 * A 3 3 +
                                                                        A 0 2 * A 2 3 * A 3 0 +
                                                                      A 0 3 * A 2 0 * A 3 2 -
                                                                    A 0 3 * A 2 2 * A 3 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 +
                                                      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 +
      1