awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)
refine_2 :
  Eq.{v + 1} (α := R)
    (∑ y : Perm (Fin n),
      HSMul.hSMul (α := ℤˣ) (β := R)
        ((sign : (a : Perm (Fin n.succ)) → ℤˣ)
            ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, y)) :
          ℤˣ)
        (∏ x : Fin n.succ,
          A
            ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, y) :
                  Perm (Fin n.succ)) :
                (a : Fin n.succ) → Fin n.succ)
              x)
            x))
    (∑ i_2 : Perm (Fin n),
      -1 *
        (A i.succ 0 *
          HSMul.hSMul (α := ℤˣ) (β := R) ((sign : (a : Perm (Fin n)) → ℤˣ) i_2 : ℤˣ)
            (∏ i_3 : Fin n,
              submatrix (l := Fin n) (m := Fin n)
                ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i_4 j : Fin n) ↦
                  A (i.succ.succAbove i_4) j.succ)
                ((⇑i.cycleRange : (a : Fin n) → Fin n) : (a : Fin n) → Fin n) id
                ((i_2 : (a : Fin n) → Fin n) i_3 : Fin n) i_3)))
⊢ ∑ y : Perm (Fin n),
      HSMul.hSMul (α := ℤˣ) (β := R)
        ((sign : (a : Perm (Fin n.succ)) → ℤˣ)
            ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, y)) :
          ℤˣ)
        (∏ x : Fin n.succ,
          A
            ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, y) :
                  Perm (Fin n.succ)) :
                (a : Fin n.succ) → Fin n.succ)
              x)
            x) =
    HPow.hPow (α := R) (-1) (↑i.succ : ℕ) * A i.succ 0 *
      det (n := Fin n)
        ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i_2 j : Fin n) ↦
          A (i.succ.succAbove i_2) j.succ)

Tactic:
rw [Fin.val_succ, pow_succ', this, mul_assoc, mul_assoc, mul_left_comm (ε _),
    ← det_permute, Matrix.det_apply, Finset.mul_sum, Finset.mul_sum]

Premises used: Matrix.det_apply, Finset.mul_sum, Matrix.det_permute, mul_assoc, Fin.val_succ, pow_succ'
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)
⊢ Eq.{v + 1} (α := R)
    (∑ y : Perm (Fin n),
      HSMul.hSMul (α := ℤˣ) (β := R)
        ((sign : (a : Perm (Fin n.succ)) → ℤˣ)
            ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, y)) :
          ℤˣ)
        (∏ x : Fin n.succ,
          A
            ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, y) :
                  Perm (Fin n.succ)) :
                (a : Fin n.succ) → Fin n.succ)
              x)
            x))
    (∑ i_2 : Perm (Fin n),
      -1 *
        (A i.succ 0 *
          HSMul.hSMul (α := ℤˣ) (β := R) ((sign : (a : Perm (Fin n)) → ℤˣ) i_2 : ℤˣ)
            (∏ i_3 : Fin n,
              submatrix (l := Fin n) (m := Fin n)
                ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i_4 j : Fin n) ↦
                  A (i.succ.succAbove i_4) j.succ)
                ((⇑i.cycleRange : (a : Fin n) → Fin n) : (a : Fin n) → Fin n) id
                ((i_2 : (a : Fin n) → Fin n) i_3 : Fin n) i_3)))

Tactic:
Finset.sum_congr rfl fun σ _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)
refine_2 :
  ∀ (σ : Perm (Fin n)),
    Membership.mem (γ := Finset (Perm (Fin n))) univ σ →
      HSMul.hSMul (α := ℤˣ) (β := R)
          ((sign : (a : Perm (Fin n.succ)) → ℤˣ)
              ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, σ)) :
            ℤˣ)
          (∏ 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))
