Generalized Kronecker Delta sum snoc

lemma generalizedKroneckerDelta_sum_snoc {n : ℕ} (μ ν : Fin n → α) :    ∑ a : α, generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a)      = ((Fintype.card α : ℤ) - n) * generalizedKroneckerDelta μ ν := by  set A : Matrix (Fin n) (Fin n) ℤ :=    Matrix.of fun i j => ((kroneckerDelta (μ i) (ν j) : ℕ) : ℤ) with hA  set b : α → Fin n → ℤ := fun a j => ((kroneckerDelta a (ν j) : ℕ) : ℤ) with hb  -- Bordering the δ-matrix with the appended index (`Matrix.det_fromBlocks_one₂₂`) and the  -- rank-one update `Matrix.det_add_rankOne` express each summand through row updates of `A`.  have key (a : α) : generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a)      = A.det - ∑ i, ((kroneckerDelta (μ i) a : ℕ) : ℤ) * (A.updateRow i (b a)).det := by    set B : Matrix (Fin n) (Fin 1) ℤ :=      Matrix.of fun i _ => ((kroneckerDelta (μ i) a : ℕ) : ℤ) with hB    set C : Matrix (Fin 1) (Fin n) ℤ := Matrix.of fun _ j => b a j with hC    have hblk : (Matrix.of fun (i j : Fin (n + 1)) =>          ((kroneckerDelta ((Fin.snoc μ a : Fin (n + 1) → α) i)            ((Fin.snoc ν a : Fin (n + 1) → α) j) : ℕ) : ℤ)).submatrix          finSumFinEquiv finSumFinEquiv = Matrix.fromBlocks A B C 1 := by      simp only [← Fin.append_right_eq_snoc μ (fun _ => a), ← Fin.append_right_eq_snoc ν        (fun _ => a)]      ext (i | i) (j | j)      · simp [hA]      · simp [hB]      · simp [hC, hb]      · simp [Subsingleton.elim i j]    have hBC : A - B * C        = A + Matrix.of fun i j => -((kroneckerDelta (μ i) a : ℕ) : ℤ) * b a j := by      ext i j      simp [hB, hC, Matrix.mul_apply, sub_eq_add_neg]    rw [show generalizedKroneckerDelta (Fin.snoc μ a) (Fin.snoc ν a)          = ((Matrix.of fun (i j : Fin (n + 1)) =>            ((kroneckerDelta ((Fin.snoc μ a : Fin (n + 1) → α) i)              ((Fin.snoc ν a : Fin (n + 1) → α) j) : ℕ) : ℤ)).submatrix            finSumFinEquiv finSumFinEquiv).det from (Matrix.det_submatrix_equiv_self _ _).symm,      hblk, Matrix.det_fromBlocks_one₂₂, hBC, Matrix.det_add_rankOne]    simp only [neg_mul, Finset.sum_neg_distrib, ← sub_eq_add_neg]  -- Summing the row updates over the shared index restores `A` itself, once per row.  have hrow (i : Fin n) :      ∑ a : α, ((kroneckerDelta (μ i) a : ℕ) : ℤ) * (A.updateRow i (b a)).det = A.det := by    simp_rw [← nsmul_eq_mul, KroneckerDelta.sum_smul]    exact congrArg Matrix.det (A.updateRow_eq_self i)  rw [Finset.sum_congr rfl fun a _ => key a, Finset.sum_sub_distrib, Finset.sum_comm,    Finset.sum_congr rfl fun i _ => hrow i, Finset.sum_const, Finset.sum_const,    Finset.card_univ, Finset.card_univ, Fintype.card_fin,    show generalizedKroneckerDelta μ ν = A.det from rfl]  simp only [nsmul_eq_mul, ← sub_mul]