-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_updateRow_sum_aux (M : Matrix n n R) {j : n} (s : Finset n) (hj : j ∉ s) (c : n → R)
    (a : R) :
    (M.updateRow j (a • M j + ∑ k ∈ s, (c k) • M k)).det = a • M.det

Proof state:
case insert
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
c : n → R
a : R
k : n
s✝ : Finset n
hk : k ∉ s✝
h_ind : j ∉ s✝ → (M.updateRow j (a • M j + ∑ k ∈ s✝, c k • M k)).det = a • M.det
hj : j ∉ insert k s✝
h : k ≠ j
⊢ (M.updateRow j (a • M j + ∑ k ∈ insert k s✝, c k • M k)).det = a • M.det

Tactic:
rw [Finset.sum_insert hk, add_comm ((c k) • M k), ← add_assoc, det_updateRow_add,
  det_updateRow_smul, det_updateRow_eq_zero h, mul_zero, add_zero, h_ind]

Result:
case insert
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
c : n → R
a : R
k : n
s✝ : Finset n
hk : k ∉ s✝
h_ind : j ∉ s✝ → (M.updateRow j (a • M j + ∑ k ∈ s✝, c k • M k)).det = a • M.det
hj : j ∉ insert k s✝
h : k ≠ j
⊢ j ∉ s✝

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
s : Finset n
hj : j ∉ s
c : n → R
a : R
⊢ (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det

Tactic:
induction s using Finset.induction_on with
| empty => rw [Finset.sum_empty, add_zero, smul_eq_mul, det_updateRow_smul, updateRow_eq_self]
| @insert k _ hk h_ind =>
    have h : k ≠ j := fun h ↦ (h ▸ hj) (Finset.mem_insert_self _ _)
    rw [Finset.sum_insert hk, add_comm ((c k) • M k), ← add_assoc, det_updateRow_add,
      det_updateRow_smul, det_updateRow_eq_zero h, mul_zero, add_zero, h_ind]
    exact fun h ↦ hj (Finset.mem_insert_of_mem h)

Result:
no goals

Proof state:
case insert
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
c : n → R
a : R
k : n
s✝ : Finset n
hk : k ∉ s✝
h_ind : j ∉ s✝ → (M.updateRow j (a • M j + ∑ k ∈ s✝, c k • M k)).det = a • M.det
hj : j ∉ insert k s✝
h : k ≠ j
⊢ j ∉ s✝

Tactic:
exact fun h ↦ hj (Finset.mem_insert_of_mem h)

Result:
no goals

Proof state:
case insert
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
c : n → R
a : R
k : n
s✝ : Finset n
hk : k ∉ s✝
h_ind : j ∉ s✝ → (M.updateRow j (a • M j + ∑ k ∈ s✝, c k • M k)).det = a • M.det
hj : j ∉ insert k s✝
⊢ (M.updateRow j (a • M j + ∑ k ∈ insert k s✝, c k • M k)).det = a • M.det

Tactic:
have h : k ≠ j := fun h ↦ (h ▸ hj) (Finset.mem_insert_self _ _)

Result:
case insert
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
c : n → R
a : R
k : n
s✝ : Finset n
hk : k ∉ s✝
h_ind : j ∉ s✝ → (M.updateRow j (a • M j + ∑ k ∈ s✝, c k • M k)).det = a • M.det
hj : j ∉ insert k s✝
h : k ≠ j
⊢ (M.updateRow j (a • M j + ∑ k ∈ insert k s✝, c k • M k)).det = a • M.det

Proof state:
case empty
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
c : n → R
a : R
hj : j ∉ ∅
⊢ (M.updateRow j (a • M j + ∑ k ∈ ∅, c k • M k)).det = a • M.det

Tactic:
rw [Finset.sum_empty, add_zero, smul_eq_mul, det_updateRow_smul, updateRow_eq_self]

Result:
no goals