⊢ Eq.{v + 1} (α := R)
    (∑ y : Perm (Fin n),
      HSMul.hSMul (α := ℤˣ) (β := R)
        ((sign : (a : Perm (Fin n.succ)) → ℤˣ)
            ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, y)) :
          ℤˣ)
        (∏ x : Fin n.succ,
          A
            ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, y) :
                  Perm (Fin n.succ)) :
                (a : Fin n.succ) → Fin n.succ)
              x)
            x))
    (∑ i_2 : Perm (Fin n),
      -1 *
        (A i.succ 0 *
          HSMul.hSMul (α := ℤˣ) (β := R) ((sign : (a : Perm (Fin n)) → ℤˣ) i_2 : ℤˣ)
            (∏ i_3 : Fin n,
              submatrix (l := Fin n) (m := Fin n)
                ((of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) fun (i_4 j : Fin n) ↦
                  A (i.succ.succAbove i_4) j.succ)
                ((⇑i.cycleRange : (a : Fin n) → Fin n) : (a : Fin n) → Fin n) id
                ((i_2 : (a : Fin n) → Fin n) i_3 : Fin n) i_3)))

Tactic:
refine Finset.sum_congr rfl fun σ _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 σ
refine_2 :
  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))
⊢ HSMul.hSMul (α := ℤˣ) (β := R)
      ((sign : (a : Perm (Fin n.succ)) → ℤˣ)
          ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, σ)) :
        ℤˣ)
      (∏ 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))

Tactic:
rw [Equiv.Perm.decomposeFin.symm_sign, if_neg (Fin.succ_ne_zero i)]

Premises used: Equiv.Perm.decomposeFin.symm_sign, Fin.succ_ne_zero, if_neg
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)

Tactic:
simp only [Fin.prod_univ_succ, Fin.succAbove_cycleRange,
        Equiv.Perm.decomposeFin_symm_apply_zero, Equiv.Perm.decomposeFin_symm_apply_succ]

Premises used: Fin.succAbove_cycleRange, Equiv.Perm.decomposeFin_symm_apply_succ, Fin.prod_univ_succ, Equiv.Perm.decomposeFin_symm_apply_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 σ
⊢ 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:
simp [_root_.neg_mul, one_mul, zsmul_eq_mul, neg_smul,
        Fin.succAbove_cycleRange, mul_left_comm]

Premises used: zsmul_eq_mul, neg_smul, mul_left_comm, Fin.succAbove_cycleRange, neg_mul, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)
σ₂ :
  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))
⊢ 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))

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]

Premises used: Units.val, Fin.succAbove, HMul.hMul, Finset.univ, Fin.succ, Equiv.Perm.sign, Prod.mk, Finset.prod, Fin.cycleRange, Equiv.Perm.decomposeFin, HSMul.hSMul, Equiv.symm, OfNat.ofNat, DFunLike.coe, Neg.neg
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
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)
⊢ A.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]

Premises used: Matrix.det_transpose, Matrix.det_succ_column_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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)

Tactic:
Finset.sum_congr rfl fun i _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
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
⊢ 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:
refine Finset.sum_congr rfl fun i _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
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
⊢ 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]

Premises used: Matrix.det_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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

Tactic:
simp only [transpose_apply, transpose_submatrix, transpose_transpose]

Premises used: Matrix.transpose_submatrix, Matrix.transpose_transpose, Matrix.transpose_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
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)
⊢ A.det =
    ∑ j : Fin n.succ, HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ)) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
simp_rw [pow_add, mul_assoc, ← mul_sum]

Premises used: Finset.mul_sum, mul_assoc, pow_add
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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 (α := ℤˣ) (-1) (↑i : ℕ) * HPow.hPow (α := ℤˣ) (-1) (↑i : ℕ)) : ℤ) : R) * A.det

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ (↑(↑(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:
simp [-Int.units_mul_self]

Premises used: Int.units_mul_self
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
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
⊢ 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]

Premises used: HMul.hMul, Equiv.Perm.sign, Fin.val, Fin.cycleRange, Inv.inv, HPow.hPow, OfNat.ofNat, DFunLike.coe, Matrix.det, Neg.neg
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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

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]
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
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)
⊢ 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]

Premises used: mul_assoc
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
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)
⊢ 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:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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
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))
⊢ (↑(↑((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:
rw [← det_permute, det_succ_row_zero]

Premises used: Matrix.det_permute, Matrix.det_succ_row_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
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))

Tactic:
Finset.sum_congr rfl fun j _ => ?_

Premises used: Finset.sum_congr, rfl