-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
a :
  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, ⋯⟩)
⊢ 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) (⟨1, sorry⟩ : Fin 3)) : ℕ) + (↑((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)) : ℕ)) *
    (A.submatrix (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, 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) (⟨1, 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) (⟨1, 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) (⟨1, 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) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j