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 *
      ((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)))))
Tactic:
simp only [mul_add, mul_sub, mul_invOf_self_assoc]
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 + (OfNat.ofNat 1 0 0 + A 0 0) * A 1 1) * OfNat.ofNat 1 2 2) +
                2 * (((OfNat.ofNat 1 0 0 + A 0 0) * OfNat.ofNat 1 1 1 + (OfNat.ofNat 1 0 0 + A 0 0) * A 1 1) * A 2 2) -
              (2 *
                  (((OfNat.ofNat 1 0 0 + A 0 0) * OfNat.ofNat 1 1 2 + (OfNat.ofNat 1 0 0 + A 0 0) * A 1 2) *
                    OfNat.ofNat 1 2 1) +
                2 * (((OfNat.ofNat 1 0 0 + A 0 0) * OfNat.ofNat 1 1 2 + (OfNat.ofNat 1 0 0 + A 0 0) * A 1 2) * A 2 1)) -
            (2 *
                (((OfNat.ofNat 1 0 1 + A 0 1) * OfNat.ofNat 1 1 0 + (OfNat.ofNat 1 0 1 + A 0 1) * A 1 0) *
                  OfNat.ofNat 1 2 2) +
              2 * (((OfNat.ofNat 1 0 1 + A 0 1) * OfNat.ofNat 1 1 0 + (OfNat.ofNat 1 0 1 + A 0 1) * A 1 0) * A 2 2)) +
          (2 *
              (((OfNat.ofNat 1 0 1 + A 0 1) * OfNat.ofNat 1 1 2 + (OfNat.ofNat 1 0 1 + A 0 1) * A 1 2) *
                OfNat.ofNat 1 2 0) +
            2 * (((OfNat.ofNat 1 0 1 + A 0 1) * OfNat.ofNat 1 1 2 + (OfNat.ofNat 1 0 1 + A 0 1) * A 1 2) * A 2 0)) +
        (2 *
            (((OfNat.ofNat 1 0 2 + A 0 2) * OfNat.ofNat 1 1 0 + (OfNat.ofNat 1 0 2 + A 0 2) * A 1 0) *
              OfNat.ofNat 1 2 1) +
          2 * (((OfNat.ofNat 1 0 2 + A 0 2) * OfNat.ofNat 1 1 0 + (OfNat.ofNat 1 0 2 + A 0 2) * A 1 0) * A 2 1)) -
      (2 *
          (((OfNat.ofNat 1 0 2 + A 0 2) * OfNat.ofNat 1 1 1 + (OfNat.ofNat 1 0 2 + A 0 2) * A 1 1) *
            OfNat.ofNat 1 2 0) +
        2 * (((OfNat.ofNat 1 0 2 + A 0 2) * OfNat.ofNat 1 1 1 + (OfNat.ofNat 1 0 2 + A 0 2) * A 1 1) * A 2 0)) =
    2 * 1 +
            (2 * (A 0 0 * A 1 1 * A 2 2) - 2 * (A 0 0 * A 1 2 * A 2 1) - 2 * (A 0 1 * A 1 0 * A 2 2) +
                  2 * (A 0 1 * A 1 2 * A 2 0) +
                2 * (A 0 2 * A 1 0 * A 2 1) -
              2 * (A 0 2 * A 1 1 * A 2 0)) +
          (2 * A 0 0 + 2 * A 1 1 + 2 * A 2 2) +
        ((A 0 0 + A 1 1 + A 2 2) * A 0 0 + (A 0 0 + A 1 1 + A 2 2) * A 1 1 + (A 0 0 + A 1 1 + A 2 2) * A 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))))