Sum generalized Kronecker Delta cons₂

lemma sum_generalizedKroneckerDelta_cons₂ (ρ σ τ ω : Fin 4) (k : ℕ) :    ∑ h : Fin k → Fin 4,        generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h)) (Fin.cons τ (Fin.cons ω h))      = (∏ j ∈ Finset.range k, ((2 : ℤ) - j))        * generalizedKroneckerDelta ![ρ, σ] ![τ, ω] := by  induction k with  | zero =>    rw [Finset.prod_range_zero, one_mul, Fintype.sum_unique]    have e1 : ∀ d : Fin 0 → Fin 4, (Fin.cons ρ (Fin.cons σ d) : Fin 2 → Fin 4) = ![ρ, σ] := by      intro d; funext i; fin_cases i <;> rfl    have e2 : ∀ d : Fin 0 → Fin 4, (Fin.cons τ (Fin.cons ω d) : Fin 2 → Fin 4) = ![τ, ω] := by      intro d; funext i; fin_cases i <;> rfl    rw [e1, e2]  | succ k ih =>    rw [sum_over_snoc]    have hstep : ∀ h' : Fin k → Fin 4, ∑ c : Fin 4,        generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ (Fin.snoc h' c)))          (Fin.cons τ (Fin.cons ω (Fin.snoc h' c)))          = ((2 : ℤ) - k) * generalizedKroneckerDelta (Fin.cons ρ (Fin.cons σ h'))              (Fin.cons τ (Fin.cons ω h')) := by      intro h'      rw [Finset.sum_congr rfl fun c _ => by        rw [Fin.cons_snoc_eq_snoc_cons, Fin.cons_snoc_eq_snoc_cons,          Fin.cons_snoc_eq_snoc_cons, Fin.cons_snoc_eq_snoc_cons],        generalizedKroneckerDelta_sum_snoc (Fin.cons ρ (Fin.cons σ h'))          (Fin.cons τ (Fin.cons ω 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