rw [trace_fin_four, pow_two]
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ A.trace ^ 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
R : Type u_1
inst✝ : CommRing R
A : Matrix (Fin 4) (Fin 4) R
⊢ (A 0 0 + A 1 1 + A 2 2 + A 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 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