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