Levi Civita basis repr eq zero of eq

lemma leviCivita_basis_repr_eq_zero_of_eq    {b : ComponentIdx (S := realLorentzTensor 3) ![Color.up, Color.up, Color.up, Color.up]}    {i j : Fin 4} (hij : i ≠ j) (h : b i = b j) :    (Tensor.basis _).repr ε4 b = 0 := by  rw [leviCivita_basis_repr_apply]  have hdet : generalizedKroneckerDelta (fun i => finSumFinEquiv (b i))      (id : Fin 4 → Fin 4) = 0 := by    rw [show generalizedKroneckerDelta (fun i => finSumFinEquiv (b i)) (id : Fin 4 → Fin 4)          = Matrix.det (fun a c => ((kroneckerDelta (finSumFinEquiv (b a)) (id c) : ℕ) : ℤ))          from rfl]    refine Matrix.det_zero_of_row_eq hij (funext fun c => ?_)    rw [congrArg (⇑finSumFinEquiv) h]  rw [hdet, Int.cast_zero]