awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
a :
  HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) : ℕ)) *
      (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 0 0 *
          A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 1 1 -
        A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 0 1 *
          A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 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 : Fin 3) ↦ i) ⟨0, ⋯⟩) j
a₁ :
  HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) : ℕ)) *
      (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 0 0 *
          A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 1 1 -
        A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 0 1 *
          A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 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 : Fin 3) ↦ i) ⟨1, ⋯⟩) j
a₂ :
  HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) : ℕ)) *
      (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 0 0 *
          A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 1 1 -
        A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 0 1 *
          A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 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 : Fin 3) ↦ i) ⟨2, ⋯⟩) j
⊢ HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑i : ℕ)) *
      (A.submatrix j.succAbove i.succAbove 0 0 * A.submatrix j.succAbove i.succAbove 1 1 -
        A.submatrix j.succAbove i.succAbove 0 1 * A.submatrix j.succAbove i.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]
      i j

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 0 0 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 1 1 -
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 0 1 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 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 : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

Premises used: Fin.succAbove, Fin.lt_def
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
a : A 0 2 * A 2 1 - A 0 1 * A 2 2 = -(A 0 1 * A 2 2) + A 0 2 * A 2 1
⊢ HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 0 0 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 1 1 -
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 0 1 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 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 : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

Premises used: Fin.succAbove, Fin.lt_def
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 0 0 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 1 1 -
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 0 1 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))) 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 : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

Premises used: Fin.succAbove, Fin.lt_def
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
a : A 1 2 * A 2 0 - A 1 0 * A 2 2 = -(A 1 0 * A 2 2) + A 1 2 * A 2 0
⊢ HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 0 0 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 1 1 -
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 0 1 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 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 : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

Premises used: Fin.succAbove, Fin.lt_def
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 0 0 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 1 1 -
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 0 1 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 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 : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

Premises used: Fin.succAbove, Fin.lt_def
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
a : HPow.hPow (α := α) (β := ℕ) (-1) 3 * (A 0 0 * A 1 2 - A 0 2 * A 1 0) = -(A 0 0 * A 1 2) + A 0 2 * A 1 0
⊢ HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 0 0 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 1 1 -
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 0 1 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))) 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 : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

Premises used: Fin.succAbove, Fin.lt_def
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)) : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 0 0 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 1 1 -
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 0 1 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 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 : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

Premises used: Fin.succAbove, Fin.lt_def
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
a : HPow.hPow (α := α) (β := ℕ) (-1) 3 * (A 0 0 * A 2 1 - A 0 1 * A 2 0) = -(A 0 0 * A 2 1) + A 0 1 * A 2 0
⊢ HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)) : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 0 0 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 1 1 -
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 0 1 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 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 : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

Premises used: Fin.succAbove, Fin.lt_def
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
a : HPow.hPow (α := α) (β := ℕ) (-1) 4 * (A 0 0 * A 1 1 - A 0 1 * A 1 0) = A 0 0 * A 1 1 - A 0 1 * A 1 0
⊢ HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 0 0 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 1 1 -
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 0 1 *
          A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
            (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))) 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 : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

Premises used: Fin.succAbove, Fin.lt_def
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ A 0 2 * A 2 1 - A 0 1 * A 2 2 = -(A 0 1 * A 2 2) + A 0 2 * A 2 1

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ A 1 2 * A 2 0 - A 1 0 * A 2 2 = -(A 1 0 * A 2 2) + A 1 2 * A 2 0

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ HPow.hPow (α := α) (β := ℕ) (-1) 3 * (A 0 0 * A 1 2 - A 0 2 * A 1 0) = -(A 0 0 * A 1 2) + A 0 2 * A 1 0

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ HPow.hPow (α := α) (β := ℕ) (-1) 3 * (A 0 0 * A 2 1 - A 0 1 * A 2 0) = -(A 0 0 * A 2 1) + A 0 1 * A 2 0

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ HPow.hPow (α := α) (β := ℕ) (-1) 4 * (A 0 0 * A 1 1 - A 0 1 * A 1 0) = A 0 0 * A 1 1 - A 0 1 * A 1 0

