awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
rw :
  det.{w, v} (n := n)
      (adjugate
        ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ))) =
    HPow.hPow (α := α)
      (det.{w, v} (n := n)
        ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ)))
      (Fintype.card n - 1)
rw₁ :
  det.{w, v} (n := n)
      ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
          (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
        (adjugate (mvPolynomialX n n ℤ))) =
    HPow.hPow (α := α)
      (det.{w, v} (n := n)
        ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ)))
      (Fintype.card n - 1)
rw₂ :
  ((MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2 :
          AlgHom.{0, v, w} ℤ (MvPolynomial (n × n) ℤ) α) :
        (a : MvPolynomial (n × n) ℤ) → α)
      (det (adjugate (mvPolynomialX n n ℤ))) =
    HPow.hPow (α := α)
      (det.{w, v} (n := n)
        ((AlgHom.mapMatrix (MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2) :
            (a : Matrix n n (MvPolynomial (n × n) ℤ)) → Matrix n n α)
          (mvPolynomialX n n ℤ)))
      (Fintype.card n - 1)
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)
have rw₃ : ((MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2 :
        AlgHom.{0, v, w} ℤ (MvPolynomial (n × n) ℤ) α) :
      (a : MvPolynomial (n × n) ℤ) → α)
    (det (adjugate (mvPolynomialX n n ℤ))) =
  HPow.hPow (α := α)
    (((MvPolynomial.aeval.{0, w, v} (R := ℤ) (S₁ := α) fun (p : n × n) ↦ A p.1 p.2 :
            AlgHom.{0, v, w} ℤ (MvPolynomial (n × n) ℤ) α) :
          (a : MvPolynomial (n × n) ℤ) → α)
        (det (mvPolynomialX n n ℤ)) :
      α)
    (Fintype.card n - 1)
Tactic: rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_det, ←
      AlgHom.map_det, ← map_pow, 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)
have inr : A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
Tactic: suffices A'.adjugate.det = A'.det ^ (Fintype.card n - 1) by
    rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_det, ←
      AlgHom.map_det, ← map_pow, 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
