Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case «0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ (-1) ^ (↑j + ↑((fun i ↦ i) ⟨0, ⋯⟩)) *
      (A.submatrix j.succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 0 0 *
          A.submatrix j.succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 1 1 -
        A.submatrix j.succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 0 1 *
          A.submatrix j.succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case «1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ (-1) ^ (↑j + ↑((fun i ↦ i) ⟨1, ⋯⟩)) *
      (A.submatrix j.succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 0 0 *
          A.submatrix j.succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 1 1 -
        A.submatrix j.succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 0 1 *
          A.submatrix j.succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨1, ⋯⟩) j

pp: case «2»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ (-1) ^ (↑j + ↑((fun i ↦ i) ⟨2, ⋯⟩)) *
      (A.submatrix j.succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 0 0 *
          A.submatrix j.succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 1 1 -
        A.submatrix j.succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 0 1 *
          A.submatrix j.succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨2, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ (-1) ^ (↑j + ↑((fun i ↦ i) ⟨0, ⋯⟩)) *
      (A.submatrix j.succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 0 0 *
          A.submatrix j.succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 1 1 -
        A.submatrix j.succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 0 1 *
          A.submatrix j.succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ (-1) ^ (↑j + ↑((fun i ↦ i) ⟨1, ⋯⟩)) *
      (A.submatrix j.succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 0 0 *
          A.submatrix j.succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 1 1 -
        A.submatrix j.succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 0 1 *
          A.submatrix j.succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨1, ⋯⟩) j

case «2»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ (-1) ^ (↑j + ↑((fun i ↦ i) ⟨2, ⋯⟩)) *
      (A.submatrix j.succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 0 0 *
          A.submatrix j.succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 1 1 -
        A.submatrix j.succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 0 1 *
          A.submatrix j.succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨2, ⋯⟩) j