Sum generalized Kronecker Delta self

lemma sum_generalizedKroneckerDelta_self (k : ℕ) :    ∑ h : Fin k → Fin 4, generalizedKroneckerDelta h h      = ∏ j ∈ Finset.range k, ((4 : ℤ) - j) := by  induction k with  | zero =>    rw [Finset.prod_range_zero, Fintype.sum_unique]    exact Matrix.det_fin_zero  | succ k ih =>    rw [sum_over_snoc]    have hstep : ∀ h' : Fin k → Fin 4, ∑ c : Fin 4,        generalizedKroneckerDelta (Fin.snoc h' c) (Fin.snoc h' c)          = ((4 : ℤ) - k) * generalizedKroneckerDelta h' h' := by      intro h'      rw [generalizedKroneckerDelta_sum_snoc h' h', Fintype.card_fin]      push_cast      ring    rw [Finset.sum_congr rfl fun h' _ => hstep h', ← Finset.mul_sum, ih,      Finset.prod_range_succ]    ring