have inr : A'.det * A'.adjugate.det = A'.det * A'.det ^ (Fintype.card n - 1)
Tactic: apply mul_left_cancel₀ (show A'.det ≠ 0 from det_mvPolynomialX_ne_zero n ℤ)
-- 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ (A' * A'.adjugate).det = A'.det ^ Fintype.card n
have rw : (HSMul.hSMul (β := Matrix n n (MvPolynomial (n × n) ℤ)) A'.det 1).det = A'.det ^ Fintype.card n
Tactic: rw [mul_adjugate A', det_smul, det_one, mul_one]
-- 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
rw : (HSMul.hSMul (β := Matrix n n (MvPolynomial (n × n) ℤ)) A'.det 1).det = A'.det ^ Fintype.card n
⊢ (A' * A'.adjugate).det = A'.det ^ Fintype.card n
have rw₁ : A'.det ^ Fintype.card n * det (n := n) 1 = A'.det ^ Fintype.card n
Tactic: rw [mul_adjugate A', det_smul, det_one, mul_one]
-- 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
rw : (HSMul.hSMul (β := Matrix n n (MvPolynomial (n × n) ℤ)) A'.det 1).det = A'.det ^ Fintype.card n
rw₁ : A'.det ^ Fintype.card n * det (n := n) 1 = A'.det ^ Fintype.card n
⊢ (A' * A'.adjugate).det = A'.det ^ Fintype.card n
have rw₂ : A'.det ^ Fintype.card n * 1 = A'.det ^ Fintype.card n
Tactic: rw [mul_adjugate A', det_smul, det_one, mul_one]
-- 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
rw : (HSMul.hSMul (β := Matrix n n (MvPolynomial (n × n) ℤ)) A'.det 1).det = A'.det ^ Fintype.card n
rw₁ : A'.det ^ Fintype.card n * det (n := n) 1 = A'.det ^ Fintype.card n
rw₂ : A'.det ^ Fintype.card n * 1 = A'.det ^ Fintype.card n
⊢ (A' * A'.adjugate).det = A'.det ^ Fintype.card n
have rw₃ : A'.det ^ Fintype.card n = A'.det ^ Fintype.card n
Tactic: rw [mul_adjugate A', det_smul, det_one, mul_one]
-- 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.det ^ Fintype.card n = A'.det * A'.det ^ (Fintype.card n - 1)
have rw : A'.det ^ Fintype.card n = A'.det ^ (Fintype.card n - 1 + 1)
Tactic: rw [← pow_succ', h_card]
-- 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
rw : A'.det ^ Fintype.card n = A'.det ^ (Fintype.card n - 1 + 1)
⊢ A'.det ^ Fintype.card n = A'.det * A'.det ^ (Fintype.card n - 1)
have rw₁ : A'.det ^ Fintype.card n = A'.det ^ Fintype.card n
Tactic: rw [← pow_succ', h_card]
-- 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.det * A'.adjugate.det = A'.det * A'.det ^ (Fintype.card n - 1)
have adjugate : (A' * A'.adjugate).det = A'.det ^ Fintype.card n
Tactic: calc
    A'.det * A'.adjugate.det = (A' * adjugate A').det := (det_mul _ _).symm
    _ = A'.det ^ Fintype.card n := by rw [mul_adjugate A', det_smul, det_one, mul_one]
    _ = A'.det * A'.det ^ (Fintype.card n - 1) := by rw [← pow_succ', h_card]
-- 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 α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
adjugate : (A' * A'.adjugate).det = A'.det ^ Fintype.card n
⊢ A'.det * A'.adjugate.det = A'.det * A'.det ^ (Fintype.card n - 1)
have adjugate₁ : A'.det ^ Fintype.card n = A'.det * A'.det ^ (Fintype.card n - 1)
Tactic: calc
    A'.det * A'.adjugate.det = (A' * adjugate A').det := (det_mul _ _).symm
    _ = A'.det ^ Fintype.card n := by rw [mul_adjugate A', det_smul, det_one, mul_one]
    _ = A'.det * A'.det ^ (Fintype.card n - 1) := by rw [← pow_succ', h_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
α : Type w
inst : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ A.adjugate i j = HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑i : ℕ)) * (A.submatrix j.succAbove i.succAbove).det
have simp_rw : ∑ x : Fin n.succ,
    HMul.hMul (β := α) (HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑x : ℕ)))
        (Pi.single (M := fun (a : Fin n.succ) ↦ α) i 1 x : α) *
      (A.submatrix j.succAbove x.succAbove).det =
  HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑i : ℕ)) * (A.submatrix j.succAbove i.succAbove).det
Tactic: simp_rw [adjugate_apply, det_succ_row _ j, updateRow_self, submatrix_updateRow_succAbove]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
α : Type w
inst : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ ∑ x : Fin n.succ,
      HMul.hMul (β := α) (HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑x : ℕ)))
          (Pi.single (M := fun (a : Fin n.succ) ↦ α) i 1 x : α) *
        (A.submatrix j.succAbove x.succAbove).det =
    HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑i : ℕ)) * (A.submatrix j.succAbove i.succAbove).det
have rw : ∀ (h : Fin n.succ) (hjk : h ≠ i),
  HMul.hMul (β := α) (HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑h : ℕ)))
        (Pi.single (M := fun (a : Fin n.succ) ↦ α) i 1 h : α) *
      (A.submatrix j.succAbove h.succAbove).det =
    0
Tactic: rw [Fintype.sum_eq_single i fun h hjk => ?_, Pi.single_eq_same, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
α : Type w
inst : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
⊢ HMul.hMul (β := α) (HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑h : ℕ)))
        (Pi.single (M := fun (a : Fin n.succ) ↦ α) i 1 h : α) *
      (A.submatrix j.succAbove h.succAbove).det =
    0
