Theorem: trace_pow_three_fin_four (MatrixCookbook/Lib/TraceDetFinFour.lean)

State before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ (A ^ 3).trace =
    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)
Tactic:
simp_rw [Matrix.trace_fin_four, pow_three, mul_apply, Fin.sum_univ_four]
State after:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ A 0 0 * (A 0 0 * A 0 0 + A 0 1 * A 1 0 + A 0 2 * A 2 0 + A 0 3 * A 3 0) +
                A 0 1 * (A 1 0 * A 0 0 + A 1 1 * A 1 0 + A 1 2 * A 2 0 + A 1 3 * A 3 0) +
              A 0 2 * (A 2 0 * A 0 0 + A 2 1 * A 1 0 + A 2 2 * A 2 0 + A 2 3 * A 3 0) +
            A 0 3 * (A 3 0 * A 0 0 + A 3 1 * A 1 0 + A 3 2 * A 2 0 + A 3 3 * A 3 0) +
          (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 1 1 * (A 1 0 * A 0 1 + A 1 1 * A 1 1 + A 1 2 * A 2 1 + A 1 3 * A 3 1) +
              A 1 2 * (A 2 0 * A 0 1 + A 2 1 * A 1 1 + A 2 2 * A 2 1 + A 2 3 * A 3 1) +
            A 1 3 * (A 3 0 * A 0 1 + A 3 1 * A 1 1 + A 3 2 * A 2 1 + A 3 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 2 1 * (A 1 0 * A 0 2 + A 1 1 * A 1 2 + A 1 2 * A 2 2 + A 1 3 * A 3 2) +
            A 2 2 * (A 2 0 * A 0 2 + A 2 1 * A 1 2 + A 2 2 * A 2 2 + A 2 3 * A 3 2) +
          A 2 3 * (A 3 0 * A 0 2 + A 3 1 * A 1 2 + A 3 2 * A 2 2 + A 3 3 * A 3 2)) +
      (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 3 1 * (A 1 0 * A 0 3 + A 1 1 * A 1 3 + A 1 2 * A 2 3 + A 1 3 * A 3 3) +
          A 3 2 * (A 2 0 * A 0 3 + A 2 1 * A 1 3 + A 2 2 * A 2 3 + A 2 3 * A 3 3) +
        A 3 3 * (A 3 0 * A 0 3 + A 3 1 * A 1 3 + A 3 2 * A 2 3 + A 3 3 * A 3 3)) =
    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)

State before:
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ A 0 0 * (A 0 0 * A 0 0 + A 0 1 * A 1 0 + A 0 2 * A 2 0 + A 0 3 * A 3 0) +
                A 0 1 * (A 1 0 * A 0 0 + A 1 1 * A 1 0 + A 1 2 * A 2 0 + A 1 3 * A 3 0) +
              A 0 2 * (A 2 0 * A 0 0 + A 2 1 * A 1 0 + A 2 2 * A 2 0 + A 2 3 * A 3 0) +
            A 0 3 * (A 3 0 * A 0 0 + A 3 1 * A 1 0 + A 3 2 * A 2 0 + A 3 3 * A 3 0) +
          (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 1 1 * (A 1 0 * A 0 1 + A 1 1 * A 1 1 + A 1 2 * A 2 1 + A 1 3 * A 3 1) +
              A 1 2 * (A 2 0 * A 0 1 + A 2 1 * A 1 1 + A 2 2 * A 2 1 + A 2 3 * A 3 1) +
            A 1 3 * (A 3 0 * A 0 1 + A 3 1 * A 1 1 + A 3 2 * A 2 1 + A 3 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 2 1 * (A 1 0 * A 0 2 + A 1 1 * A 1 2 + A 1 2 * A 2 2 + A 1 3 * A 3 2) +
            A 2 2 * (A 2 0 * A 0 2 + A 2 1 * A 1 2 + A 2 2 * A 2 2 + A 2 3 * A 3 2) +
          A 2 3 * (A 3 0 * A 0 2 + A 3 1 * A 1 2 + A 3 2 * A 2 2 + A 3 3 * A 3 2)) +
      (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 3 1 * (A 1 0 * A 0 3 + A 1 1 * A 1 3 + A 1 2 * A 2 3 + A 1 3 * A 3 3) +
          A 3 2 * (A 2 0 * A 0 3 + A 2 1 * A 1 3 + A 2 2 * A 2 3 + A 2 3 * A 3 3) +
        A 3 3 * (A 3 0 * A 0 3 + A 3 1 * A 1 3 + A 3 2 * A 2 3 + A 3 3 * A 3 3)) =
    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)
Tactic:
ring
State after:
no goals