From bc79ff5920386b29856c4ec983e1ff62a67cc299 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 19 Jul 2024 16:14:16 -0400
Subject: [PATCH] refactor: Multiplication

---
 HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
index d3f0cc0..a7e6d38 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
@@ -460,8 +460,7 @@ lemma mulS_assoc (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (U : Re
   rw [Finset.sum_congr rfl (fun x _ => Finset.sum_mul _ _ _)]
   rw [Finset.sum_congr rfl (fun x _ => Finset.mul_sum _ _ _)]
   rw [Finset.sum_comm]
-  refine Finset.sum_congr rfl (fun a _ => ?_)
-  refine Finset.sum_congr rfl (fun b _ => ?_)
+  refine Finset.sum_congr rfl (fun a _ => Finset.sum_congr rfl (fun b _ => ?_))
   rw [mul_assoc]
   refine Mathlib.Tactic.Ring.mul_congr rfl (Mathlib.Tactic.Ring.mul_congr ?_ rfl rfl) rfl
   apply congrArg
@@ -476,7 +475,8 @@ lemma mulS_assoc (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (U : Re
     · rw [mulSFstArg_on_not_mem, mulSSndArg_on_not_mem, mulSSndArg_on_not_mem,
         mulSFstArg_on_not_mem]
       rw [mulSAssocIndexValue, indexValueIso_eq_symm, indexValueIso_symm_apply']
-      simp [colorsIndexCast, Equiv.refl_apply]
+      simp only [ne_eq, Function.comp_apply, Equiv.symm_symm_apply, mulS_color, Sum.elim_inr,
+        colorsIndexCast, Equiv.cast_refl, Equiv.refl_symm]
       erw [Equiv.refl_apply]
       rfl
       exact hcy'