-- 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.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

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

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
⊢ (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

Proof state:
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

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

Result:
no goals

Proof state:
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
⊢ (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

Result:
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

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

Proof state:
case succ
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)).det =
    (M.submatrix i.castSucc.succAbove id).det

Tactic:
congr

Result:
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

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)
this : ∀ (j : Fin (n + 1)), (M.submatrix j.succAbove id).det = (↑↑j).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
⊢ (M.submatrix j₁.succAbove id).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix j₂.succAbove id).det

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

Result:
no goals

Proof state:
case zero
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 (Fin.succAbove 0) id).det = (↑↑0).negOnePow • (M.submatrix (Fin.succAbove 0) id).det

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

Result:
no goals

Proof state:
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

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

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 : 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

Proof state:
case succ
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).det = (↑↑i.succ).negOnePow • (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.coe_castSucc i, ← h_ind]

Result:
case succ
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)).det =
    (M.submatrix i.castSucc.succAbove id).det

Proof state:
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

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

Result:
no goals

Proof state:
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 : 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

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

Result:
no goals