awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ (M.submatrix j₁.succAbove id).det =
    (HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ)).negOnePow • (M.submatrix j₂.succAbove id).det
have rw : Int.negOnePow (↑(↑j₁ : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ (M.submatrix j₁.succAbove id).det =
    (HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ)).negOnePow • (M.submatrix j₂.succAbove id).det
have 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
Tactic: rw [this j₁, this j₂, smul_smul, ← Int.negOnePow_add, sub_add_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ (M.submatrix j₁.succAbove id).det =
    (HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ)).negOnePow • (M.submatrix j₂.succAbove id).det
have 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
Tactic: rw [this j₁, this j₂, smul_smul, ← Int.negOnePow_add, sub_add_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ (M.submatrix j₁.succAbove id).det =
    (HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ)).negOnePow • (M.submatrix j₂.succAbove id).det
have rw₃ : Int.negOnePow (↑(↑j₁ : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det =
  (HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ) + (↑(↑j₂ : ℕ) : ℤ)).negOnePow •
    (M.submatrix (Fin.succAbove 0) id).det
Tactic: rw [this j₁, this j₂, smul_smul, ← Int.negOnePow_add, sub_add_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ (M.submatrix j₁.succAbove id).det =
    (HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ)).negOnePow • (M.submatrix j₂.succAbove id).det
have rw₄ : Int.negOnePow (↑(↑j₁ : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det =
  Int.negOnePow (↑(↑j₁ : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
Tactic: rw [this j₁, this j₂, smul_smul, ← Int.negOnePow_add, sub_add_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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)
⊢ (M.submatrix j₁.succAbove id).det =
    (HSub.hSub (α := ℤ) (↑(↑j₁ : ℕ) : ℤ) (↑(↑j₂ : ℕ) : ℤ)).negOnePow • (M.submatrix j₂.succAbove id).det
have suffices : ∀ (j : Fin (n + 1)),
  (M.submatrix j.succAbove id).det = Int.negOnePow (↑(↑j : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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)
⊢ (M.submatrix (Fin.succAbove 0) id).det = Int.negOnePow (↑(↑0 : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
have zero : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ (M.submatrix (Fin.succAbove 0) id).det = Int.negOnePow (↑(↑0 : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
have zero₁ : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ (M.submatrix (Fin.succAbove 0) id).det = Int.negOnePow (↑(↑0 : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
have zero₂ : (M.submatrix (Fin.succAbove 0) id).det = HSMul.hSMul (α := ℤˣ) 1 (M.submatrix (Fin.succAbove 0) id).det
Tactic: rw [Fin.val_zero, Nat.cast_zero, Int.negOnePow_zero, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ (M.submatrix (Fin.succAbove 0) id).det = Int.negOnePow (↑(↑0 : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
have zero₃ : (M.submatrix (Fin.succAbove 0) id).det = (M.submatrix (Fin.succAbove 0) id).det
Tactic: rw [Fin.val_zero, Nat.cast_zero, Int.negOnePow_zero, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ (M.submatrix i.succ.succAbove id).det = Int.negOnePow (↑(↑i.succ : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ ((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
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ (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
have 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
Tactic: ext a b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ (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
have 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
Tactic: simp_rw [neg_one_smul, updateRow_apply, Finset.sum_neg_distrib, Pi.neg_apply,
        Finset.sum_apply, submatrix_apply, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ (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
have pos : ∀ (h : a = i), -∑ x : Fin n, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ (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
have neg : ∀ (h : ¬a = i), M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (hypothesis)
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
⊢ -∑ x : Fin n, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b
have hv₁ : Eq.{u_1 + 1} (α := R) ((∑ j : Fin (n + 1), M j) b) (0 b)
Tactic: replace hv := congr_fun hv b
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (hypothesis)
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)
⊢ -∑ x : Fin n, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b
have hv₁ : 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
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ -∑ x : Fin n, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b
have pos : -∑ x : Fin n, M (i.succ.succAbove x) b = M (i.castSucc.succAbove i) b
Tactic: rwa [h, Fin.succAbove_castSucc_self, neg_eq_iff_add_eq_zero, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ -∑ x : Fin n, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b
have pos₁ : -∑ x : Fin n, M (i.succ.succAbove x) b = M i.succ b
Tactic: rwa [h, Fin.succAbove_castSucc_self, neg_eq_iff_add_eq_zero, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ -∑ x : Fin n, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b
have pos₂ : ∑ x : Fin n, M (i.succ.succAbove x) b + M i.succ b = 0
Tactic: rwa [h, Fin.succAbove_castSucc_self, neg_eq_iff_add_eq_zero, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ -∑ x : Fin n, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b
have pos₃ : M i.succ b + ∑ x : Fin n, M (i.succ.succAbove x) b = 0
Tactic: rwa [h, Fin.succAbove_castSucc_self, neg_eq_iff_add_eq_zero, add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b
have neg : ∀ (h : a < i), M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b
Tactic: obtain h | h := ne_iff_lt_or_gt.mp h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b
have neg₁ : ∀ (h : i < a), M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b
Tactic: obtain h | h := ne_iff_lt_or_gt.mp h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b
have neg : M (i.succ.succAbove a) b = M a.castSucc b
Tactic: rw [Fin.succAbove_castSucc_of_lt _ _ h,
            Fin.succAbove_of_succ_le _ _ (Fin.succ_lt_succ_iff.mpr h).le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b
have neg₁ : M a.castSucc b = M a.castSucc b
Tactic: rw [Fin.succAbove_castSucc_of_lt _ _ h,
            Fin.succAbove_of_succ_le _ _ (Fin.succ_lt_succ_iff.mpr h).le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b
have neg : M a.succ b = M (i.castSucc.succAbove a) b
Tactic: rw [Fin.succAbove_succ_of_lt _ _ h, Fin.succAbove_castSucc_of_le _ _ h.le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b
have neg₁ : M a.succ b = M a.succ b
Tactic: rw [Fin.succAbove_succ_of_lt _ _ h, Fin.succAbove_castSucc_of_le _ _ h.le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Misc (goal)
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₂ j : Fin (n + 1)
⊢ (M.submatrix j.succAbove id).det = Int.negOnePow (↑(↑j : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
have zero : (M.submatrix (Fin.succAbove 0) id).det = Int.negOnePow (↑(↑0 : ℕ) : ℤ) • (M.submatrix (Fin.succAbove 0) id).det
Tactic: induction j using Fin.induction with
  | zero => rw [Fin.val_zero, Nat.cast_zero, Int.negOnePow_zero, one_smul]
  | succ i h_ind =>
      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]
      congr
      ext a b
      simp_rw [neg_one_smul, updateRow_apply, Finset.sum_neg_distrib, Pi.neg_apply,
        Finset.sum_apply, submatrix_apply, id_eq]
      split_ifs with h
      · replace hv := congr_fun hv b
        rw [Fin.sum_univ_succAbove _ i.succ, Pi.add_apply, Finset.sum_apply] at hv
        rwa [h, Fin.succAbove_castSucc_self, neg_eq_iff_add_eq_zero, add_comm]
      · obtain h | h := ne_iff_lt_or_gt.mp h
        · rw [Fin.succAbove_castSucc_of_lt _ _ h,
            Fin.succAbove_of_succ_le _ _ (Fin.succ_lt_succ_iff.mpr h).le]
        · rw [Fin.succAbove_succ_of_lt _ _ h, Fin.succAbove_castSucc_of_le _ _ h.le]
Cleared hypotheses: j