Theorem: MatrixCookbook.eq_27
Proof state before:
ι : Type ?u.74781
R : Type u_1
m : Type ?u.74787
n : Type ?u.74790
p : Type ?u.74793
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : Fintype p
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Field R
A : Matrix (Fin 4) (Fin 4) R
inst✝ : CharZero R
⊢ (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) *
      (2 * 6) =
    ((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) +
              (A 0 0 + A 1 1 + A 2 2 + A 3 3)) *
            2 +
          (A 0 0 ^ 2 + A 1 1 ^ 2 + A 2 2 ^ 2 + A 3 3 ^ 2 + 2 * A 0 0 * A 1 1 + 2 * A 0 0 * A 2 2 + 2 * A 0 0 * A 3 3 +
                  2 * A 1 1 * A 2 2 +
                2 * A 1 1 * A 3 3 +
              2 * A 2 2 * A 3 3 -
            (A 0 0 ^ 2 + A 1 1 ^ 2 + A 2 2 ^ 2 + A 3 3 ^ 2 + 2 * A 0 1 * A 1 0 + 2 * A 0 2 * A 2 0 + 2 * A 0 3 * A 3 0 +
                  2 * A 1 2 * A 2 1 +
                2 * A 1 3 * A 3 1 +
              2 * A 2 3 * A 3 2))) *
        6 +
      ((A 0 0 + A 1 1 + A 2 2 + A 3 3) ^ 3 -
            3 * (A 0 0 + A 1 1 + A 2 2 + A 3 3) *
              (A 0 0 ^ 2 + A 1 1 ^ 2 + A 2 2 ^ 2 + A 3 3 ^ 2 + 2 * A 0 1 * A 1 0 + 2 * A 0 2 * A 2 0 +
                      2 * A 0 3 * A 3 0 +
                    2 * A 1 2 * A 2 1 +
                  2 * A 1 3 * A 3 1 +
                2 * A 2 3 * A 3 2) +
          2 *
            (A 0 0 * (A 0 0 ^ 2 + A 0 1 * A 1 0 + A 0 2 * A 2 0 + A 0 3 * A 3 0) +
                                          A 1 1 * (A 1 1 ^ 2 + A 0 1 * A 1 0 + A 1 2 * A 2 1 + A 1 3 * A 3 1) +
                                        A 2 2 * (A 2 2 ^ 2 + A 0 2 * A 2 0 + A 1 2 * A 2 1 + A 2 3 * A 3 2) +
                                      A 3 3 * (A 3 3 ^ 2 + A 0 3 * A 3 0 + A 1 3 * A 3 1 + A 2 3 * A 3 2) +
                                    A 1 0 * (A 0 0 * A 0 1 + A 0 1 * A 1 1 + A 0 2 * A 2 1 + A 0 3 * A 3 1) +
                                  A 2 0 * (A 0 0 * A 0 2 + A 0 1 * A 1 2 + A 0 2 * A 2 2 + A 0 3 * A 3 2) +
                                A 0 1 * (A 0 0 * A 1 0 + A 1 0 * A 1 1 + A 1 2 * A 2 0 + A 1 3 * A 3 0) +
                              A 3 0 * (A 0 0 * A 0 3 + A 0 1 * A 1 3 + A 0 2 * A 2 3 + A 0 3 * A 3 3) +
                            A 2 1 * (A 0 2 * A 1 0 + A 1 1 * A 1 2 + A 1 2 * A 2 2 + A 1 3 * A 3 2) +
                          A 0 2 * (A 0 0 * A 2 0 + A 1 0 * A 2 1 + A 2 0 * A 2 2 + A 2 3 * A 3 0) +
                        A 3 1 * (A 0 3 * A 1 0 + A 1 1 * A 1 3 + A 1 2 * A 2 3 + A 1 3 * A 3 3) +
                      A 1 2 * (A 0 1 * A 2 0 + A 1 1 * A 2 1 + A 2 1 * A 2 2 + A 2 3 * A 3 1) +
                    A 0 3 * (A 0 0 * A 3 0 + A 1 0 * A 3 1 + A 2 0 * A 3 2 + A 3 0 * A 3 3) +
                  A 3 2 * (A 0 3 * A 2 0 + A 1 3 * A 2 1 + A 2 2 * A 2 3 + A 2 3 * A 3 3) +
                A 1 3 * (A 0 1 * A 3 0 + A 1 1 * A 3 1 + A 2 1 * A 3 2 + A 3 1 * A 3 3) +
              A 2 3 * (A 0 2 * A 3 0 + A 1 2 * A 3 1 + A 2 2 * A 3 2 + A 3 2 * A 3 3))) *
        2
Tactic:
ring
Proof state after:
no goals