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 + (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))))
Tactic:
simp_rw [Matrix.one_apply]
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 *
                  (((((if True then 1 else 0) + A 0 0) * if True then 1 else 0) +
                      ((if True then 1 else 0) + A 0 0) * A 1 1) *
                    if True then 1 else 0) +
                2 *
                  (((((if True then 1 else 0) + A 0 0) * if True then 1 else 0) +
                      ((if True then 1 else 0) + A 0 0) * A 1 1) *
                    A 2 2) -
              (2 *
                  (((((if True then 1 else 0) + A 0 0) * if 1 = 2 then 1 else 0) +
                      ((if True then 1 else 0) + A 0 0) * A 1 2) *
                    if 2 = 1 then 1 else 0) +
                2 *
                  (((((if True then 1 else 0) + A 0 0) * if 1 = 2 then 1 else 0) +
                      ((if True then 1 else 0) + A 0 0) * A 1 2) *
                    A 2 1)) -
            (2 *
                (((((if 0 = 1 then 1 else 0) + A 0 1) * if 1 = 0 then 1 else 0) +
                    ((if 0 = 1 then 1 else 0) + A 0 1) * A 1 0) *
                  if True then 1 else 0) +
              2 *
                (((((if 0 = 1 then 1 else 0) + A 0 1) * if 1 = 0 then 1 else 0) +
                    ((if 0 = 1 then 1 else 0) + A 0 1) * A 1 0) *
                  A 2 2)) +
          (2 *
              (((((if 0 = 1 then 1 else 0) + A 0 1) * if 1 = 2 then 1 else 0) +
                  ((if 0 = 1 then 1 else 0) + A 0 1) * A 1 2) *
                if 2 = 0 then 1 else 0) +
            2 *
              (((((if 0 = 1 then 1 else 0) + A 0 1) * if 1 = 2 then 1 else 0) +
                  ((if 0 = 1 then 1 else 0) + A 0 1) * A 1 2) *
                A 2 0)) +
        (2 *
            (((((if 0 = 2 then 1 else 0) + A 0 2) * if 1 = 0 then 1 else 0) +
                ((if 0 = 2 then 1 else 0) + A 0 2) * A 1 0) *
              if 2 = 1 then 1 else 0) +
          2 *
            (((((if 0 = 2 then 1 else 0) + A 0 2) * if 1 = 0 then 1 else 0) +
                ((if 0 = 2 then 1 else 0) + A 0 2) * A 1 0) *
              A 2 1)) -
      (2 *
          (((((if 0 = 2 then 1 else 0) + A 0 2) * if True then 1 else 0) + ((if 0 = 2 then 1 else 0) + A 0 2) * A 1 1) *
            if 2 = 0 then 1 else 0) +
        2 *
          (((((if 0 = 2 then 1 else 0) + A 0 2) * if True then 1 else 0) + ((if 0 = 2 then 1 else 0) + 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))))