Theorem: MatrixCookbook.eq_26 (MatrixCookbook/1Basic.lean)

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
⊢ (1 + A).det = 1 + A.det + A.trace + ⅟2 * A.trace ^ 2 - ⅟2 * (A ^ 2).trace
Tactic:
apply mul_left_cancel₀ (isUnit_of_invertible (2 : R)).ne_zero
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 * (1 + A).det = 2 * (1 + A.det + A.trace + ⅟2 * A.trace ^ 2 - ⅟2 * (A ^ 2).trace)

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).det = 2 * (1 + A.det + A.trace + ⅟2 * A.trace ^ 2 - ⅟2 * (A ^ 2).trace)
Tactic:
simp only [det_fin_three, trace_fin_three, pow_two, Matrix.mul_apply,
  Fin.sum_univ_succ, Matrix.one_apply]
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 *
      ((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)))))

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
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)))))

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]
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))))

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]
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))))

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 *
                  (((((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))))
Tactic:
simp (config := {decide := true})
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 * (1 + A 0 0 + (1 + A 0 0) * A 1 1) + 2 * ((1 + A 0 0 + (1 + A 0 0) * A 1 1) * A 2 2) -
              2 * ((1 + A 0 0) * A 1 2 * A 2 1) -
            (2 * (A 0 1 * A 1 0) + 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 0 2 * A 1 1) * A 2 0) =
    2 +
            (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) + (A 1 0 * A 0 1 + (A 1 1 * A 1 1 + A 1 2 * A 2 1)) +
        (A 2 0 * A 0 2 + (A 2 1 * A 1 2 + A 2 2 * A 2 2)))

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 0 0) * A 1 1) + 2 * ((1 + A 0 0 + (1 + A 0 0) * A 1 1) * A 2 2) -
              2 * ((1 + A 0 0) * A 1 2 * A 2 1) -
            (2 * (A 0 1 * A 1 0) + 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 0 2 * A 1 1) * A 2 0) =
    2 +
            (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) + (A 1 0 * A 0 1 + (A 1 1 * A 1 1 + A 1 2 * A 2 1)) +
        (A 2 0 * A 0 2 + (A 2 1 * A 1 2 + A 2 2 * A 2 2)))
Tactic:
ring
State after:
no goals