-- Mathlib/LinearAlgebra/Matrix/Determinant/Misc.lean
theorem submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det {n : ℕ}
    (M : Matrix (Fin (n + 1)) (Fin n) R) (hv : ∑ j, M j = 0) (j₁ j₂ : Fin (n + 1)) :
    (M.submatrix (Fin.succAbove j₁) id).det =
      Int.negOnePow (j₁ - j₂) • (M.submatrix (Fin.succAbove j₂) id).det

Proof state:
case succ.e_M
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j : Fin (n + 1), M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
⊢ (M.submatrix i.succ.succAbove id).updateRow i (∑ k : Fin n, -1 • M.submatrix i.succ.succAbove id k) =
    M.submatrix i.castSucc.succAbove id

Tactic:
ext a b

Result:
case succ.e_M.a
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j : Fin (n + 1), M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
⊢ (M.submatrix i.succ.succAbove id).updateRow i (∑ k : Fin n, -1 • M.submatrix i.succ.succAbove id k) a b =
    M.submatrix i.castSucc.succAbove id a b

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j : Fin (n + 1), M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (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

Tactic:
replace hv := congr_fun hv b

Result:
case pos
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 = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : a = i
hv : (∑ j : Fin (n + 1), M j) b = 0 b
⊢ -∑ x : Fin n, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j : Fin (n + 1), M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (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

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

Result:
case neg.inl
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j : Fin (n + 1), M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h✝ : ¬a = i
h : a < i
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b

case neg.inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j : Fin (n + 1), M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h✝ : ¬a = i
h : a > i
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j : Fin (n + 1), M j = 0
j₁ j₂ : Fin (n + 1)
⊢ ∀ (j : Fin (n + 1)), (M.submatrix j.succAbove id).det = (↑↑j).negOnePow • (M.submatrix (Fin.succAbove 0) id).det

Tactic:
intro j

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j : Fin (n + 1), M j = 0
j₁ j₂ j : Fin (n + 1)
⊢ (M.submatrix j.succAbove id).det = (↑↑j).negOnePow • (M.submatrix (Fin.succAbove 0) id).det

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j : Fin (n + 1), M j = 0
j₁ j₂ : Fin (n + 1)
⊢ (M.submatrix j₁.succAbove id).det = (↑↑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]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j : Fin (n + 1), M j = 0
j₁ j₂ : Fin (n + 1)
⊢ ∀ (j : Fin (n + 1)), (M.submatrix j.succAbove id).det = (↑↑j).negOnePow • (M.submatrix (Fin.succAbove 0) id).det