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 : Fin n.succ
this :
  A.det =
    HPow.hPow (α := R) (-1) (↑i : ℕ) * (↑(↑((sign : (a : Perm (Fin n.succ)) → ℤˣ) i.cycleRange⁻¹) : ℤ) : R) * A.det
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)
⊢ 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:
refine Finset.sum_congr rfl fun j _ => ?_

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
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
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)
⊢ 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:
rw [mul_assoc, Matrix.submatrix_apply, submatrix_submatrix, id_comp, Function.comp_def, id]

Premises used: mul_assoc, id, Function.comp_def, Matrix.submatrix_submatrix, Matrix.submatrix_apply, Function.id_comp
-- 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
j : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) univ j
⊢ 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:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j : Fin n.succ
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)
⊢ A.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]

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

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
j : Fin n.succ
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
⊢ 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:
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
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
rw₄ 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

Tactic:
rw [add_comm, ← det_transpose, transpose_apply, transpose_submatrix, transpose_transpose]

Premises used: Matrix.det_transpose, Matrix.transpose_submatrix, Matrix.transpose_transpose, add_comm, Matrix.transpose_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
A : Matrix (Fin 0) (Fin 0) R
⊢ A.det = 1

Tactic:
det_isEmpty

Premises used: Matrix.det_isEmpty
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
A : Matrix (Fin 1) (Fin 1) R
⊢ A.det = A 0 0

Tactic:
det_unique A

Premises used: Matrix.det_unique
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
a : R
⊢ det (n := Fin 1) !![a] = a

Tactic:
det_fin_one _

Premises used: Eq.mpr, Matrix.det_fin_one, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
A : Matrix (Fin 2) (Fin 2) R
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
⊢ A.det = 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]

Premises used: Fin.zero_succAbove, Fin.succ_succAbove_zero, Finset.univ_unique, Fin.val_succ, Fin.succ_zero_eq_one, Finset.sum_singleton, Fin.val_eq_zero, Fin.default_eq_zero, Matrix.submatrix_apply, Matrix.det_unique, Matrix.det_succ_row_zero, Fin.val_zero, Fin.sum_univ_succ
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
A : Matrix (Fin 2) (Fin 2) R
⊢ 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:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
a b c d : R
⊢ det (n := Fin 2) !![a, b; c, d] = a * d - b * c

Tactic:
det_fin_two _

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.det_fin_two, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
A : Matrix (Fin 3) (Fin 3) R
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
⊢ 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

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]

