Rep Gauge Group I eq iff mul eq

lemma repGaugeGroupI_eq_iff_mul_eq {g₁ g₂ : GaugeGroupI} :    repGaugeGroupI g₁ = repGaugeGroupI g₂ ↔ ∀ i i',      star g₁.toU1.1 ^ 2 * g₁.toSU3.1 i' i =        star g₂.toU1.1 ^ 2 * g₂.toSU3.1 i' i := by  let b := RightHandedWeyl.basis.tensorProduct    (EuclideanSpace.basisFun (Fin 3) ℂ).toBasis  constructor  · intro h i i'    have h' := congrFun (congrArg (fun f => f.1) h)      ⟨RightHandedWeyl.basis 0 ⊗ₜ[ℂ] EuclideanSpace.basisFun (Fin 3) ℂ i⟩    simp only [Fin.isValue, LinearMap.coe_toAddHom, repGaugeGroupI_tmul_basis_eq_sum] at h'    replace h' := congrArg b.repr (congrArg valLinEquiv h')    simpa [Module.Basis.tensorProduct_repr_tmul_apply, -Fin.sum_univ_two, b] using      congrArg (fun f => f (0, i')) h'  · intro h    apply (valLinEquiv.symm.eq_comp_toLinearMap_iff      (repGaugeGroupI g₁) (repGaugeGroupI g₂)).mp    apply b.ext    rintro ⟨k, i⟩    have h₁ := repGaugeGroupI_tmul_basis_eq_sum g₁ k i    have h₂ := repGaugeGroupI_tmul_basis_eq_sum g₂ k i    simp only [EuclideanSpace.basisFun_apply] at h₁ h₂    simp [valLinEquiv_symm_apply, h₁, h₂, b]    apply Finset.sum_congr rfl    intro i' _    have hi' : (starRingEnd ℂ) g₁.toU1.1 ^ 2 * g₁.toSU3.1 i' i =        (starRingEnd ℂ) g₂.toU1.1 ^ 2 * g₂.toSU3.1 i' i := h i i'    rw [hi']