Tactic:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
α : Type w
inst : CommRing α
a b c d e f g h i : α
⊢ Eq.{w + 1} (α := Matrix (Fin 3) (Fin 3) α) (adjugate !![a, b, c; d, e, f; g, h, i])
    !![e * i - f * h, -(b * i) + c * h, b * f - c * e;
      -(d * i) + f * g, a * i - c * g, -(a * f) + c * d;
      d * h - e * g, -(a * h) + b * g, a * e - b * d]

Tactic:
adjugate_fin_three _

Premises used: Eq.mpr, Matrix.adjugate_fin_three, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i : n
⊢ Nonempty n

Tactic:
haveI : Nonempty n := ⟨i⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
obtain : ∀ (n' : ℕ) (hn' : Fintype.card n = n'.succ), A.det = ∑ j : n, A i j * A.adjugate j i
⊢ A.det = ∑ j : n, A i j * A.adjugate j i

Tactic:
obtain ⟨n', hn'⟩ := Nat.exists_eq_succ_of_ne_zero (Fintype.card_ne_zero : Fintype.card n ≠ 0)

Premises used: Fintype.card_ne_zero, Nat.exists_eq_succ_of_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
mk : ∀ (x : Trunc (n ≃ Fin n'.succ)) (e : n ≃ Fin n'.succ), A.det = ∑ j : n, A i j * A.adjugate j i
⊢ A.det = ∑ j : n, A i j * A.adjugate j i

Tactic:
obtain ⟨e⟩ := Fintype.truncEquivFinOfCardEq hn'

Premises used: Fintype.truncEquivFinOfCardEq
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i : n
this_1 : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e : (a : Matrix n n α) → Matrix (Fin n'.succ) (Fin n'.succ) α) A
this : A'.det = ∑ j : Fin n'.succ, A' ((e : (a : n) → Fin n'.succ) i) j * A'.adjugate j ((e : (a : n) → Fin n'.succ) i)
⊢ A.det = ∑ x : n, A i x * A.adjugate x i

Tactic:
simp_rw [A', det_reindex_self, adjugate_reindex, reindex_apply, submatrix_apply, ← e.sum_comp,
      Equiv.symm_apply_apply] at this

Premises used: Equiv.symm_apply_apply, Equiv.sum_comp, Matrix.reindex_apply, Matrix.adjugate_reindex, Matrix.det_reindex_self, Matrix.submatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i : n
this_1 : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e : (a : Matrix n n α) → Matrix (Fin n'.succ) (Fin n'.succ) α) A
this : A.det = ∑ x : n, A i x * A.adjugate x i
⊢ A.det = ∑ j : n, A i j * A.adjugate j i

Tactic:
this
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i : n
this_1 : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e : (a : Matrix n n α) → Matrix (Fin n'.succ) (Fin n'.succ) α) A
this : A.det = ∑ x : n, A i x * A.adjugate x i
⊢ A.det = ∑ j : n, A i j * A.adjugate j i

Tactic:
exact this
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e : (a : Matrix n n α) → Matrix (Fin n'.succ) (Fin n'.succ) α) A
mk : A'.det = ∑ j : Fin n'.succ, A' ((e : (a : n) → Fin n'.succ) i) j * A'.adjugate j ((e : (a : n) → Fin n'.succ) i)
⊢ A.det = ∑ j : n, A i j * A.adjugate j i