have rw : HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑h : ℕ)) * 0 * (A.submatrix j.succAbove h.succAbove).det = 0
Tactic: rw [Pi.single_eq_of_ne hjk, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
α : Type w
inst : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
rw : HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑h : ℕ)) * 0 * (A.submatrix j.succAbove h.succAbove).det = 0
⊢ HMul.hMul (β := α) (HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑h : ℕ)))
        (Pi.single (M := fun (a : Fin n.succ) ↦ α) i 1 h : α) *
      (A.submatrix j.succAbove h.succAbove).det =
    0
have rw₁ : 0 * (A.submatrix j.succAbove h.succAbove).det = 0
Tactic: rw [Pi.single_eq_of_ne hjk, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
α : Type w
inst : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
rw : HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑h : ℕ)) * 0 * (A.submatrix j.succAbove h.succAbove).det = 0
rw₁ : 0 * (A.submatrix j.succAbove h.succAbove).det = 0
⊢ HMul.hMul (β := α) (HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑h : ℕ)))
        (Pi.single (M := fun (a : Fin n.succ) ↦ α) i 1 h : α) *
      (A.submatrix j.succAbove h.succAbove).det =
    0
have rw₂ : Eq.{w + 1} (α := α) 0 0
Tactic: rw [Pi.single_eq_of_ne hjk, mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ A.adjugate = !![A 1 1, -A 0 1; -A 1 0, A 0 0]
have a : ∀ (i j : Fin 2), A.adjugate i j = !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ A.adjugate i j = !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j
have a : HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑i : ℕ)) * (A.submatrix j.succAbove i.succAbove).det =
  !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j
Tactic: rw [adjugate_fin_succ_eq_det_submatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑i : ℕ)) * (A.submatrix j.succAbove i.succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j
have a : HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) : ℕ)) *
    (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)))).det =
  !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
a :
  HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
⊢ HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑i : ℕ)) * (A.submatrix j.succAbove i.succAbove).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j
have a₁ : HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) : ℕ)) *
    (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)))).det =
  !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Adjugate (goal)
Goal:
α : Type w
inst : CommRing α
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have a : HPow.hPow (α := α) (-1)
      ((↑((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) : ℕ)) *
    (A.submatrix (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)))
        (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)))).det =
  !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ 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 2) (Fin 2) α
j : Fin 2
a :
  HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))
          (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have a₁ : HPow.hPow (α := α) (-1)
      ((↑((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) : ℕ)) *
    (A.submatrix (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)))
        (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)))).det =
  !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, 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 2) (Fin 2) α
j : Fin 2
⊢ HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have a : HPow.hPow (α := α) (-1)
      ((↑((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) : ℕ)) *
    (A.submatrix (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)))
        (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)))).det =
  !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ 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 2) (Fin 2) α
j : Fin 2
a :
  HPow.hPow (α := α) (-1)
        ((↑((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)))
          (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ HPow.hPow (α := α) (-1) ((↑j : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) : ℕ)) *
      (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)))).det =
    !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have a₁ : HPow.hPow (α := α) (-1)
      ((↑((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) : ℕ) + (↑((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) : ℕ)) *
    (A.submatrix (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)))
        (Fin.succAbove ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)))).det =
  !![A 1 1, -A 0 1; -A 1 0, A 0 0] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, 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) α
⊢ A.adjugate =
    !![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]
have a : ∀ (i j : Fin 3),
  A.adjugate i j =
    !![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: ext i j
-- 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.adjugate i j =
    !![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 : ℕ) + (↑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: rw [adjugate_fin_succ_eq_det_submatrix, det_fin_two]
-- 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
⊢ 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) (⟨0, sorry⟩ : Fin 3)) : ℕ)) *
    (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) 0 0 *
        A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) 1 1 -
      A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))) 0 1 *
        A.submatrix j.succAbove (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⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
⊢ 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) (⟨1, sorry⟩ : Fin 3)) : ℕ)) *
    (A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) 0 0 *
        A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) 1 1 -
      A.submatrix j.succAbove (Fin.succAbove ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))) 0 1 *
        A.submatrix j.succAbove (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⟩) j
Tactic: fin_cases i
Cleared hypotheses: i