-- Mathlib/LinearAlgebra/Matrix/Determinant/Misc.lean
theorem det_eq_sum_column_mul_submatrix_succAbove_succAbove_det {n : ℕ}
    (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R) (i₀ j₀ : Fin (n + 1))
    (hv : ∀ j ≠ j₀, ∑ i, M i j = 0) :
    M.det = (-1) ^ (i₀ + j₀ : ℕ) *
      (∑ i, M i j₀) * (M.submatrix (Fin.succAbove i₀) (Fin.succAbove j₀)).det

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i : Fin (n + 1), M i j = 0
⊢ ∑ x : Fin n.succ, ((-1) ^ (↑i₀ + ↑x) * ∑ c : Fin (n + 1), M c x) * (M.submatrix i₀.succAbove x.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i : Fin (n + 1), M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
rw [Fintype.sum_eq_add_sum_subtype_ne _ j₀]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i : Fin (n + 1), M i j = 0
⊢ ((-1) ^ (↑i₀ + ↑j₀) * ∑ c : Fin (n + 1), M c j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det +
      ∑ i : { i // i ≠ j₀ },
        ((-1) ^ (↑i₀ + ↑↑i) * ∑ c : Fin (n + 1), M c ↑i) * (M.submatrix i₀.succAbove (↑i).succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i : Fin (n + 1), M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i : Fin (n + 1), M i j = 0
⊢ M.det = 1 • det ?m.19670

Tactic:
rw [one_smul]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i : Fin (n + 1), M i j = 0
⊢ ∑ j : Fin n.succ,
      (-1) ^ (↑i₀ + ↑j) * M.updateRow i₀ (∑ k : Fin (n + 1), 1 • M k) i₀ j *
        ((M.updateRow i₀ (∑ k : Fin (n + 1), 1 • M k)).submatrix i₀.succAbove j.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i : Fin (n + 1), M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
simp only [updateRow_apply, if_true, one_smul, submatrix_updateRow_succAbove, Finset.sum_apply]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i : Fin (n + 1), M i j = 0
⊢ ∑ x : Fin n.succ, ((-1) ^ (↑i₀ + ↑x) * ∑ c : Fin (n + 1), M c x) * (M.submatrix i₀.succAbove x.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i : Fin (n + 1), M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i : Fin (n + 1), M i j = 0
⊢ ((-1) ^ (↑i₀ + ↑j₀) * ∑ c : Fin (n + 1), M c j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det +
      ∑ i : { i // i ≠ j₀ },
        ((-1) ^ (↑i₀ + ↑↑i) * ∑ c : Fin (n + 1), M c ↑i) * (M.submatrix i₀.succAbove (↑i).succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i : Fin (n + 1), M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
conv_lhs =>
  enter [2, 2, i]
  rw [hv _ i.prop, mul_zero, zero_mul]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i : Fin (n + 1), M i j = 0
⊢ ((-1) ^ (↑i₀ + ↑j₀) * ∑ c : Fin (n + 1), M c j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det +
      ∑ i : { i // i ≠ j₀ }, 0 =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i : Fin (n + 1), M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i : Fin (n + 1), M i j = 0
⊢ ((-1) ^ (↑i₀ + ↑j₀) * ∑ c : Fin (n + 1), M c j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det +
      ∑ i : { i // i ≠ j₀ }, 0 =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i : Fin (n + 1), M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
simp [Finset.sum_const_zero, add_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i : Fin (n + 1), M i j = 0
⊢ M.det = ((-1) ^ (↑i₀ + ↑j₀) * ∑ i : Fin (n + 1), M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
rw [show M.det = (1 : R) • Matrix.det _ by rw [one_smul],
  ← Matrix.det_updateRow_sum _ i₀ (fun _ ↦ 1), Matrix.det_succ_row _ i₀]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i : Fin (n + 1), M i j = 0
⊢ ∑ j : Fin n.succ,
      (-1) ^ (↑i₀ + ↑j) * M.updateRow i₀ (∑ k : Fin (n + 1), 1 • M k) i₀ j *
        ((M.updateRow i₀ (∑ k : Fin (n + 1), 1 • M k)).submatrix i₀.succAbove j.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ i : Fin (n + 1), M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det