awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i_1 : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ i_1
i : Fin n
this : HPow.hPow (α := R) (-1) (↑i : ℕ) = (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) i.cycleRange) : ℤ) : R)
σ : Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Perm (Fin n))) univ σ
⊢ HSMul.hSMul (β := R) (HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) σ : ℤˣ))
      (∏ x : Fin n.succ,
        A
          ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, σ) :
                Perm (Fin n.succ)) :
              (a : Fin n.succ) → Fin n.succ)
            x)
          x) =
    -1 *
      (A i.succ 0 *
        HSMul.hSMul (α := ℤˣ) (β := R) ((sign : (a : Perm (Fin n)) → ℤˣ) σ : ℤˣ)
          (∏ i_2 : Fin n,
            submatrix (l := Fin n) (m := Fin n)
              ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i_3 j : Fin n) ↦
                A (i.succ.succAbove i_3) j.succ)
              ((⇑i.cycleRange : (a : Fin n) → Fin n) : (a : Fin n) → Fin n) id ((σ : (a : Fin n) → Fin n) i_2 : Fin n)
              i_2))
have σ₁ : HSMul.hSMul (β := R) (HMul.hMul (α := ℤ) (-1) (↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ))
    (∏ i' : Fin n.succ,
      A
        ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, σ) :
              Perm (Fin n.succ)) :
            (a : Fin n.succ) → Fin n.succ)
          i')
        i') =
  HMul.hMul (α := ℤ) (-1) (↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) •
    (A i.succ 0 *
      ∏ i' : Fin n, A (i.succ.succAbove ((i.cycleRange : (a : Fin n) → Fin n) ((σ : (a : Fin n) → Fin n) i'))) i'.succ)
Tactic: calc
    ((-1 * Perm.sign σ : ℤ) • ∏ i', A (Perm.decomposeFin.symm (Fin.succ i, σ) i') i') =
        (-1 * Perm.sign σ : ℤ) • (A (Fin.succ i) 0 *
          ∏ i', A ((Fin.succ i).succAbove (Fin.cycleRange i (σ i'))) i'.succ) := by
      simp only [Fin.prod_univ_succ, Fin.succAbove_cycleRange,
        Equiv.Perm.decomposeFin_symm_apply_zero, Equiv.Perm.decomposeFin_symm_apply_succ]
    _ = -1 * (A (Fin.succ i) 0 * (Perm.sign σ : ℤ) •
        ∏ i', A ((Fin.succ i).succAbove (Fin.cycleRange i (σ i'))) i'.succ) := by
      simp [_root_.neg_mul, one_mul, zsmul_eq_mul, neg_smul,
        Fin.succAbove_cycleRange, mul_left_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i_1 : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ i_1
i : Fin n
this : HPow.hPow (α := R) (-1) (↑i : ℕ) = (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) i.cycleRange) : ℤ) : R)
σ : Perm (Fin n)
h_1 : Membership.mem (γ := Finset (Perm (Fin n))) univ σ
σ₁ :
  HSMul.hSMul (β := R) (HMul.hMul (α := ℤ) (-1) (↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ))
      (∏ i' : Fin n.succ,
        A
          ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, σ) :
                Perm (Fin n.succ)) :
              (a : Fin n.succ) → Fin n.succ)
            i')
          i') =
    HMul.hMul (α := ℤ) (-1) (↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) •
      (A i.succ 0 *
        ∏ i' : Fin n,
          A (i.succ.succAbove ((i.cycleRange : (a : Fin n) → Fin n) ((σ : (a : Fin n) → Fin n) i'))) i'.succ)
⊢ HSMul.hSMul (β := R) (HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) σ : ℤˣ))
      (∏ x : Fin n.succ,
        A
          ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, σ) :
                Perm (Fin n.succ)) :
              (a : Fin n.succ) → Fin n.succ)
            x)
          x) =
    -1 *
      (A i.succ 0 *
        HSMul.hSMul (α := ℤˣ) (β := R) ((sign : (a : Perm (Fin n)) → ℤˣ) σ : ℤˣ)
          (∏ i_2 : Fin n,
            submatrix (l := Fin n) (m := Fin n)
              ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i_3 j : Fin n) ↦
                A (i.succ.succAbove i_3) j.succ)
              ((⇑i.cycleRange : (a : Fin n) → Fin n) : (a : Fin n) → Fin n) id ((σ : (a : Fin n) → Fin n) i_2 : Fin n)
              i_2))