Tactic:
suffices det A' = ∑ j : Fin n'.succ, A' (e i) j * adjugate A' j (e i) by
    simp_rw [A', det_reindex_self, adjugate_reindex, reindex_apply, submatrix_apply, ← e.sum_comp,
      Equiv.symm_apply_apply] at this
    exact this
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e : (a : Matrix n n α) → Matrix (Fin n'.succ) (Fin n'.succ) α) A
mk :
  Eq.{w + 1} (α := α)
    (∑ j : Fin n'.succ,
      HPow.hPow (α := α) (-1) ((↑((e : (a : n) → Fin n'.succ) i) : ℕ) + (↑j : ℕ)) *
          A' ((e : (a : n) → Fin n'.succ) i) j *
        (A'.submatrix (Fin.succAbove ((e : (a : n) → Fin n'.succ) i)) j.succAbove).det)
    (∑ j : Fin n'.succ, A' ((e : (a : n) → Fin n'.succ) i) j * A'.adjugate j ((e : (a : n) → Fin n'.succ) i))
⊢ A'.det = ∑ j : Fin n'.succ, A' ((e : (a : n) → Fin n'.succ) i) j * A'.adjugate j ((e : (a : n) → Fin n'.succ) i)

Tactic:
rw [det_succ_row A' (e i)]

Premises used: Matrix.det_succ_row, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e : (a : Matrix n n α) → Matrix (Fin n'.succ) (Fin n'.succ) α) A
mk :
  Eq.{w + 1} (α := α)
    (∑ x : Fin n'.succ,
      HPow.hPow (α := α) (-1) ((↑((e : (a : n) → Fin n'.succ) i) : ℕ) + (↑x : ℕ)) *
        (A' ((e : (a : n) → Fin n'.succ) i) x *
          (A'.submatrix (Fin.succAbove ((e : (a : n) → Fin n'.succ) i)) x.succAbove).det))
    (∑ j : Fin n'.succ, A' ((e : (a : n) → Fin n'.succ) i) j * A'.adjugate j ((e : (a : n) → Fin n'.succ) i))
mk₁ :
  Eq.{w + 1} (α := α)
    (∑ x : Fin n'.succ,
      A' ((e : (a : n) → Fin n'.succ) i) x *
        (HPow.hPow (α := α) (-1) ((↑((e : (a : n) → Fin n'.succ) i) : ℕ) + (↑x : ℕ)) *
          (A'.submatrix (Fin.succAbove ((e : (a : n) → Fin n'.succ) i)) x.succAbove).det))
    (∑ j : Fin n'.succ, A' ((e : (a : n) → Fin n'.succ) i) j * A'.adjugate j ((e : (a : n) → Fin n'.succ) i))
⊢ Eq.{w + 1} (α := α)
    (∑ j : Fin n'.succ,
      HPow.hPow (α := α) (-1) ((↑((e : (a : n) → Fin n'.succ) i) : ℕ) + (↑j : ℕ)) *
          A' ((e : (a : n) → Fin n'.succ) i) j *
        (A'.submatrix (Fin.succAbove ((e : (a : n) → Fin n'.succ) i)) j.succAbove).det)
    (∑ j : Fin n'.succ, A' ((e : (a : n) → Fin n'.succ) i) j * A'.adjugate j ((e : (a : n) → Fin n'.succ) i))

Tactic:
simp_rw [mul_assoc, mul_left_comm _ (A' _ _), ← adjugate_fin_succ_eq_det_submatrix]

Premises used: Matrix.adjugate_fin_succ_eq_det_submatrix, mul_assoc, mul_left_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
j : n
⊢ A.det = ∑ i : n, A i j * A.adjugate j i

Tactic:
simpa only [det_transpose, ← adjugate_transpose] using det_eq_sum_mul_adjugate_row Aᵀ j

Premises used: Matrix.det_transpose, Matrix.det_eq_sum_mul_adjugate_row, Matrix.transpose, Matrix.adjugate_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Adjugate
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
inst_3 : StarRing α
A : Matrix n n α
⊢ Aᵀ.adjugate.map star = (Aᵀ.map star).adjugate

Tactic:
have : Aᵀ.adjugate.map star = adjugate (Aᵀ.map star) := (starRingEnd α).map_adjugate Aᵀ