awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ 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
have a : HPow.hPow (α := α) (-1)
      ((↑((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)) : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)) : ℕ)) *
    (A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)))
          (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) 0 0 *
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)))
          (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) 1 1 -
      A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)))
          (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) 0 1 *
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)))
          (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : 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, sorry⟩) ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ 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
have a : HPow.hPow (α := α) (-1)
      ((↑((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)) : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3)) : ℕ)) *
    (A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)))
          (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) 0 0 *
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)))
          (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) 1 1 -
      A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)))
          (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) 0 1 *
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)))
          (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : 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, sorry⟩) ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ 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
have a : HPow.hPow (α := α) (-1)
      ((↑((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)) : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)) : ℕ)) *
    (A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)))
          (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) 0 0 *
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)))
          (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) 1 1 -
      A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)))
          (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))) 0 1 *
        A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)))
          (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : 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, sorry⟩) ((fun (i : Fin 3) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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) (⟨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, ⋯⟩)
have 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
Tactic: simp [Fin.succAbove, Fin.lt_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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) (⟨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, ⋯⟩)
have 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
Tactic: simp [Fin.succAbove, Fin.lt_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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) (⟨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, ⋯⟩)
have 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
Tactic: simp [Fin.succAbove, Fin.lt_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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) (⟨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, ⋯⟩)
have 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
Tactic: simp [Fin.succAbove, Fin.lt_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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) (⟨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, ⋯⟩)
have 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
Tactic: simp [Fin.succAbove, Fin.lt_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (hypothesis)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
i : n
⊢ A.det = ∑ j : n, A i j * A.adjugate j i
have this : Nonempty n
Tactic: haveI : Nonempty n := ⟨i⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ A.det = ∑ j : n, A i j * A.adjugate j i
have obtain : ∀ (n' : ℕ) (hn' : Fintype.card n = n'.succ), 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ A.det = ∑ j : n, A i j * A.adjugate j i
have mk : ∀ (x : Trunc (n ≃ Fin n'.succ)) (e : n ≃ Fin n'.succ), A.det = ∑ j : n, A i j * A.adjugate j i
Tactic: obtain ⟨e⟩ := Fintype.truncEquivFinOfCardEq hn'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ A.det = ∑ j : n, A i j * A.adjugate j i
have 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)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ 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)
have 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))
Tactic: rw [det_succ_row A' (e i)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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
⊢ 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))
have 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))
Tactic: simp_rw [mul_assoc, mul_left_comm _ (A' _ _), ← adjugate_fin_succ_eq_det_submatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
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))
⊢ 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))
have 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))
Tactic: simp_rw [mul_assoc, mul_left_comm _ (A' _ _), ← adjugate_fin_succ_eq_det_submatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (hypothesis)
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
have this : Aᵀ.adjugate.map star = (Aᵀ.map star).adjugate
Tactic: have : Aᵀ.adjugate.map star = adjugate (Aᵀ.map star) := (starRingEnd α).map_adjugate Aᵀ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
inst_3 : StarRing α
A : Matrix n n α
this : Aᵀ.adjugate.map star = (Aᵀ.map star).adjugate
rw : Aᵀ.adjugate.map star = (Aᵀ.map star).adjugate
⊢ A.adjugateᵀ.map star = (Aᵀ.map star).adjugate
have rw₁ : (Aᵀ.map star).adjugate = (Aᵀ.map star).adjugate
Tactic: rw [A.adjugate_transpose, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
⊢ IsRegular A
have left : IsLeftRegular A
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
left : IsLeftRegular A
⊢ IsRegular A
have right : IsRightRegular A
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : Eq (α := Matrix n n α) ((fun (x : Matrix n n α) ↦ A * x) B) ((fun (x : Matrix n n α) ↦ A * x) C)
⊢ B = C
have left : Eq (α := Matrix n n α) ((fun (x : Matrix n n α) ↦ A.det • x) B) ((fun (x : Matrix n n α) ↦ A.det • x) C)
Tactic: refine hA.matrix ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
⊢ A.det • B = A.det • C
have left : A.det • (1 * B) = A.det • C
Tactic: rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ←
      adjugate_mul, Matrix.mul_assoc, Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
left : A.det • (1 * B) = A.det • C
⊢ A.det • B = A.det • C
have left₁ : A.det • (1 * B) = A.det • (1 * C)
Tactic: rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ←
      adjugate_mul, Matrix.mul_assoc, Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
left : A.det • (1 * B) = A.det • C
left₁ : A.det • (1 * B) = A.det • (1 * C)
⊢ A.det • B = A.det • C
have left₂ : HSMul.hSMul (β := Matrix n n α) A.det 1 * B = A.det • (1 * C)
Tactic: rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ←
      adjugate_mul, Matrix.mul_assoc, Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
left : A.det • (1 * B) = A.det • C
left₁ : A.det • (1 * B) = A.det • (1 * C)
left₂ : HSMul.hSMul (β := Matrix n n α) A.det 1 * B = A.det • (1 * C)
⊢ A.det • B = A.det • C
have left₃ : HSMul.hSMul (β := Matrix n n α) A.det 1 * B = HSMul.hSMul (β := Matrix n n α) A.det 1 * C
Tactic: rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ←
      adjugate_mul, Matrix.mul_assoc, Matrix.mul_assoc, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
n : Type v
α : Type w
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
left : A.det • (1 * B) = A.det • C
left₁ : A.det • (1 * B) = A.det • (1 * C)
left₂ : HSMul.hSMul (β := Matrix n n α) A.det 1 * B = A.det • (1 * C)
left₃ : HSMul.hSMul (β := Matrix n n α) A.det 1 * B = HSMul.hSMul (β := Matrix n n α) A.det 1 * C
⊢ A.det • B = A.det • C
have left₄ : A.adjugate * A * B = A.adjugate * A * C
Tactic: rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ←
      adjugate_mul, Matrix.mul_assoc, Matrix.mul_assoc, h]