have σ₂ : HMul.hMul (α := ℤ) (-1) (↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) •
    (A i.succ 0 *
      ∏ i' : Fin n,
        A (i.succ.succAbove ((i.cycleRange : (a : Fin n) → Fin n) ((σ : (a : Fin n) → Fin n) i'))) i'.succ) =
  -1 *
    (A i.succ 0 *
      HSMul.hSMul (α := ℤ) (β := R) (↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ)
        (∏ i' : Fin n,
          A (i.succ.succAbove ((i.cycleRange : (a : Fin n) → Fin n) ((σ : (a : Fin n) → Fin n) i'))) i'.succ))
Tactic: calc
    ((-1 * Perm.sign σ : ℤ) • ∏ i', A (Perm.decomposeFin.symm (Fin.succ i, σ) i') i') =
        (-1 * Perm.sign σ : ℤ) • (A (Fin.succ i) 0 *
          ∏ i', A ((Fin.succ i).succAbove (Fin.cycleRange i (σ i'))) i'.succ) := by
      simp only [Fin.prod_univ_succ, Fin.succAbove_cycleRange,
        Equiv.Perm.decomposeFin_symm_apply_zero, Equiv.Perm.decomposeFin_symm_apply_succ]
    _ = -1 * (A (Fin.succ i) 0 * (Perm.sign σ : ℤ) •
        ∏ i', A ((Fin.succ i).succAbove (Fin.cycleRange i (σ i'))) i'.succ) := by
      simp [_root_.neg_mul, one_mul, zsmul_eq_mul, neg_smul,
        Fin.succAbove_cycleRange, mul_left_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ A.det = ∑ j : Fin n.succ, HPow.hPow (α := R) (-1) (↑j : ℕ) * A 0 j * (A.submatrix Fin.succ j.succAbove).det
have rw : Eq.{v + 1} (α := R)
  (∑ i : Fin n.succ, HPow.hPow (α := R) (-1) (↑i : ℕ) * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det)
  (∑ j : Fin n.succ, HPow.hPow (α := R) (-1) (↑j : ℕ) * A 0 j * (A.submatrix Fin.succ j.succAbove).det)
Tactic: rw [← det_transpose A, det_succ_column_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ Eq.{v + 1} (α := R)
    (∑ i : Fin n.succ, HPow.hPow (α := R) (-1) (↑i : ℕ) * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det)
    (∑ j : Fin n.succ, HPow.hPow (α := R) (-1) (↑j : ℕ) * A 0 j * (A.submatrix Fin.succ j.succAbove).det)
have refine : ∀ (i : Fin n.succ),
  Membership.mem (γ := Finset (Fin n.succ)) univ i →
    HPow.hPow (α := R) (-1) (↑i : ℕ) * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det =
      HPow.hPow (α := R) (-1) (↑i : ℕ) * A 0 i * (A.submatrix Fin.succ i.succAbove).det
Tactic: refine Finset.sum_congr rfl fun i _ => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ i
⊢ HPow.hPow (α := R) (-1) (↑i : ℕ) * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det =
    HPow.hPow (α := R) (-1) (↑i : ℕ) * A 0 i * (A.submatrix Fin.succ i.succAbove).det
have rw : HPow.hPow (α := R) (-1) (↑i : ℕ) * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ)ᵀ.det =
  HPow.hPow (α := R) (-1) (↑i : ℕ) * A 0 i * (A.submatrix Fin.succ i.succAbove).det
Tactic: rw [← det_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det =
    ∑ j : Fin n.succ, HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
have simp_rw : A.det =
  HPow.hPow (α := R) (-1) (↑i : ℕ) *
    ∑ i_1 : Fin n.succ, HPow.hPow (α := R) (-1) (↑i_1 : ℕ) * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
Tactic: simp_rw [pow_add, mul_assoc, ← mul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det =
    HPow.hPow (α := R) (-1) (↑i : ℕ) * (↑(↑((sign : (a : Perm (Fin n.succ)) → ℤˣ) i.cycleRange⁻¹) : ℤ) : R) * A.det
have det : A.det = (↑(↑(HPow.hPow (α := ℤˣ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤˣ) (-1) (↑i : ℕ)) : ℤ) : R) * A.det
Tactic: calc
      det A = ↑((-1 : ℤˣ) ^ (i : ℕ) * (-1 : ℤˣ) ^ (i : ℕ) : ℤˣ) * det A := by simp
      _ = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by simp [-Int.units_mul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
det : A.det = (↑(↑(HPow.hPow (α := ℤˣ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤˣ) (-1) (↑i : ℕ)) : ℤ) : R) * A.det
⊢ A.det =
    HPow.hPow (α := R) (-1) (↑i : ℕ) * (↑(↑((sign : (a : Perm (Fin n.succ)) → ℤˣ) i.cycleRange⁻¹) : ℤ) : R) * A.det
have det₁ : (↑(↑(HPow.hPow (α := ℤˣ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤˣ) (-1) (↑i : ℕ)) : ℤ) : R) * A.det =
  HPow.hPow (α := R) (-1) (↑i : ℕ) * (↑(↑((sign : (a : Perm (Fin n.succ)) → ℤˣ) i.cycleRange⁻¹) : ℤ) : R) * A.det
Tactic: calc
      det A = ↑((-1 : ℤˣ) ^ (i : ℕ) * (-1 : ℤˣ) ^ (i : ℕ) : ℤˣ) * det A := by simp
      _ = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by simp [-Int.units_mul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det =
    HPow.hPow (α := R) (-1) (↑i : ℕ) *
      ∑ i_1 : Fin n.succ, HPow.hPow (α := R) (-1) (↑i_1 : ℕ) * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
have this : A.det = HPow.hPow (α := R) (-1) (↑i : ℕ) * (↑(↑((sign : (a : Perm (Fin n.succ)) → ℤˣ) i.cycleRange⁻¹) : ℤ) : R) * A.det
Tactic: have : det A = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by
    calc
      det A = ↑((-1 : ℤˣ) ^ (i : ℕ) * (-1 : ℤˣ) ^ (i : ℕ) : ℤˣ) * det A := by simp
      _ = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by simp [-Int.units_mul_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this :
  A.det =
    HPow.hPow (α := R) (-1) (↑i : ℕ) * (↑(↑((sign : (a : Perm (Fin n.succ)) → ℤˣ) i.cycleRange⁻¹) : ℤ) : R) * A.det
⊢ A.det =
    HPow.hPow (α := R) (-1) (↑i : ℕ) *
      ∑ i_1 : Fin n.succ, HPow.hPow (α := R) (-1) (↑i_1 : ℕ) * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
have rw : HPow.hPow (α := R) (-1) (↑i : ℕ) * ((↑(↑((sign : (a : Perm (Fin n.succ)) → ℤˣ) i.cycleRange⁻¹) : ℤ) : R) * A.det) =
  HPow.hPow (α := R) (-1) (↑i : ℕ) *
    ∑ i_1 : Fin n.succ, HPow.hPow (α := R) (-1) (↑i_1 : ℕ) * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
Tactic: rw [this, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this :
  A.det =
    HPow.hPow (α := R) (-1) (↑i : ℕ) * (↑(↑((sign : (a : Perm (Fin n.succ)) → ℤˣ) i.cycleRange⁻¹) : ℤ) : R) * A.det
⊢ HPow.hPow (α := R) (-1) (↑i : ℕ) * ((↑(↑((sign : (a : Perm (Fin n.succ)) → ℤˣ) i.cycleRange⁻¹) : ℤ) : R) * A.det) =
    HPow.hPow (α := R) (-1) (↑i : ℕ) *
      ∑ i_1 : Fin n.succ, HPow.hPow (α := R) (-1) (↑i_1 : ℕ) * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
have e_a : (↑(↑((sign : (a : Perm (Fin n.succ)) → ℤˣ) i.cycleRange⁻¹) : ℤ) : R) * A.det =
  ∑ i_1 : Fin n.succ, HPow.hPow (α := R) (-1) (↑i_1 : ℕ) * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this :
  A.det =
    HPow.hPow (α := R) (-1) (↑i : ℕ) * (↑(↑((sign : (a : Perm (Fin n.succ)) → ℤˣ) i.cycleRange⁻¹) : ℤ) : R) * A.det
⊢ (↑(↑((sign : (a : Perm (Fin n.succ)) → ℤˣ) i.cycleRange⁻¹) : ℤ) : R) * A.det =
    ∑ i_1 : Fin n.succ, HPow.hPow (α := R) (-1) (↑i_1 : ℕ) * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)
have e_a : Eq.{v + 1} (α := R)
  (∑ j : Fin n.succ,
    HPow.hPow (α := R) (-1) (↑j : ℕ) *
        A.submatrix (l := Fin n.succ) (⇑i.cycleRange⁻¹ : (a : Fin n.succ) → Fin n.succ) id 0 j *
      det (submatrix (A.submatrix (⇑i.cycleRange⁻¹ : (a : Fin n.succ) → Fin n.succ) id) Fin.succ j.succAbove))
  (∑ i_1 : Fin n.succ, HPow.hPow (α := R) (-1) (↑i_1 : ℕ) * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det))
Tactic: rw [← det_permute, det_succ_row_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this :
  A.det =
    HPow.hPow (α := R) (-1) (↑i : ℕ) * (↑(↑((sign : (a : Perm (Fin n.succ)) → ℤˣ) i.cycleRange⁻¹) : ℤ) : R) * A.det
⊢ Eq.{v + 1} (α := R)
    (∑ j : Fin n.succ,
      HPow.hPow (α := R) (-1) (↑j : ℕ) *
          A.submatrix (l := Fin n.succ) (⇑i.cycleRange⁻¹ : (a : Fin n.succ) → Fin n.succ) id 0 j *
        det (submatrix (A.submatrix (⇑i.cycleRange⁻¹ : (a : Fin n.succ) → Fin n.succ) id) Fin.succ j.succAbove))
    (∑ i_1 : Fin n.succ, HPow.hPow (α := R) (-1) (↑i_1 : ℕ) * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det))
have e_a : ∀ (j : Fin n.succ),
  Membership.mem (γ := Finset (Fin n.succ)) univ j →
    HPow.hPow (α := R) (-1) (↑j : ℕ) *
          A.submatrix (l := Fin n.succ) (⇑i.cycleRange⁻¹ : (a : Fin n.succ) → Fin n.succ) id 0 j *
        det (submatrix (A.submatrix (⇑i.cycleRange⁻¹ : (a : Fin n.succ) → Fin n.succ) id) Fin.succ j.succAbove) =
      HPow.hPow (α := R) (-1) (↑j : ℕ) * (A i j * (A.submatrix i.succAbove j.succAbove).det)
Tactic: refine Finset.sum_congr rfl fun j _ => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this :
  A.det =
    HPow.hPow (α := R) (-1) (↑i : ℕ) * (↑(↑((sign : (a : Perm (Fin n.succ)) → ℤˣ) i.cycleRange⁻¹) : ℤ) : R) * A.det
j : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ j
⊢ HPow.hPow (α := R) (-1) (↑j : ℕ) *
        A.submatrix (l := Fin n.succ) (⇑i.cycleRange⁻¹ : (a : Fin n.succ) → Fin n.succ) id 0 j *
      det (submatrix (A.submatrix (⇑i.cycleRange⁻¹ : (a : Fin n.succ) → Fin n.succ) id) Fin.succ j.succAbove) =
    HPow.hPow (α := R) (-1) (↑j : ℕ) * (A i j * (A.submatrix i.succAbove j.succAbove).det)
have e_a : HPow.hPow (α := R) (-1) (↑j : ℕ) *
    (A ((i.cycleRange⁻¹ : (a : Fin n.succ) → Fin n.succ) 0) j *
      det (A.submatrix (fun (x : Fin n) ↦ (i.cycleRange⁻¹ : (a : Fin n.succ) → Fin n.succ) x.succ) j.succAbove)) =
  HPow.hPow (α := R) (-1) (↑j : ℕ) * (A i j * (A.submatrix i.succAbove j.succAbove).det)
Tactic: rw [mul_assoc, Matrix.submatrix_apply, submatrix_submatrix, id_comp, Function.comp_def, id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j : Fin n.succ
⊢ A.det =
    ∑ i : Fin n.succ, HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
have rw : Eq.{v + 1} (α := R)
  (∑ j_1 : Fin n.succ,
    HPow.hPow (α := R) (-1) ((↑j : ℕ) + (↑j_1 : ℕ)) * Aᵀ j j_1 * (Aᵀ.submatrix j.succAbove j_1.succAbove).det)
  (∑ i : Fin n.succ, HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det)
Tactic: rw [← det_transpose, det_succ_row _ j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j : Fin n.succ
⊢ Eq.{v + 1} (α := R)
    (∑ j_1 : Fin n.succ,
      HPow.hPow (α := R) (-1) ((↑j : ℕ) + (↑j_1 : ℕ)) * Aᵀ j j_1 * (Aᵀ.submatrix j.succAbove j_1.succAbove).det)
    (∑ i : Fin n.succ,
      HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det)
have refine : ∀ (i : Fin n.succ),
  Membership.mem (γ := Finset (Fin n.succ)) univ i →
    HPow.hPow (α := R) (-1) ((↑j : ℕ) + (↑i : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
      HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
Tactic: refine Finset.sum_congr rfl fun i _ => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j i : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ i
⊢ HPow.hPow (α := R) (-1) ((↑j : ℕ) + (↑i : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
have rw : HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
Tactic: rw [add_comm, ← det_transpose, transpose_apply, transpose_submatrix, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j i : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ i
rw :
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
⊢ HPow.hPow (α := R) (-1) ((↑j : ℕ) + (↑i : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
have rw₁ : HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove)ᵀ.det =
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
Tactic: rw [add_comm, ← det_transpose, transpose_apply, transpose_submatrix, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j i : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ i
rw :
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
rw₁ :
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove)ᵀ.det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
⊢ HPow.hPow (α := R) (-1) ((↑j : ℕ) + (↑i : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
have rw₂ : HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (Aᵀ.submatrix j.succAbove i.succAbove)ᵀ.det =
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
Tactic: rw [add_comm, ← det_transpose, transpose_apply, transpose_submatrix, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j i : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ i
rw :
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
rw₁ :
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove)ᵀ.det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
rw₂ :
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (Aᵀ.submatrix j.succAbove i.succAbove)ᵀ.det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
⊢ HPow.hPow (α := R) (-1) ((↑j : ℕ) + (↑i : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
have rw₃ : HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (Aᵀᵀ.submatrix i.succAbove j.succAbove).det =
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
Tactic: rw [add_comm, ← det_transpose, transpose_apply, transpose_submatrix, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j i : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ i
rw :
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
rw₁ :
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove)ᵀ.det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
rw₂ :
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (Aᵀ.submatrix j.succAbove i.succAbove)ᵀ.det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
rw₃ :
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (Aᵀᵀ.submatrix i.succAbove j.succAbove).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
⊢ HPow.hPow (α := R) (-1) ((↑j : ℕ) + (↑i : ℕ)) * Aᵀ j i * (Aᵀ.submatrix j.succAbove i.succAbove).det =
    HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
have rw₄ : HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det =
  HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det
Tactic: rw [add_comm, ← det_transpose, transpose_apply, transpose_submatrix, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Matrix (Fin 2) (Fin 2) R
⊢ A.det = A 0 0 * A 1 1 - A 0 1 * A 1 0
have simp : HPow.hPow (α := R) (β := ℕ) (-1) 0 * A 0 0 * A 1 1 + HPow.hPow (α := R) (-1) (HAdd.hAdd (α := ℕ) 0 1) * A 0 1 * A 1 0 =
  A 0 0 * A 1 1 - A 0 1 * A 1 0
Tactic: simp only [det_succ_row_zero, det_unique, Fin.default_eq_zero, submatrix_apply,
    Fin.succ_zero_eq_one, Fin.sum_univ_succ, Fin.val_zero, Fin.zero_succAbove, univ_unique,
    Fin.val_succ, Fin.val_eq_zero, Fin.succ_succAbove_zero, sum_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.det =
    A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 +
        A 0 2 * A 1 0 * A 2 1 -
      A 0 2 * A 1 1 * A 2 0
have simp : HPow.hPow (α := R) (β := ℕ) (-1) 0 * A 0 0 *
      (HPow.hPow (α := R) (β := ℕ) (-1) 0 * A 1 1 * A 2 2 +
        HPow.hPow (α := R) (-1) (HAdd.hAdd (α := ℕ) 0 1) * A 1 2 * A 2 1) +
    (HPow.hPow (α := R) (-1) (HAdd.hAdd (α := ℕ) 0 1) * A 0 1 *
        (HPow.hPow (α := R) (β := ℕ) (-1) 0 * A 1 0 * A 2 2 +
          HPow.hPow (α := R) (-1) (HAdd.hAdd (α := ℕ) 0 1) * A 1 2 * A 2 0) +
      HPow.hPow (α := R) (-1) (HAdd.hAdd (α := ℕ) 0 1 + 1) * A 0 2 *
        (HPow.hPow (α := R) (β := ℕ) (-1) 0 * A 1 0 * A 2 1 +
          HPow.hPow (α := R) (-1) (HAdd.hAdd (α := ℕ) 0 1) * A 1 1 * A 2 0)) =
  A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 +
      A 0 2 * A 1 0 * A 2 1 -
    A 0 2 * A 1 1 * A 2 0
Tactic: simp only [det_succ_row_zero, submatrix_apply, Fin.succ_zero_eq_one, submatrix_submatrix,
    det_unique, Fin.default_eq_zero, Function.comp_apply, Fin.succ_one_eq_two, Fin.sum_univ_succ,
    Fin.val_zero, Fin.zero_succAbove, univ_unique, Fin.val_succ, Fin.val_eq_zero,
    Fin.succ_succAbove_zero, sum_singleton, Fin.succ_succAbove_one]