Premises used: Fin.zero_succAbove, Fin.succ_succAbove_zero, Finset.univ_unique, Fin.val_succ, Fin.succ_zero_eq_one, Finset.sum_singleton, Fin.val_eq_zero, Matrix.submatrix_submatrix, Function.comp_apply, Fin.default_eq_zero, Matrix.submatrix_apply, Fin.succ_succAbove_one, Matrix.det_unique, Matrix.det_succ_row_zero, Fin.val_zero, Fin.sum_univ_succ, Fin.succ_one_eq_two
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
A : Matrix (Fin 3) (Fin 3) R
⊢ 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:
ring
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), M j) 0
j₁ j₂ : Fin (n + 1)
this :
  ∀ (j : Fin (n + 1)),
    (M.submatrix j.succAbove id).det = Int.negOnePow (↑(↑j : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
rw :
  Int.negOnePow (↑(↑j₁ : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det =
    (HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ)).negOnePow • (M.submatrix j₂.succAbove id).det
rw₁ :
  Int.negOnePow (↑(↑j₁ : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det =
    (HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ)).negOnePow •
      Int.negOnePow (↑(↑j₂ : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
rw₂ :
  Int.negOnePow (↑(↑j₁ : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det =
    ((HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ)).negOnePow * Int.negOnePow (↑(↑j₂ : ℕ) : ℤ)) •
      (M.submatrix (Fin.succAbove 0) id).det
rw₃ :
  Int.negOnePow (↑(↑j₁ : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det =
    (HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ) + (↑(↑j₂ : ℕ) : ℤ)).negOnePow •
      (M.submatrix (Fin.succAbove 0) id).det
rw₄ rw₅ :
  Int.negOnePow (↑(↑j₁ : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det =
    Int.negOnePow (↑(↑j₁ : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
⊢ (M.submatrix j₁.succAbove id).det =
    (HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ)).negOnePow • (M.submatrix j₂.succAbove id).det

Tactic:
rw [this j₁, this j₂, smul_smul, ← Int.negOnePow_add, sub_add_cancel]

Premises used: smul_smul, Int.negOnePow_add, sub_add_cancel
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), M j) 0
j₁ j₂ : Fin (n + 1)
suffices :
  ∀ (j : Fin (n + 1)),
    (M.submatrix j.succAbove id).det = Int.negOnePow (↑(↑j : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
⊢ (M.submatrix j₁.succAbove id).det =
    (HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ)).negOnePow • (M.submatrix j₂.succAbove id).det

Tactic:
suffices ∀ j, (M.submatrix (Fin.succAbove j) id).det =
      Int.negOnePow j • (M.submatrix (Fin.succAbove 0) id).det by
    rw [this j₁, this j₂, smul_smul, ← Int.negOnePow_add, sub_add_cancel]
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), M j) 0
j₁ j₂ : Fin (n + 1)
zero : (M.submatrix (Fin.succAbove 0) id).det = Int.negOnePow (↑0 : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
zero₁ : (M.submatrix (Fin.succAbove 0) id).det = Int.negOnePow 0 • (M.submatrix (Fin.succAbove 0) id).det
zero₂ : (M.submatrix (Fin.succAbove 0) id).det = HSMul.hSMul (α := ℤˣ) 1 (M.submatrix (Fin.succAbove 0) id).det
zero₃ zero₄ : (M.submatrix (Fin.succAbove 0) id).det = (M.submatrix (Fin.succAbove 0) id).det
⊢ (M.submatrix (Fin.succAbove 0) id).det = Int.negOnePow (↑(↑0 : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det

Tactic:
rw [Fin.val_zero, Nat.cast_zero, Int.negOnePow_zero, one_smul]

Premises used: one_smul, Int.negOnePow_zero, Nat.cast_zero, Fin.val_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), M j) 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind :
  (M.submatrix i.castSucc.succAbove id).det =
    Int.negOnePow (↑(↑i.castSucc : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
succ :
  ((M.submatrix i.succ.succAbove id).updateRow i
        (∑ k : Fin n, HSMul.hSMul (α := R) (-1) (M.submatrix i.succ.succAbove id k))).det =
    (M.submatrix i.castSucc.succAbove id).det
⊢ (M.submatrix i.succ.succAbove id).det = Int.negOnePow (↑(↑i.succ : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det

Tactic:
rw [Fin.val_succ, Nat.cast_add, Nat.cast_one, Int.negOnePow_succ, Units.neg_smul,
        ← neg_eq_iff_eq_neg, ← neg_one_smul R,
        ← det_updateRow_sum (M.submatrix i.succ.succAbove id) i (fun _ ↦ -1),
        ← Fin.val_castSucc i, ← h_ind]

Premises used: Fin.succAbove, Matrix.submatrix, Fin.succ, neg_one_smul, neg_eq_iff_eq_neg, id, Matrix.det_updateRow_sum, Fin.val_succ, Nat.cast_add, Units.neg_smul, OfNat.ofNat, Nat.cast_one, Int.negOnePow_succ, Neg.neg, Fin.val_castSucc
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), M j) 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind :
  (M.submatrix i.castSucc.succAbove id).det =
    Int.negOnePow (↑(↑i.castSucc : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
succ :
  (M.submatrix i.succ.succAbove id).updateRow i
      (∑ k : Fin n, HSMul.hSMul (α := R) (-1) (M.submatrix i.succ.succAbove id k)) =
    M.submatrix i.castSucc.succAbove id
⊢ ((M.submatrix i.succ.succAbove id).updateRow i
        (∑ k : Fin n, HSMul.hSMul (α := R) (-1) (M.submatrix i.succ.succAbove id k))).det =
    (M.submatrix i.castSucc.succAbove id).det

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), M j) 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind :
  (M.submatrix i.castSucc.succAbove id).det =
    Int.negOnePow (↑(↑i.castSucc : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
succ :
  ∀ (a b : Fin n),
    (M.submatrix i.succ.succAbove id).updateRow i
        (∑ k : Fin n, HSMul.hSMul (α := R) (-1) (M.submatrix i.succ.succAbove id k)) a b =
      M.submatrix i.castSucc.succAbove id a b
⊢ (M.submatrix i.succ.succAbove id).updateRow i
      (∑ k : Fin n, HSMul.hSMul (α := R) (-1) (M.submatrix i.succ.succAbove id k)) =
    M.submatrix i.castSucc.succAbove id

Tactic:
ext a b
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), M j) 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind :
  (M.submatrix i.castSucc.succAbove id).det =
    Int.negOnePow (↑(↑i.castSucc : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
succ :
  (if a = i then -∑ x : Fin n, M (i.succ.succAbove x) b else M (i.succ.succAbove a) b) = M (i.castSucc.succAbove a) b
⊢ (M.submatrix i.succ.succAbove id).updateRow i
      (∑ k : Fin n, HSMul.hSMul (α := R) (-1) (M.submatrix i.succ.succAbove id k)) a b =
    M.submatrix i.castSucc.succAbove id a b

Tactic:
simp_rw [neg_one_smul, updateRow_apply, Finset.sum_neg_distrib, Pi.neg_apply,
        Finset.sum_apply, submatrix_apply, id_eq]

Premises used: neg_one_smul, Finset.sum_apply, Matrix.submatrix_apply, Finset.sum_neg_distrib, Pi.neg_apply, Matrix.updateRow_apply, id_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), M j) 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind :
  (M.submatrix i.castSucc.succAbove id).det =
    Int.negOnePow (↑(↑i.castSucc : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
pos : ∀ (h : a = i), -∑ x : Fin n, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b
neg : ∀ (h : ¬a = i), M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b
⊢ (if a = i then -∑ x : Fin n, M (i.succ.succAbove x) b else M (i.succ.succAbove a) b) = M (i.castSucc.succAbove a) b

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), M j) 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind :
  (M.submatrix i.castSucc.succAbove id).det =
    Int.negOnePow (↑(↑i.castSucc : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : a = i
⊢ Eq.{u_1 + 1} (α := R) ((∑ j : Fin (n + 1), M j) b) (0 b)

Tactic:
replace hv := congr_fun hv b
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind :
  (M.submatrix i.castSucc.succAbove id).det =
    Int.negOnePow (↑(↑i.castSucc : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : a = i
hv : Eq.{u_1 + 1} (α := R) ((∑ j : Fin (n + 1), M j) b) (0 b)
⊢ M i.succ b + ∑ c : Fin n, M (i.succ.succAbove c) b = 0 b

Tactic:
rw [Fin.sum_univ_succAbove _ i.succ, Pi.add_apply, Finset.sum_apply] at hv

Premises used: Fin.succ, Finset.sum_apply, Pi.add_apply, Fin.sum_univ_succAbove
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind :
  (M.submatrix i.castSucc.succAbove id).det =
    Int.negOnePow (↑(↑i.castSucc : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : a = i
hv : M i.succ b + ∑ c : Fin n, M (i.succ.succAbove c) b = 0 b
pos : -∑ x : Fin n, M (i.succ.succAbove x) b = M (i.castSucc.succAbove i) b
pos₁ : -∑ x : Fin n, M (i.succ.succAbove x) b = M i.succ b
pos₂ : ∑ x : Fin n, M (i.succ.succAbove x) b + M i.succ b = 0
pos₃ pos₄ pos₅ pos₆ : M i.succ b + ∑ x : Fin n, M (i.succ.succAbove x) b = 0
⊢ -∑ x : Fin n, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b

Tactic:
rwa [h, Fin.succAbove_castSucc_self, neg_eq_iff_add_eq_zero, add_comm]

Premises used: neg_eq_iff_add_eq_zero, Fin.succAbove_castSucc_self, add_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), M j) 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind :
  (M.submatrix i.castSucc.succAbove id).det =
    Int.negOnePow (↑(↑i.castSucc : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : ¬a = i
neg : ∀ (h : a < i), M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b
neg₁ : ∀ (h : i < a), M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b

Tactic:
obtain h | h := ne_iff_lt_or_gt.mp h

Premises used: ne_iff_lt_or_gt, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), M j) 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind :
  (M.submatrix i.castSucc.succAbove id).det =
    Int.negOnePow (↑(↑i.castSucc : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h_1 : ¬a = i
h : a < i
neg : M (i.succ.succAbove a) b = M a.castSucc b
neg₁ neg₂ : M a.castSucc b = M a.castSucc b
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b

Tactic:
rw [Fin.succAbove_castSucc_of_lt _ _ h,
            Fin.succAbove_of_succ_le _ _ (Fin.succ_lt_succ_iff.mpr h).le]

Premises used: Iff.mpr, Fin.succ_lt_succ_iff, LT.lt.le, Fin.succAbove_of_succ_le, Fin.succAbove_castSucc_of_lt
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : Eq.{u_1 + 1} (α := Fin n → R) (∑ j : Fin (n + 1), M j) 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind :
  (M.submatrix i.castSucc.succAbove id).det =
    Int.negOnePow (↑(↑i.castSucc : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h_1 : ¬a = i
h : i < a
neg : M a.succ b = M (i.castSucc.succAbove a) b
neg₁ neg₂ : M a.succ b = M a.succ b
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b

Tactic:
rw [Fin.succAbove_succ_of_lt _ _ h, Fin.succAbove_castSucc_of_le _ _ h.le]

Premises used: LT.lt.le, Fin.succAbove_succ_of_lt, Fin.succAbove_castSucc_of_le