Theorem: MatrixCookbook.eq_26
Proof state before:
ι : Type ?u.45702
R : Type u_1
m : Type ?u.45708
n : Type ?u.45711
p : Type ?u.45714
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : Fintype p
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Field R
A : Matrix (Fin 3) (Fin 3) R
inst✝ : Invertible 2
⊢ 2 *
      ((1 + A) 0 0 * (1 + A) 1 1 * (1 + A) 2 2 - (1 + A) 0 0 * (1 + A) 1 2 * (1 + A) 2 1 -
              (1 + A) 0 1 * (1 + A) 1 0 * (1 + A) 2 2 +
            (1 + A) 0 1 * (1 + A) 1 2 * (1 + A) 2 0 +
          (1 + A) 0 2 * (1 + A) 1 0 * (1 + A) 2 1 -
        (1 + A) 0 2 * (1 + A) 1 1 * (1 + A) 2 0) =
    2 *
      (1 +
              (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 2 2) +
          ⅟2 * ((A 0 0 + A 1 1 + A 2 2) * (A 0 0 + A 1 1 + A 2 2)) -
        ⅟2 *
          (A 0 0 * A 0 0 +
                (A 0 (Fin.succ 0) * A (Fin.succ 0) 0 +
                  (A 0 (Fin.succ 0).succ * A (Fin.succ 0).succ 0 +
                    ∑ i : Fin 0, A 0 i.succ.succ.succ * A i.succ.succ.succ 0)) +
              (A 1 0 * A 0 1 +
                (A 1 (Fin.succ 0) * A (Fin.succ 0) 1 +
                  (A 1 (Fin.succ 0).succ * A (Fin.succ 0).succ 1 +
                    ∑ i : Fin 0, A 1 i.succ.succ.succ * A i.succ.succ.succ 1))) +
            (A 2 0 * A 0 2 +
              (A 2 (Fin.succ 0) * A (Fin.succ 0) 2 +
                (A 2 (Fin.succ 0).succ * A (Fin.succ 0).succ 2 +
                  ∑ i : Fin 0, A 2 i.succ.succ.succ * A i.succ.succ.succ 2)))))
Tactic:
dsimp
Proof state after:
ι : Type ?u.45702
R : Type u_1
m : Type ?u.45708
n : Type ?u.45711
p : Type ?u.45714
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : Fintype p
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Field R
A : Matrix (Fin 3) (Fin 3) R
inst✝ : Invertible 2
⊢ 2 *
      ((OfNat.ofNat 1 0 0 + A 0 0) * (OfNat.ofNat 1 1 1 + A 1 1) * (OfNat.ofNat 1 2 2 + A 2 2) -
                (OfNat.ofNat 1 0 0 + A 0 0) * (OfNat.ofNat 1 1 2 + A 1 2) * (OfNat.ofNat 1 2 1 + A 2 1) -
              (OfNat.ofNat 1 0 1 + A 0 1) * (OfNat.ofNat 1 1 0 + A 1 0) * (OfNat.ofNat 1 2 2 + A 2 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) +
          (OfNat.ofNat 1 0 2 + A 0 2) * (OfNat.ofNat 1 1 0 + A 1 0) * (OfNat.ofNat 1 2 1 + A 2 1) -
        (OfNat.ofNat 1 0 2 + A 0 2) * (OfNat.ofNat 1 1 1 + A 1 1) * (OfNat.ofNat 1 2 0 + A 2 0)) =
    2 *
      (1 +
              (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 2 2) +
          ⅟2 * ((A 0 0 + A 1 1 + A 2 2) * (A 0 0 + A 1 1 + A 2 2)) -
        ⅟2 *
          (A 0 0 * A 0 0 +
                (A 0 1 * A 1 0 + (A 0 2 * A 2 0 + ∑ i : Fin 0, A 0 i.succ.succ.succ * A i.succ.succ.succ 0)) +
              (A 1 0 * A 0 1 +
                (A 1 1 * A 1 1 + (A 1 2 * A 2 1 + ∑ i : Fin 0, A 1 i.succ.succ.succ * A i.succ.succ.succ 1))) +
            (A 2 0 * A 0 2 +
              (A 2 1 * A 1 2 + (A 2 2 * A 2 2 + ∑ i : Fin 0, A 2 i.succ.succ.succ * A i.succ.succ.succ 2)))))