From bc2db84389a9787358ffa85bc3bb8d1f8ba7eeb5 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 18 Jul 2024 16:34:00 -0400
Subject: [PATCH 1/6] feat: mult on arbitary index

---
 .../SpaceTime/LorentzTensor/Real/Basic.lean   | 151 +++++++++++++++++-
 .../LorentzTensor/Real/Constructors.lean      |  60 +++++--
 .../LorentzTensor/Real/Multiplication.lean    |  81 ++++++++++
 3 files changed, 274 insertions(+), 18 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index 15c753f..aea5a09 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -8,6 +8,7 @@ import Mathlib.Data.Real.Basic
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Logic.Equiv.Fin
 import Mathlib.Tactic.FinCases
+import Mathlib.Logic.Equiv.Fintype
 /-!
 
 # Real Lorentz Tensors
@@ -386,9 +387,8 @@ def twoMarkedIndexValue (T : Marked d X 2) (x : ColorsIndex d (T.color (markedPo
   | 1 => y
 
 /-- An equivalence of types used to turn the first marked index into an unmarked index. -/
-def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃
-    (X ⊕ Fin 1) ⊕ Fin n :=
-  trans (Equiv.sumCongr (Equiv.refl _) $
+def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃ (X ⊕ Fin 1) ⊕ Fin n :=
+  trans (Equiv.sumCongr (Equiv.refl _)
     (((Fin.castOrderIso (Nat.succ_eq_one_add n)).toEquiv.trans finSumFinEquiv.symm)))
   (Equiv.sumAssoc _ _ _).symm
 
@@ -396,6 +396,151 @@ def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃
 def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ Fin 1) n :=
   mapIso d (unmarkFirstSet X n)
 
+@[simps!]
+def notInImage {n m : ℕ} (f : Fin m ↪ Fin (n + m)) :
+    Fin n ≃ {x // x ∈ (Finset.image (⇑f) Finset.univ)ᶜ} :=
+  (Finset.orderIsoOfFin (Finset.image f Finset.univ)ᶜ (by rw [Finset.card_compl,
+    Finset.card_image_of_injective _ (Function.Embedding.injective f)]; simp)).toEquiv
+
+@[simps!]
+def splitMarkedIndices {n m : ℕ} (f : Fin m ↪ Fin (n + m)) : Fin (n + m) ≃ Fin n ⊕ Fin m :=
+  (Equiv.Set.sumCompl (Set.range ⇑f)).symm.trans <|
+  (Equiv.sumComm _ _).trans <|
+  Equiv.sumCongr ((Equiv.subtypeEquivRight (by simp)).trans (notInImage f).symm) <|
+  (Function.Embedding.toEquivRange f).symm
+
+@[simps!]
+def oneEmbed {n : ℕ} (i : Fin n.succ) : Fin 1 ↪ Fin n.succ :=
+  ⟨fun _ => i, fun x y => by fin_cases x; fin_cases y; simp⟩
+
+@[simps!]
+def splitMarkedIndicesOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin n ⊕ Fin 1 :=
+  splitMarkedIndices (oneEmbed i)
+
+lemma splitMarkedIndicesOne_self {n : ℕ} (i : Fin n.succ) :
+    splitMarkedIndicesOne i i = Sum.inr 0 := by
+  rw [splitMarkedIndicesOne, splitMarkedIndices]
+  have h1 : (Equiv.Set.sumCompl (Set.range (oneEmbed i))).symm i =
+      Sum.inl ⟨i, by simp⟩ := by
+    rw  [Equiv.Set.sumCompl_symm_apply_of_mem]
+  simp
+  rw [h1]
+  change Sum.inr ((⇑(oneEmbed i).toEquivRange.symm) (⟨(oneEmbed i) 0, _⟩)) = Sum.inr 0
+  congr
+  rw [Function.Embedding.toEquivRange_symm_apply_self]
+
+lemma notInImage_oneEmbed {n : ℕ} (i : Fin n.succ) :
+    (notInImage (oneEmbed i)).toFun = fun x => ⟨i.succAbove x, by simpa using Fin.succAbove_ne i x⟩ := by
+  symm
+  simp [notInImage]
+  funext x
+  apply Subtype.ext
+  rw [Finset.coe_orderIsoOfFin_apply]
+  symm
+  apply congrFun
+  symm
+  apply Finset.orderEmbOfFin_unique
+  intro x
+  simp
+  exact Fin.succAbove_ne i x
+  exact Fin.strictMono_succAbove i
+
+lemma splitMarkedIndicesOne_not_self {n : ℕ} {i j : Fin n.succ.succ} (hij : i ≠ j) :
+    splitMarkedIndicesOne i j = Sum.inl ((Fin.predAbove 0 i).predAbove j) := by
+  rw [splitMarkedIndicesOne, splitMarkedIndices]
+  have h1 : (Equiv.Set.sumCompl (Set.range (oneEmbed i))).symm j =
+      Sum.inr ⟨j, by simp [hij]⟩ := by
+    rw [Equiv.Set.sumCompl_symm_apply_of_not_mem]
+  simp
+  rw [h1]
+  change Sum.inl ((⇑(notInImage (oneEmbed i)).symm ∘ ⇑(Equiv.subtypeEquivRight _))
+    ⟨j, _⟩) = _
+  apply congrArg
+  simp
+  rw [Equiv.symm_apply_eq]
+  change _ = (notInImage (oneEmbed i)).toFun ((Fin.predAbove 0 i).predAbove j)
+  rw [notInImage_oneEmbed]
+  simp
+  apply Subtype.ext
+  simp
+  simp [Fin.succAbove, Fin.predAbove, Fin.lt_def]
+  split <;> split <;> simp <;> split <;> apply Fin.ext_iff.mpr
+    <;> rename_i _ h2 h3 h4 <;> simp at h1 h2 h3 h4  <;> omega
+
+
+@[simps!]
+def markSelectedIndex (i : Fin n.succ) : Marked d X n.succ ≃ Marked d (X ⊕ Fin n) 1 :=
+  mapIso d ((Equiv.sumCongr (Equiv.refl X) (splitMarkedIndicesOne i)).trans
+    (Equiv.sumAssoc _ _ _).symm)
+
+lemma markSelectedIndex_markedColor (T : Marked d X n.succ) (i : Fin n.succ) :
+    (markSelectedIndex i T).markedColor 0 = T.markedColor i := rfl
+
+/-! TODO: Simplify prove and move. -/
+lemma succAbove_predAbove_predAbove (i p : Fin n.succ.succ) (hip : i ≠ p) :
+     i.succAbove ((Fin.predAbove 0 i).predAbove p) = p := by
+  simp [Fin.succAbove, Fin.predAbove, Fin.lt_def]
+  split <;> split <;> simp   <;> rw [Fin.ext_iff] <;> simp
+  intro h
+  all_goals
+    rename_i h1 h2
+    simp at h1 h2
+    omega
+
+@[simps!]
+def equivDropPoint  (e : Fin n.succ ≃ Fin m.succ) {i : Fin n.succ} {j : Fin m.succ} (he : e i = j) :
+    Fin n ≃ Fin m :=
+  (notInImage (oneEmbed i)).trans <|
+  (Equiv.subtypeEquivOfSubtype' e).trans  <|
+  (Equiv.subtypeEquivRight (fun x => by simp [oneEmbed, Equiv.symm_apply_eq, he])).trans <|
+  (notInImage (oneEmbed j)).symm
+
+
+lemma markSelectedIndex_mapIso (f : X ≃ Y) (e : Fin n.succ.succ ≃ Fin m.succ.succ) (i : Fin n.succ.succ)
+    (j : Fin m.succ.succ) (he : e i = j) (T : Marked d X n.succ.succ) :
+    mapIso d (Equiv.sumCongr (Equiv.sumCongr f (equivDropPoint e he)) (Equiv.refl (Fin 1)))
+    (markSelectedIndex i T) = markSelectedIndex j (mapIso d (Equiv.sumCongr f e) T) := by
+  rw [markSelectedIndex, markSelectedIndex]
+  erw [← Equiv.trans_apply, ← Equiv.trans_apply]
+  rw [mapIso_trans, mapIso_trans]
+  apply congrFun
+  apply congrArg
+  apply congrArg
+  apply Equiv.ext
+  intro x
+  match x with
+  | Sum.inl x => rfl
+  | Sum.inr x =>
+    simp only [Nat.succ_eq_add_one, Equiv.trans_apply, Equiv.coe_refl,
+       Fin.isValue]
+    change  ((f.sumCongr (equivDropPoint e he)).sumCongr (Equiv.refl (Fin 1)))
+      ((Equiv.sumAssoc X (Fin n.succ) (Fin 1)).symm (Sum.inr ((splitMarkedIndicesOne i) x)))  =
+      (Equiv.sumAssoc Y (Fin m.succ) (Fin 1)).symm (Sum.inr ((splitMarkedIndicesOne j) (e x)))
+    by_cases h : x = i
+    subst h
+    rw [he]
+    rw [splitMarkedIndicesOne_self, splitMarkedIndicesOne_self]
+    simp
+    subst he
+    rw [splitMarkedIndicesOne_not_self (fun a => h a.symm), splitMarkedIndicesOne_not_self]
+    simp [equivDropPoint]
+    rw [Equiv.symm_apply_eq]
+    change _ =
+      (notInImage (oneEmbed (e i))).toFun ((Fin.predAbove 0 (e i)).predAbove (e x))
+    rw [notInImage_oneEmbed]
+    simp
+    apply Subtype.ext
+    simp
+    change (e.subtypeEquivOfSubtype'
+      ((notInImage (oneEmbed i)).toFun ((Fin.predAbove 0 i).predAbove x))).1 = _
+    rw [notInImage_oneEmbed]
+    rw [Equiv.subtypeEquivOfSubtype', Equiv.subtypeEquivOfSubtype]
+    simp
+    rw [succAbove_predAbove_predAbove, succAbove_predAbove_predAbove]
+    exact e.apply_eq_iff_eq.mp.mt (fun a => h a.symm)
+    exact fun a => h a.symm
+    exact e.apply_eq_iff_eq.mp.mt (fun a => h a.symm)
+
 end Marked
 
 /-!
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
index a349177..60369d5 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
@@ -18,6 +18,43 @@ We will derive properties of these constructors.
 -/
 
 namespace RealLorentzTensor
+/-!
+
+# Tensors from and to the reals
+
+An important point that we shall see here is that there is a well defined map
+to the real numbers, i.e. which is invariant under transformations of mapIso.
+
+-/
+
+/-- An equivalence from Real tensors on an empty set to `ℝ`. -/
+@[simps!]
+def toReal (d : ℕ) {X : Type} (h : IsEmpty X) : RealLorentzTensor d X ≃ ℝ where
+  toFun := fun T => T.coord (IsEmpty.elim h)
+  invFun := fun r => {
+    color := fun x => IsEmpty.elim h x,
+    coord := fun _ => r}
+  left_inv T := by
+    refine ext ?_ ?_
+    funext x
+    exact IsEmpty.elim h x
+    funext a
+    change T.coord (IsEmpty.elim h) = _
+    apply congrArg
+    funext x
+    exact IsEmpty.elim h x
+  right_inv x := rfl
+
+/-- The real number obtained from a tensor is invariant under `mapIso`. -/
+lemma toReal_mapIso (d : ℕ) {X Y : Type} (h : IsEmpty X) (f : X ≃ Y) :
+    (mapIso d f).trans (toReal d (Equiv.isEmpty f.symm)) = toReal d h := by
+  apply Equiv.ext
+  intro x
+  simp
+  apply congrArg
+  funext x
+  exact IsEmpty.elim h x
+
 
 /-!
 
@@ -28,11 +65,6 @@ action of the Lorentz group. They are provided for constructive purposes.
 
 -/
 
-/-- A 0-tensor from a real number. -/
-def ofReal (d : ℕ) (r : ℝ) : RealLorentzTensor d Empty where
-  color := fun _ => Colors.up
-  coord := fun _ => r
-
 /-- A marked 1-tensor with a single up index constructed from a vector.
 
   Note: This is not the same as rising indices on `ofVecDown`. -/
@@ -186,14 +218,14 @@ open Marked
 
 /-- Contracting the indices of `ofMatUpDown` returns the trace of the matrix. -/
 lemma contr_ofMatUpDown_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
-    contr (ofMatUpDown M) (by rfl) = ofReal d M.trace := by
+    contr (ofMatUpDown M) (by rfl) = (toReal d instIsEmptyEmpty).symm M.trace := by
   refine ext ?_ rfl
   · funext i
     exact Empty.elim i
 
 /-- Contracting the indices of `ofMatDownUp` returns the trace of the matrix. -/
 lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) :
-    contr (ofMatDownUp M) (by rfl) = ofReal d M.trace := by
+    contr (ofMatDownUp M) (by rfl) = (toReal d instIsEmptyEmpty).symm M.trace := by
   refine ext ?_ rfl
   · funext i
     exact Empty.elim i
@@ -207,20 +239,18 @@ lemma contr_ofMatDownUp_eq_trace {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
 /-- Multiplying `ofVecUp` with `ofVecDown` gives the dot product. -/
 @[simp]
 lemma mul_ofVecUp_ofVecDown_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
-    mapIso d (@Equiv.equivEmpty (Empty ⊕ Empty) instIsEmptySum)
-    (mul (ofVecUp v₁) (ofVecDown v₂) (by rfl)) = ofReal d (v₁ ⬝ᵥ v₂) := by
+    mul (ofVecUp v₁) (ofVecDown v₂) rfl = (toReal d instIsEmptySum).symm (v₁ ⬝ᵥ v₂) := by
   refine ext ?_ rfl
   · funext i
-    exact Empty.elim i
+    exact IsEmpty.elim instIsEmptySum i
 
 /-- Multiplying `ofVecDown` with `ofVecUp` gives the dot product. -/
 @[simp]
 lemma mul_ofVecDown_ofVecUp_eq_dot_prod {d : ℕ} (v₁ v₂ : Fin 1 ⊕ Fin d → ℝ) :
-    mapIso d (Equiv.equivEmpty (Empty ⊕ Empty))
-    (mul (ofVecDown v₁) (ofVecUp v₂) rfl) = ofReal d (v₁ ⬝ᵥ v₂) := by
+    mul (ofVecDown v₁) (ofVecUp v₂) rfl = (toReal d instIsEmptySum).symm (v₁ ⬝ᵥ v₂) := by
   refine ext ?_ rfl
   · funext i
-    exact Empty.elim i
+    exact IsEmpty.elim instIsEmptySum i
 
 lemma mul_ofMatUpDown_ofVecUp_eq_mulVec {d : ℕ} (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (v : Fin 1 ⊕ Fin d → ℝ) :
@@ -255,8 +285,8 @@ open Matrix
 
 /-- The action of the Lorentz group on `ofReal v` is trivial. -/
 @[simp]
-lemma lorentzAction_ofReal (r : ℝ) : Λ • ofReal d r = ofReal d r :=
-  lorentzAction_on_isEmpty Λ (ofReal d r)
+lemma lorentzAction_toReal (h : IsEmpty X) (r : ℝ) : Λ • (toReal d h).symm r = (toReal d h).symm r :=
+  lorentzAction_on_isEmpty Λ  ((toReal d h).symm r)
 
 /-- The action of the Lorentz group on `ofVecUp v` is by vector multiplication. -/
 @[simp]
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
index 6cc5629..8e70920 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
@@ -231,4 +231,85 @@ lemma mul_lorentzAction (T : Marked d X 1) (S : Marked d Y 1)
   simp only [← marked_unmarked_action_eq_action]
   rw [mul_markedLorentzAction, mul_unmarkedLorentzAction]
 
+/-!
+
+## Multiplication on selected indices
+
+-/
+
+variable {n m : ℕ}
+
+def mulSSetEquiv : (X ⊕ Fin n) ⊕ Y ⊕ Fin m ≃ (X ⊕ Y) ⊕ (Fin (n + m)) :=
+  (Equiv.sumAssoc _ _ _).trans <|
+  (Equiv.sumCongr (Equiv.refl _ ) (Equiv.sumAssoc _ _ _).symm).trans <|
+  (Equiv.sumCongr (Equiv.refl _ ) (Equiv.sumCongr (Equiv.sumComm _ _) (Equiv.refl _)).symm).trans <|
+  (Equiv.sumAssoc _ _ _).symm.trans <|
+  (Equiv.sumCongr (Equiv.sumAssoc _ _ _) (Equiv.refl _ )).symm.trans <|
+  (Equiv.sumAssoc _ _ _).trans <|
+  Equiv.sumCongr (Equiv.refl _) finSumFinEquiv
+
+@[simps!]
+def mulS (T : Marked d X n.succ) (S : Marked d Y m.succ) (i : Fin n.succ) (j : Fin m.succ)
+    (h : T.markedColor i = τ (S.markedColor j)) : Marked d (X ⊕ Y) (n + m) :=
+  mapIso d mulSSetEquiv (mul (markSelectedIndex i T) (markSelectedIndex j S) h)
+
+
+/-- Given a marked index of `T` and returns a marked index of `mulS T S _ _ _`. -/
+def mulSInl {n m : ℕ} {i j : Fin n.succ.succ} (h : j ≠ i) : Fin (n.succ + m) :=
+  finSumFinEquiv <|
+  Sum.inl <|
+  (notInImage (oneEmbed i)).symm <|
+  ⟨j, by simp [oneEmbed, h]⟩
+
+/-- Given a marked index of `S` and returns a marked index of `mulS S T _ _ _`. -/
+def mulSInr {n m : ℕ} {i j : Fin m.succ.succ} (h : j ≠ i) : Fin (n + m.succ) :=
+  finSumFinEquiv <|
+  Sum.inr <|
+  (notInImage (oneEmbed i)).symm <|
+  ⟨j, by simp [oneEmbed, h]⟩
+
+lemma mulSInl_mulSSetEquiv {n m : ℕ} {i j : Fin n.succ.succ} (h : j ≠ i) :
+    (@mulSSetEquiv X Y n.succ m).symm (Sum.inr (mulSInl h)) =
+    Sum.inl (Sum.inr ((notInImage (oneEmbed i)).symm  ⟨j, by simp [oneEmbed, h]⟩)) := by
+  rw [Equiv.symm_apply_eq]
+  rfl
+
+lemma mulSInr_mulSSetEquiv {n m : ℕ} {i j : Fin m.succ.succ} (h : j ≠ i) :
+    (@mulSSetEquiv X Y n m.succ).symm (Sum.inr (mulSInr h)) =
+    Sum.inr (Sum.inr ((notInImage (oneEmbed i)).symm  ⟨j, by simp [oneEmbed, h]⟩)) := by
+  rw [Equiv.symm_apply_eq]
+  rfl
+/-
+@[simp]
+lemma mulSInl_color {n m : ℕ}
+    (T : Marked d X n.succ.succ) (S : Marked d Y m.succ) (a b : Fin n.succ.succ) (c : Fin m.succ)
+    (h : T.markedColor a = τ (S.markedColor c)) (hab : b ≠ a):
+    (mulS T S a c h).markedColor (mulSInl hab) = T.markedColor b := by
+  rw [markedColor]
+  simp [mulS_color]
+  rw [mulSInl_mulSSetEquiv]
+  simp  [unmarkedColor, markSelectedIndex, Nat.succ_eq_add_one, Fintype.univ_ofSubsingleton,
+    Fin.zero_eta, Fin.isValue, notInImage, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv,
+    Sum.elim_inl, Function.comp_apply, mapIso_apply_color, Equiv.symm_trans_apply,
+    Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.symm_symm, Equiv.sumAssoc_apply_inl_inr,
+    Equiv.sumCongr_apply, Equiv.coe_refl, Sum.map_inr, splitMarkedIndicesOne_symm_apply,
+    Sum.map_inl, OrderIso.symm_symm, OrderIso.apply_symm_apply, Equiv.coe_fn_symm_mk, Sum.swap_inl,
+    Equiv.Set.sumCompl_apply_inr, markedColor]
+
+@[simp]
+lemma mulSInr_color {n m : ℕ}
+    (T : Marked d X n.succ) (S : Marked d Y m.succ.succ) (c : Fin n.succ) (a b : Fin m.succ.succ)
+    (h : T.markedColor c = τ (S.markedColor a)) (hab : b ≠ a) :
+    (mulS T S c a h).markedColor (mulSInr hab) = S.markedColor b := by
+  rw [markedColor]
+  simp [mulS_color]
+  rw [mulSInr_mulSSetEquiv]
+  simp only [unmarkedColor, markSelectedIndex, Nat.succ_eq_add_one, Fintype.univ_ofSubsingleton,
+    Fin.zero_eta, Fin.isValue, notInImage, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv,
+    Sum.elim_inr, Function.comp_apply, mapIso_apply_color, Equiv.symm_trans_apply,
+    Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.symm_symm, Equiv.sumAssoc_apply_inl_inr,
+    Equiv.sumCongr_apply, Equiv.coe_refl, Sum.map_inr, splitMarkedIndicesOne_symm_apply,
+    Sum.map_inl, OrderIso.symm_symm, OrderIso.apply_symm_apply, Equiv.coe_fn_symm_mk, Sum.swap_inl,
+    Equiv.Set.sumCompl_apply_inr, markedColor]
+-/
 end RealLorentzTensor

From 99ccbb5d04ece7cd8ee7dff6959c49983b352676 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 19 Jul 2024 15:46:43 -0400
Subject: [PATCH 2/6] feat: Associativity of multiplication

---
 .../SpaceTime/LorentzTensor/Real/Basic.lean   | 326 +++++++++++-------
 .../LorentzTensor/Real/Constructors.lean      |   8 +-
 .../LorentzTensor/Real/Multiplication.lean    | 314 +++++++++++++----
 3 files changed, 451 insertions(+), 197 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index aea5a09..aeddde7 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -166,7 +166,7 @@ lemma indexValueIso_symm (d : ℕ) (f : X ≃ Y) (h : i = j ∘ f) :
   rw [← Equiv.symm_apply_eq]
   funext y
   rw [indexValueIso_symm_apply', indexValueIso_symm_apply']
-  simp [colorsIndexCast]
+  simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast]
   apply cast_eq_iff_heq.mpr
   rw [Equiv.apply_symm_apply]
 
@@ -396,150 +396,226 @@ def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃ (X ⊕ Fin 1) 
 def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ Fin 1) n :=
   mapIso d (unmarkFirstSet X n)
 
-@[simps!]
-def notInImage {n m : ℕ} (f : Fin m ↪ Fin (n + m)) :
-    Fin n ≃ {x // x ∈ (Finset.image (⇑f) Finset.univ)ᶜ} :=
-  (Finset.orderIsoOfFin (Finset.image f Finset.univ)ᶜ (by rw [Finset.card_compl,
-    Finset.card_image_of_injective _ (Function.Embedding.injective f)]; simp)).toEquiv
+/-!
 
-@[simps!]
-def splitMarkedIndices {n m : ℕ} (f : Fin m ↪ Fin (n + m)) : Fin (n + m) ≃ Fin n ⊕ Fin m :=
+## Marking elements.
+
+-/
+section markingElements
+
+variable [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
+
+/-- Splits a type based on an embedding from `Fin n` into elements not in the image of the
+  embedding, and elements in the image. -/
+def markEmbeddingSet {n : ℕ} (f : Fin n ↪ X) :
+    X ≃ {x // x ∈ (Finset.image f Finset.univ)ᶜ} ⊕ Fin n :=
   (Equiv.Set.sumCompl (Set.range ⇑f)).symm.trans <|
   (Equiv.sumComm _ _).trans <|
-  Equiv.sumCongr ((Equiv.subtypeEquivRight (by simp)).trans (notInImage f).symm) <|
+  Equiv.sumCongr ((Equiv.subtypeEquivRight (by simp))) <|
   (Function.Embedding.toEquivRange f).symm
 
+lemma markEmbeddingSet_on_mem {n : ℕ} (f : Fin n ↪ X) (x : X)
+    (hx : x ∈ Finset.image f Finset.univ) : markEmbeddingSet f x =
+    Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩) := by
+  rw [markEmbeddingSet]
+  simp only [Equiv.trans_apply, Equiv.sumComm_apply, Equiv.sumCongr_apply]
+  rw [Equiv.Set.sumCompl_symm_apply_of_mem]
+  rfl
+
+lemma markEmbeddingSet_on_not_mem {n : ℕ} (f : Fin n ↪ X) (x : X)
+    (hx : ¬ x ∈ (Finset.image f Finset.univ)) : markEmbeddingSet f x =
+    Sum.inl ⟨x, by simpa using hx⟩ := by
+  rw [markEmbeddingSet]
+  simp only [Equiv.trans_apply, Equiv.sumComm_apply, Equiv.sumCongr_apply]
+  rw [Equiv.Set.sumCompl_symm_apply_of_not_mem]
+  rfl
+  simpa using hx
+
+/-- Marks the indicies of tensor in the image of an embedding. -/
 @[simps!]
-def oneEmbed {n : ℕ} (i : Fin n.succ) : Fin 1 ↪ Fin n.succ :=
-  ⟨fun _ => i, fun x y => by fin_cases x; fin_cases y; simp⟩
+def markEmbedding {n : ℕ} (f : Fin n ↪ X) :
+    RealLorentzTensor d X ≃ Marked d {x // x ∈ (Finset.image f Finset.univ)ᶜ} n :=
+  mapIso d (markEmbeddingSet f)
 
-@[simps!]
-def splitMarkedIndicesOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin n ⊕ Fin 1 :=
-  splitMarkedIndices (oneEmbed i)
-
-lemma splitMarkedIndicesOne_self {n : ℕ} (i : Fin n.succ) :
-    splitMarkedIndicesOne i i = Sum.inr 0 := by
-  rw [splitMarkedIndicesOne, splitMarkedIndices]
-  have h1 : (Equiv.Set.sumCompl (Set.range (oneEmbed i))).symm i =
-      Sum.inl ⟨i, by simp⟩ := by
-    rw  [Equiv.Set.sumCompl_symm_apply_of_mem]
-  simp
-  rw [h1]
-  change Sum.inr ((⇑(oneEmbed i).toEquivRange.symm) (⟨(oneEmbed i) 0, _⟩)) = Sum.inr 0
-  congr
-  rw [Function.Embedding.toEquivRange_symm_apply_self]
-
-lemma notInImage_oneEmbed {n : ℕ} (i : Fin n.succ) :
-    (notInImage (oneEmbed i)).toFun = fun x => ⟨i.succAbove x, by simpa using Fin.succAbove_ne i x⟩ := by
+lemma markEmbeddingSet_on_mem_indexValue_apply {n : ℕ} (f : Fin n ↪ X) (T : RealLorentzTensor d X)
+    (i : IndexValue d (markEmbedding f T).color) (x : X) (hx : x ∈ (Finset.image f Finset.univ)) :
+    i (markEmbeddingSet f x) = colorsIndexCast (congrArg ((markEmbedding f) T).color
+    (markEmbeddingSet_on_mem f x hx).symm)
+    (i (Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩))) := by
+  simp [colorsIndexCast]
   symm
-  simp [notInImage]
-  funext x
-  apply Subtype.ext
-  rw [Finset.coe_orderIsoOfFin_apply]
+  apply cast_eq_iff_heq.mpr
+  rw [markEmbeddingSet_on_mem f x hx]
+
+lemma markEmbeddingSet_on_not_mem_indexValue_apply {n : ℕ}
+    (f : Fin n ↪ X) (T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color)
+    (x : X) (hx : ¬ x ∈ (Finset.image f Finset.univ)) :
+    i (markEmbeddingSet f x) = colorsIndexCast (congrArg ((markEmbedding f) T).color
+    (markEmbeddingSet_on_not_mem f x hx).symm) (i (Sum.inl ⟨x, by simpa using hx⟩)) := by
+  simp [colorsIndexCast]
   symm
-  apply congrFun
-  symm
-  apply Finset.orderEmbOfFin_unique
-  intro x
-  simp
-  exact Fin.succAbove_ne i x
-  exact Fin.strictMono_succAbove i
-
-lemma splitMarkedIndicesOne_not_self {n : ℕ} {i j : Fin n.succ.succ} (hij : i ≠ j) :
-    splitMarkedIndicesOne i j = Sum.inl ((Fin.predAbove 0 i).predAbove j) := by
-  rw [splitMarkedIndicesOne, splitMarkedIndices]
-  have h1 : (Equiv.Set.sumCompl (Set.range (oneEmbed i))).symm j =
-      Sum.inr ⟨j, by simp [hij]⟩ := by
-    rw [Equiv.Set.sumCompl_symm_apply_of_not_mem]
-  simp
-  rw [h1]
-  change Sum.inl ((⇑(notInImage (oneEmbed i)).symm ∘ ⇑(Equiv.subtypeEquivRight _))
-    ⟨j, _⟩) = _
-  apply congrArg
-  simp
-  rw [Equiv.symm_apply_eq]
-  change _ = (notInImage (oneEmbed i)).toFun ((Fin.predAbove 0 i).predAbove j)
-  rw [notInImage_oneEmbed]
-  simp
-  apply Subtype.ext
-  simp
-  simp [Fin.succAbove, Fin.predAbove, Fin.lt_def]
-  split <;> split <;> simp <;> split <;> apply Fin.ext_iff.mpr
-    <;> rename_i _ h2 h3 h4 <;> simp at h1 h2 h3 h4  <;> omega
-
+  apply cast_eq_iff_heq.mpr
+  rw [markEmbeddingSet_on_not_mem f x hx]
 
+/-- An equivalence between the IndexValues for a tensor `T` and the corresponding
+  tensor with indicies maked by an embedding. -/
 @[simps!]
-def markSelectedIndex (i : Fin n.succ) : Marked d X n.succ ≃ Marked d (X ⊕ Fin n) 1 :=
-  mapIso d ((Equiv.sumCongr (Equiv.refl X) (splitMarkedIndicesOne i)).trans
-    (Equiv.sumAssoc _ _ _).symm)
+def markEmbeddingIndexValue {n : ℕ} (f : Fin n ↪ X) (T : RealLorentzTensor d X) :
+    IndexValue d T.color ≃ IndexValue d (markEmbedding f T).color :=
+  indexValueIso d (markEmbeddingSet f) (
+    (Equiv.comp_symm_eq (markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl)
 
-lemma markSelectedIndex_markedColor (T : Marked d X n.succ) (i : Fin n.succ) :
-    (markSelectedIndex i T).markedColor 0 = T.markedColor i := rfl
+lemma markEmbeddingIndexValue_apply_symm_on_mem {n : ℕ}
+    (f : Fin n.succ ↪ X) (T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color)
+    (x : X) (hx : x ∈ (Finset.image f Finset.univ)) :
+    (markEmbeddingIndexValue f T).symm i x = (colorsIndexCast ((congrFun ((Equiv.comp_symm_eq
+    (markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl) x).trans
+    (congrArg ((markEmbedding f) T).color (markEmbeddingSet_on_mem f x hx)))).symm
+    (i (Sum.inr (f.toEquivRange.symm ⟨x, by simpa using hx⟩))) := by
+  rw [markEmbeddingIndexValue, indexValueIso_symm_apply']
+  rw [markEmbeddingSet_on_mem_indexValue_apply f T i x hx]
+  simp [colorsIndexCast]
 
-/-! TODO: Simplify prove and move. -/
-lemma succAbove_predAbove_predAbove (i p : Fin n.succ.succ) (hip : i ≠ p) :
-     i.succAbove ((Fin.predAbove 0 i).predAbove p) = p := by
-  simp [Fin.succAbove, Fin.predAbove, Fin.lt_def]
-  split <;> split <;> simp   <;> rw [Fin.ext_iff] <;> simp
-  intro h
-  all_goals
-    rename_i h1 h2
-    simp at h1 h2
-    omega
+lemma markEmbeddingIndexValue_apply_symm_on_not_mem {n : ℕ} (f : Fin n.succ ↪ X)
+    (T : RealLorentzTensor d X) (i : IndexValue d (markEmbedding f T).color) (x : X)
+    (hx : ¬ x ∈ (Finset.image f Finset.univ)) : (markEmbeddingIndexValue f T).symm i x =
+    (colorsIndexCast ((congrFun ((Equiv.comp_symm_eq
+      (markEmbeddingSet f) ((markEmbedding f) T).color T.color).mp rfl) x).trans
+      ((congrArg ((markEmbedding f) T).color (markEmbeddingSet_on_not_mem f x hx))))).symm
+     (i (Sum.inl ⟨x, by simpa using hx⟩)) := by
+  rw [markEmbeddingIndexValue, indexValueIso_symm_apply']
+  rw [markEmbeddingSet_on_not_mem_indexValue_apply f T i x hx]
+  simp only [Nat.succ_eq_add_one, Function.comp_apply, markEmbedding_apply_color, colorsIndexCast,
+    Equiv.cast_symm, id_eq, eq_mp_eq_cast, eq_mpr_eq_cast, Equiv.cast_apply, cast_cast, cast_eq,
+    Equiv.cast_refl, Equiv.refl_symm]
+  rfl
 
+/-- Given an equivalence of types, an embedding `f` to an embedding `g`, the equivalence
+  taking the complement of the image of `f` to the complement of the image of `g`. -/
 @[simps!]
-def equivDropPoint  (e : Fin n.succ ≃ Fin m.succ) {i : Fin n.succ} {j : Fin m.succ} (he : e i = j) :
-    Fin n ≃ Fin m :=
-  (notInImage (oneEmbed i)).trans <|
-  (Equiv.subtypeEquivOfSubtype' e).trans  <|
-  (Equiv.subtypeEquivRight (fun x => by simp [oneEmbed, Equiv.symm_apply_eq, he])).trans <|
-  (notInImage (oneEmbed j)).symm
+def equivEmbedCompl (e : X ≃ Y) {f : Fin n ↪ X} {g : Fin n ↪ Y} (he : f.trans e = g) :
+    {x // x ∈ (Finset.image f Finset.univ)ᶜ} ≃ {y // y ∈ (Finset.image g Finset.univ)ᶜ} :=
+  (Equiv.subtypeEquivOfSubtype' e).trans <|
+  (Equiv.subtypeEquivRight (fun x => by simp [← he, Equiv.eq_symm_apply]))
 
-
-lemma markSelectedIndex_mapIso (f : X ≃ Y) (e : Fin n.succ.succ ≃ Fin m.succ.succ) (i : Fin n.succ.succ)
-    (j : Fin m.succ.succ) (he : e i = j) (T : Marked d X n.succ.succ) :
-    mapIso d (Equiv.sumCongr (Equiv.sumCongr f (equivDropPoint e he)) (Equiv.refl (Fin 1)))
-    (markSelectedIndex i T) = markSelectedIndex j (mapIso d (Equiv.sumCongr f e) T) := by
-  rw [markSelectedIndex, markSelectedIndex]
+lemma markEmbedding_mapIso_right (e : X ≃ Y) (f : Fin n ↪ X) (g : Fin n ↪ Y) (he : f.trans e = g)
+    (T : RealLorentzTensor d X) : markEmbedding g (mapIso d e T) =
+    mapIso d (Equiv.sumCongr (equivEmbedCompl e he) (Equiv.refl (Fin n))) (markEmbedding f T) := by
+  rw [markEmbedding, markEmbedding]
   erw [← Equiv.trans_apply, ← Equiv.trans_apply]
   rw [mapIso_trans, mapIso_trans]
   apply congrFun
-  apply congrArg
-  apply congrArg
-  apply Equiv.ext
-  intro x
-  match x with
-  | Sum.inl x => rfl
-  | Sum.inr x =>
-    simp only [Nat.succ_eq_add_one, Equiv.trans_apply, Equiv.coe_refl,
-       Fin.isValue]
-    change  ((f.sumCongr (equivDropPoint e he)).sumCongr (Equiv.refl (Fin 1)))
-      ((Equiv.sumAssoc X (Fin n.succ) (Fin 1)).symm (Sum.inr ((splitMarkedIndicesOne i) x)))  =
-      (Equiv.sumAssoc Y (Fin m.succ) (Fin 1)).symm (Sum.inr ((splitMarkedIndicesOne j) (e x)))
-    by_cases h : x = i
-    subst h
-    rw [he]
-    rw [splitMarkedIndicesOne_self, splitMarkedIndicesOne_self]
-    simp
+  repeat apply congrArg
+  refine Equiv.ext (fun x => ?_)
+  simp only [Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_refl]
+  by_cases hx : x ∈ Finset.image f Finset.univ
+  · rw [markEmbeddingSet_on_mem f x hx, markEmbeddingSet_on_mem g (e x) (by simpa [← he] using hx)]
     subst he
-    rw [splitMarkedIndicesOne_not_self (fun a => h a.symm), splitMarkedIndicesOne_not_self]
-    simp [equivDropPoint]
-    rw [Equiv.symm_apply_eq]
-    change _ =
-      (notInImage (oneEmbed (e i))).toFun ((Fin.predAbove 0 (e i)).predAbove (e x))
-    rw [notInImage_oneEmbed]
-    simp
-    apply Subtype.ext
-    simp
-    change (e.subtypeEquivOfSubtype'
-      ((notInImage (oneEmbed i)).toFun ((Fin.predAbove 0 i).predAbove x))).1 = _
-    rw [notInImage_oneEmbed]
-    rw [Equiv.subtypeEquivOfSubtype', Equiv.subtypeEquivOfSubtype]
-    simp
-    rw [succAbove_predAbove_predAbove, succAbove_predAbove_predAbove]
-    exact e.apply_eq_iff_eq.mp.mt (fun a => h a.symm)
-    exact fun a => h a.symm
-    exact e.apply_eq_iff_eq.mp.mt (fun a => h a.symm)
+    simp only [Sum.map_inr, id_eq, Sum.inr.injEq, Equiv.symm_apply_eq,
+      Function.Embedding.toEquivRange_apply, Function.Embedding.trans_apply, Equiv.coe_toEmbedding,
+      Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq]
+    change x = f.toEquivRange _
+    rw [Equiv.apply_symm_apply]
+  · rw [markEmbeddingSet_on_not_mem f x hx,
+      markEmbeddingSet_on_not_mem g (e x) (by simpa [← he] using hx)]
+    subst he
+    rfl
+
+lemma markEmbedding_mapIso_left {n m : ℕ} (e : Fin n ≃ Fin m) (f : Fin n ↪ X) (g : Fin m ↪ X)
+    (he : e.symm.toEmbedding.trans f = g) (T : RealLorentzTensor d X) :
+    markEmbedding g T = mapIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by
+     simpa [← he] using Equiv.forall_congr_left e)) e) (markEmbedding f T) := by
+  rw [markEmbedding, markEmbedding]
+  erw [← Equiv.trans_apply]
+  rw [mapIso_trans]
+  apply congrFun
+  repeat apply congrArg
+  refine Equiv.ext (fun x => ?_)
+  simp only [Equiv.trans_apply, Equiv.sumCongr_apply]
+  by_cases hx : x ∈ Finset.image f Finset.univ
+  · rw [markEmbeddingSet_on_mem f x hx, markEmbeddingSet_on_mem g x (by
+      simp [← he, hx]
+      obtain ⟨y, _, hy2⟩ := Finset.mem_image.mp hx
+      use e y
+      simpa using hy2)]
+    subst he
+    simp [Equiv.symm_apply_eq]
+    change x = f.toEquivRange _
+    rw [Equiv.apply_symm_apply]
+  · rw [markEmbeddingSet_on_not_mem f x hx, markEmbeddingSet_on_not_mem g x (by
+      simpa [← he, hx] using fun x => not_exists.mp (Finset.mem_image.mpr.mt hx) (e.symm x))]
+    subst he
+    rfl
+
+/-!
+
+## Marking a single element
+
+-/
+
+/-- An embedding from `Fin 1` into `X` given an element `x ∈ X`. -/
+@[simps!]
+def embedSingleton (x : X) : Fin 1 ↪ X :=
+  ⟨![x], fun x y => by fin_cases x; fin_cases y; simp⟩
+
+lemma embedSingleton_toEquivRange_symm (x : X) :
+    (embedSingleton x).toEquivRange.symm ⟨x, by simp⟩ = 0 := by
+  exact Fin.fin_one_eq_zero _
+
+/-- Equivalence, taking a tensor to a tensor with a single marked index. -/
+@[simps!]
+def markSingle (x : X) : RealLorentzTensor d X ≃ Marked d {x' // x' ≠ x} 1 :=
+  (markEmbedding (embedSingleton x)).trans
+  (mapIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by simp)) (Equiv.refl _)))
+
+/-- Equivalence between index values of a tensor and the corrsponding tensor with a single
+  marked index. -/
+@[simps!]
+def markSingleIndexValue (T : RealLorentzTensor d X) (x : X) :
+    IndexValue d T.color ≃ IndexValue d (markSingle x T).color :=
+  (markEmbeddingIndexValue (embedSingleton x) T).trans <|
+  indexValueIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by simp)) (Equiv.refl _))
+   (by funext x_1; simp)
+
+/-- Given an equivalence of types, taking `x` to `y` the corresponding equivalence of
+  subtypes of elements not equal to `x` and not equal to `y` respectively. -/
+@[simps!]
+def equivSingleCompl (e : X ≃ Y) {x : X} {y : Y} (he : e x = y) :
+    {x' // x' ≠ x} ≃ {y' // y' ≠ y} :=
+  (Equiv.subtypeEquivOfSubtype' e).trans <|
+  Equiv.subtypeEquivRight (fun a => by simp [Equiv.symm_apply_eq, he])
+
+lemma markSingle_mapIso (e : X ≃ Y) (x : X) (y : Y) (he : e x = y)
+    (T : RealLorentzTensor d X) : markSingle y (mapIso d e T) =
+    mapIso d (Equiv.sumCongr (equivSingleCompl e he) (Equiv.refl _)) (markSingle x T) := by
+  rw [markSingle, Equiv.trans_apply]
+  rw [markEmbedding_mapIso_right e (embedSingleton x) (embedSingleton y)
+    (Function.Embedding.ext_iff.mp (fun a => by simpa using he)), markSingle, markEmbedding]
+  erw [← Equiv.trans_apply, ← Equiv.trans_apply, ← Equiv.trans_apply]
+  rw [mapIso_trans, mapIso_trans, mapIso_trans, mapIso_trans]
+  apply congrFun
+  repeat apply congrArg
+  refine Equiv.ext fun x => ?_
+  simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.sumCongr_trans,
+    Equiv.trans_refl, Equiv.trans_apply, Equiv.sumCongr_apply, Equiv.coe_trans, Equiv.coe_refl,
+    Sum.map_map, CompTriple.comp_eq]
+  subst he
+  rfl
+
+/-!
+
+## Marking two elements
+
+-/
+
+/-- An embedding from `Fin 2` given two inequivalent elements. -/
+@[simps!]
+def embedDoubleton (x y : X) (h : x ≠ y) : Fin 2 ↪ X :=
+  ⟨![x, y], fun a b => by
+    fin_cases a <;> fin_cases b <;> simp [h]
+    exact h.symm⟩
+
+end markingElements
 
 end Marked
 
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
index 60369d5..acd45d4 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
@@ -50,12 +50,11 @@ lemma toReal_mapIso (d : ℕ) {X Y : Type} (h : IsEmpty X) (f : X ≃ Y) :
     (mapIso d f).trans (toReal d (Equiv.isEmpty f.symm)) = toReal d h := by
   apply Equiv.ext
   intro x
-  simp
+  simp only [Equiv.trans_apply, toReal_apply, mapIso_apply_color, mapIso_apply_coord]
   apply congrArg
   funext x
   exact IsEmpty.elim h x
 
-
 /-!
 
 # Tensors from reals, vectors and matrices
@@ -285,8 +284,9 @@ open Matrix
 
 /-- The action of the Lorentz group on `ofReal v` is trivial. -/
 @[simp]
-lemma lorentzAction_toReal (h : IsEmpty X) (r : ℝ) : Λ • (toReal d h).symm r = (toReal d h).symm r :=
-  lorentzAction_on_isEmpty Λ  ((toReal d h).symm r)
+lemma lorentzAction_toReal (h : IsEmpty X) (r : ℝ) :
+    Λ • (toReal d h).symm r = (toReal d h).symm r :=
+  lorentzAction_on_isEmpty Λ ((toReal d h).symm r)
 
 /-- The action of the Lorentz group on `ofVecUp v` is by vector multiplication. -/
 @[simp]
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
index 8e70920..31c37f5 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
@@ -15,7 +15,6 @@ marked index. This is equivalent to contracting two Lorentz tensors.
 We prove various results about this multiplication.
 
 -/
-/-! TODO: Generalize to contracting any marked index of a marked tensor. -/
 /-! TODO: Set up a good notation for the multiplication. -/
 
 namespace RealLorentzTensor
@@ -38,6 +37,31 @@ def mul {X Y : Type} (T : Marked d X 1) (S : Marked d Y 1)
     S.coord (splitIndexValue.symm ((indexValueSumEquiv i).2,
       oneMarkedIndexValue $ colorsIndexDualCast h x))
 
+/-- The index value appearing in the multiplication of Marked tensors on the left. -/
+def mulFstArg {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
+    (i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
+    (x : ColorsIndex d (T.color (markedPoint X 0))) : IndexValue d T.color :=
+  splitIndexValue.symm ((indexValueSumEquiv i).1, oneMarkedIndexValue x)
+
+lemma mulFstArg_inr {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
+    (i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
+    (x : ColorsIndex d (T.color (markedPoint X 0))) :
+    mulFstArg i x (Sum.inr 0) = x := by
+  rfl
+
+lemma mulFstArg_inl {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
+    (i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
+    (x : ColorsIndex d (T.color (markedPoint X 0))) (c : X):
+    mulFstArg i x (Sum.inl c) = i (Sum.inl c) := by
+  rfl
+
+/-- The index value appearing in the multiplication of Marked tensors on the right. -/
+def mulSndArg {X Y : Type} {T : Marked d X 1} {S : Marked d Y 1}
+    (i : IndexValue d (Sum.elim T.unmarkedColor S.unmarkedColor))
+    (x : ColorsIndex d (T.color (markedPoint X 0))) (h : T.markedColor 0 = τ (S.markedColor 0)) :
+    IndexValue d S.color :=
+  splitIndexValue.symm ((indexValueSumEquiv i).2, oneMarkedIndexValue $ colorsIndexDualCast h x)
+
 /-!
 
 ## Expressions for multiplication
@@ -237,79 +261,233 @@ lemma mul_lorentzAction (T : Marked d X 1) (S : Marked d Y 1)
 
 -/
 
-variable {n m : ℕ}
-
-def mulSSetEquiv : (X ⊕ Fin n) ⊕ Y ⊕ Fin m ≃ (X ⊕ Y) ⊕ (Fin (n + m)) :=
-  (Equiv.sumAssoc _ _ _).trans <|
-  (Equiv.sumCongr (Equiv.refl _ ) (Equiv.sumAssoc _ _ _).symm).trans <|
-  (Equiv.sumCongr (Equiv.refl _ ) (Equiv.sumCongr (Equiv.sumComm _ _) (Equiv.refl _)).symm).trans <|
-  (Equiv.sumAssoc _ _ _).symm.trans <|
-  (Equiv.sumCongr (Equiv.sumAssoc _ _ _) (Equiv.refl _ )).symm.trans <|
-  (Equiv.sumAssoc _ _ _).trans <|
-  Equiv.sumCongr (Equiv.refl _) finSumFinEquiv
+variable {n m : ℕ} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
+  {X' Y' Z : Type} [Fintype X'] [DecidableEq X'] [Fintype Y'] [DecidableEq Y']
+  [Fintype Z] [DecidableEq Z]
 
+/-- The multiplication of two real Lorentz Tensors along provided indices. -/
 @[simps!]
-def mulS (T : Marked d X n.succ) (S : Marked d Y m.succ) (i : Fin n.succ) (j : Fin m.succ)
-    (h : T.markedColor i = τ (S.markedColor j)) : Marked d (X ⊕ Y) (n + m) :=
-  mapIso d mulSSetEquiv (mul (markSelectedIndex i T) (markSelectedIndex j S) h)
+def mulS (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (x : X) (y : Y)
+    (h : T.color x = τ (S.color y)) : RealLorentzTensor d ({x' // x' ≠ x} ⊕ {y' // y' ≠ y}) :=
+  mul (markSingle x T) (markSingle y S) h
 
+/-- The first index value appearing in the multiplication of two Lorentz tensors. -/
+def mulSFstArg {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
+    (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
+    (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))) :
+    IndexValue d T.color := (markSingleIndexValue T x).symm (mulFstArg i a)
 
-/-- Given a marked index of `T` and returns a marked index of `mulS T S _ _ _`. -/
-def mulSInl {n m : ℕ} {i j : Fin n.succ.succ} (h : j ≠ i) : Fin (n.succ + m) :=
-  finSumFinEquiv <|
-  Sum.inl <|
-  (notInImage (oneEmbed i)).symm <|
-  ⟨j, by simp [oneEmbed, h]⟩
-
-/-- Given a marked index of `S` and returns a marked index of `mulS S T _ _ _`. -/
-def mulSInr {n m : ℕ} {i j : Fin m.succ.succ} (h : j ≠ i) : Fin (n + m.succ) :=
-  finSumFinEquiv <|
-  Sum.inr <|
-  (notInImage (oneEmbed i)).symm <|
-  ⟨j, by simp [oneEmbed, h]⟩
-
-lemma mulSInl_mulSSetEquiv {n m : ℕ} {i j : Fin n.succ.succ} (h : j ≠ i) :
-    (@mulSSetEquiv X Y n.succ m).symm (Sum.inr (mulSInl h)) =
-    Sum.inl (Sum.inr ((notInImage (oneEmbed i)).symm  ⟨j, by simp [oneEmbed, h]⟩)) := by
-  rw [Equiv.symm_apply_eq]
+lemma mulSFstArg_ext {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
+    {i j : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)}
+    {a b : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))}
+    (hij : i = j) (hab : a = b) : mulSFstArg i a = mulSFstArg j b := by
+  subst hij; subst hab
   rfl
 
-lemma mulSInr_mulSSetEquiv {n m : ℕ} {i j : Fin m.succ.succ} (h : j ≠ i) :
-    (@mulSSetEquiv X Y n m.succ).symm (Sum.inr (mulSInr h)) =
-    Sum.inr (Sum.inr ((notInImage (oneEmbed i)).symm  ⟨j, by simp [oneEmbed, h]⟩)) := by
-  rw [Equiv.symm_apply_eq]
+lemma mulSFstArg_on_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
+    (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
+    (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))) :
+    mulSFstArg i a x = a := by
+  rw [mulSFstArg, markSingleIndexValue]
+  simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
+     Sum.map_inr, id_eq]
+  erw [markEmbeddingIndexValue_apply_symm_on_mem]
+  swap
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Finset.univ_unique, Fin.default_eq_zero,
+    Fin.isValue, Finset.image_singleton, embedSingleton_apply, Finset.mem_singleton]
+  rw [indexValueIso_symm_apply']
+  erw [Equiv.symm_apply_eq, Equiv.symm_apply_eq]
+  simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast]
+  symm
+  apply cast_eq_iff_heq.mpr
+  rw [embedSingleton_toEquivRange_symm]
   rfl
-/-
-@[simp]
-lemma mulSInl_color {n m : ℕ}
-    (T : Marked d X n.succ.succ) (S : Marked d Y m.succ) (a b : Fin n.succ.succ) (c : Fin m.succ)
-    (h : T.markedColor a = τ (S.markedColor c)) (hab : b ≠ a):
-    (mulS T S a c h).markedColor (mulSInl hab) = T.markedColor b := by
-  rw [markedColor]
-  simp [mulS_color]
-  rw [mulSInl_mulSSetEquiv]
-  simp  [unmarkedColor, markSelectedIndex, Nat.succ_eq_add_one, Fintype.univ_ofSubsingleton,
-    Fin.zero_eta, Fin.isValue, notInImage, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv,
-    Sum.elim_inl, Function.comp_apply, mapIso_apply_color, Equiv.symm_trans_apply,
-    Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.symm_symm, Equiv.sumAssoc_apply_inl_inr,
-    Equiv.sumCongr_apply, Equiv.coe_refl, Sum.map_inr, splitMarkedIndicesOne_symm_apply,
-    Sum.map_inl, OrderIso.symm_symm, OrderIso.apply_symm_apply, Equiv.coe_fn_symm_mk, Sum.swap_inl,
-    Equiv.Set.sumCompl_apply_inr, markedColor]
 
-@[simp]
-lemma mulSInr_color {n m : ℕ}
-    (T : Marked d X n.succ) (S : Marked d Y m.succ.succ) (c : Fin n.succ) (a b : Fin m.succ.succ)
-    (h : T.markedColor c = τ (S.markedColor a)) (hab : b ≠ a) :
-    (mulS T S c a h).markedColor (mulSInr hab) = S.markedColor b := by
-  rw [markedColor]
-  simp [mulS_color]
-  rw [mulSInr_mulSSetEquiv]
-  simp only [unmarkedColor, markSelectedIndex, Nat.succ_eq_add_one, Fintype.univ_ofSubsingleton,
-    Fin.zero_eta, Fin.isValue, notInImage, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv,
-    Sum.elim_inr, Function.comp_apply, mapIso_apply_color, Equiv.symm_trans_apply,
-    Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.symm_symm, Equiv.sumAssoc_apply_inl_inr,
-    Equiv.sumCongr_apply, Equiv.coe_refl, Sum.map_inr, splitMarkedIndicesOne_symm_apply,
-    Sum.map_inl, OrderIso.symm_symm, OrderIso.apply_symm_apply, Equiv.coe_fn_symm_mk, Sum.swap_inl,
-    Equiv.Set.sumCompl_apply_inr, markedColor]
--/
+lemma mulSFstArg_on_not_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
+    (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
+    (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
+    (c : X) (hc : c ≠ x) : mulSFstArg i a c = i (Sum.inl ⟨c, hc⟩) := by
+  rw [mulSFstArg, markSingleIndexValue]
+  simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
+     Sum.map_inr, id_eq]
+  erw [markEmbeddingIndexValue_apply_symm_on_not_mem]
+  swap
+  simpa using hc
+  rfl
+
+/-- The second index value appearing in the multiplication of two Lorentz tensors. -/
+def mulSSndArg {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
+    (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
+    (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
+    (h : T.color x = τ (S.color y)) : IndexValue d S.color :=
+  (markSingleIndexValue S y).symm (mulSndArg i a h)
+
+lemma mulSSndArg_on_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
+    (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
+    (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
+    (h : T.color x = τ (S.color y)) : mulSSndArg i a h y = colorsIndexDualCast h a := by
+  rw [mulSSndArg, markSingleIndexValue]
+  simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
+     Sum.map_inr, id_eq]
+  erw [markEmbeddingIndexValue_apply_symm_on_mem]
+  swap
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Finset.univ_unique, Fin.default_eq_zero,
+    Fin.isValue, Finset.image_singleton, embedSingleton_apply, Finset.mem_singleton]
+  rw [indexValueIso_symm_apply']
+  erw [Equiv.symm_apply_eq, Equiv.symm_apply_eq]
+  simp only [Function.comp_apply, colorsIndexCast, Equiv.cast_symm, Equiv.cast_apply, cast_cast]
+  symm
+  apply cast_eq_iff_heq.mpr
+  rw [embedSingleton_toEquivRange_symm]
+  rfl
+
+lemma mulSSndArg_on_not_mem {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
+    (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor))
+    (a : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0)))
+    (h : T.color x = τ (S.color y)) (c : Y) (hc : c ≠ y) :
+    mulSSndArg i a h c = i (Sum.inr ⟨c, hc⟩) := by
+  rw [mulSSndArg, markSingleIndexValue]
+  simp only [ne_eq, Fintype.univ_ofSubsingleton, Fin.zero_eta, Fin.isValue, Equiv.symm_trans_apply,
+     Sum.map_inr, id_eq]
+  erw [markEmbeddingIndexValue_apply_symm_on_not_mem]
+  swap
+  simpa using hc
+  rfl
+
+lemma mulSSndArg_ext {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y} {x : X} {y : Y}
+    {i j : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)}
+    {a b : ColorsIndex d ((markSingle x T).color (markedPoint {x' // x' ≠ x} 0))}
+    (h : T.color x = τ (S.color y)) (hij : i = j) (hab : a = b) :
+    mulSSndArg i a h = mulSSndArg j b h := by
+  subst hij
+  subst hab
+  rfl
+
+lemma mulS_coord_arg (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (x : X) (y : Y)
+    (h : T.color x = τ (S.color y))
+    (i : IndexValue d (Sum.elim (markSingle x T).unmarkedColor (markSingle y S).unmarkedColor)) :
+  (mulS T S x y h).coord i = ∑ a, T.coord (mulSFstArg i a) * S.coord (mulSSndArg i a h) := by
+  rfl
+
+lemma mulS_mapIso (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
+    (eX : X ≃ X') (eY : Y ≃ Y') (x : X) (y : Y) (x' : X') (y' : Y') (hx : eX x = x')
+    (hy : eY y = y') (h : T.color x = τ (S.color y)) :
+    mulS (mapIso d eX T) (mapIso d eY S) x' y' (by subst hx hy; simpa using h) =
+    mapIso d (Equiv.sumCongr (equivSingleCompl eX hx) (equivSingleCompl eY hy))
+      (mulS T S x y h) := by
+  rw [mulS, mulS, mul_mapIso]
+  congr 1 <;> rw [markSingle_mapIso]
+
+lemma mulS_lorentzAction (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
+    (x : X) (y : Y) (h : T.color x = τ (S.color y)) (Λ : LorentzGroup d) :
+    mulS (Λ • T) (Λ • S) x y h = Λ • mulS T S x y h := by
+  rw [mulS, mulS, ← mul_lorentzAction]
+  congr 1
+  all_goals
+    rw [markSingle, markEmbedding, Equiv.trans_apply]
+    erw [lorentzAction_mapIso, lorentzAction_mapIso]
+    rfl
+
+lemma mulS_symm (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
+    (x : X) (y : Y) (h : T.color x = τ (S.color y)) :
+    mapIso d (Equiv.sumComm _ _) (mulS T S x y h) = mulS S T y x (color_eq_dual_symm h) := by
+  rw [mulS, mulS, mul_symm]
+
+/-- An equivalence of types assocaited with multipying two consecutive indices,
+with the second index appearing on the left. -/
+def mulSSplitLeft {y y' : Y} (hy : y ≠ y') (z : Z) :
+    {yz // yz ≠ (Sum.inl ⟨y, hy⟩ : {y'' // y'' ≠ y'} ⊕ {z' // z' ≠ z})} ≃
+    {y'' // y'' ≠ y' ∧ y'' ≠ y} ⊕ {z' // z' ≠ z} :=
+  Equiv.subtypeSum.trans <|
+  Equiv.sumCongr (
+      (Equiv.subtypeEquivRight (fun a => by
+        obtain ⟨a, p⟩ := a; simp only [ne_eq, Sum.inl.injEq, Subtype.mk.injEq])).trans
+      (Equiv.subtypeSubtypeEquivSubtypeInter _ _)) <|
+  Equiv.subtypeUnivEquiv (fun a => by simp)
+
+/-- An equivalence of types assocaited with multipying two consecutive indices with the
+second index appearing on the right. -/
+def mulSSplitRight {y y' : Y} (hy : y ≠ y') (z : Z) :
+    {yz // yz ≠ (Sum.inr ⟨y', hy.symm⟩ : {z' // z' ≠ z} ⊕ {y'' // y'' ≠ y})} ≃
+    {z' // z' ≠ z} ⊕ {y'' // y'' ≠ y' ∧ y'' ≠ y} :=
+   Equiv.subtypeSum.trans <|
+  Equiv.sumCongr (Equiv.subtypeUnivEquiv (fun a => by simp)) <|
+  (Equiv.subtypeEquivRight (fun a => by
+    obtain ⟨a, p⟩ := a; simp only [ne_eq, Sum.inr.injEq, Subtype.mk.injEq])).trans <|
+  ((Equiv.subtypeSubtypeEquivSubtypeInter _ _).trans
+    (Equiv.subtypeEquivRight (fun y'' => And.comm)))
+
+/-- An equivalence of types associated with the associativity property of multiplication. -/
+def mulSAssocIso (x : X) {y y' : Y} (hy : y ≠ y') (z : Z) :
+    {x' // x' ≠ x} ⊕ {yz // yz ≠ (Sum.inl ⟨y, hy⟩ : {y'' // y'' ≠ y'} ⊕ {z' // z' ≠ z})}
+    ≃ {xy // xy ≠ (Sum.inr ⟨y', hy.symm⟩ : {x' // x' ≠ x} ⊕ {y'' // y'' ≠ y})} ⊕ {z' // z' ≠ z} :=
+  (Equiv.sumCongr (Equiv.refl _) (mulSSplitLeft hy z)).trans <|
+  (Equiv.sumAssoc _ _ _).symm.trans <|
+  (Equiv.sumCongr (mulSSplitRight hy x).symm (Equiv.refl _))
+
+lemma mulS_assoc_color {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y}
+    {U : RealLorentzTensor d Z} {x : X} {y y' : Y} (hy : y ≠ y') {z : Z}
+    (h : T.color x = τ (S.color y))
+    (h' : S.color y' = τ (U.color z)) : (mulS (mulS T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h').color
+    = (mapIso d (mulSAssocIso x hy z) (mulS T (mulS S U y' z h') x (Sum.inl ⟨y, hy⟩) h)).color := by
+  funext a
+  match a with
+  | .inl ⟨.inl _, _⟩ => rfl
+  | .inl ⟨.inr _, _⟩ => rfl
+  | .inr _ => rfl
+
+/-- An equivalence of index values associated with the associativity property of multiplication. -/
+def mulSAssocIndexValue {T : RealLorentzTensor d X} {S : RealLorentzTensor d Y}
+    {U : RealLorentzTensor d Z} {x : X} {y y' : Y} (hy : y ≠ y') {z : Z}
+    (h : T.color x = τ (S.color y)) (h' : S.color y' = τ (U.color z)) :
+    IndexValue d ((T.mulS S x y h).mulS U (Sum.inr ⟨y', hy.symm⟩) z h').color ≃
+    IndexValue d (T.mulS (S.mulS U y' z h') x (Sum.inl ⟨y, hy⟩) h).color :=
+  indexValueIso d (mulSAssocIso x hy z).symm (mulS_assoc_color hy h h')
+
+/-- Multiplication of indices is associative, up to a `mapIso` equivalence. -/
+lemma mulS_assoc (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (U : RealLorentzTensor d Z)
+    (x : X) (y y' : Y) (hy : y ≠ y') (z : Z) (h : T.color x = τ (S.color y))
+    (h' : S.color y' = τ (U.color z)) : mulS (mulS T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h' =
+    mapIso d (mulSAssocIso x hy z) (mulS T (mulS S U y' z h') x (Sum.inl ⟨y, hy⟩) h) := by
+  apply ext ?_ ?_
+  · funext a
+    match a with
+    | .inl ⟨.inl _, _⟩ => rfl
+    | .inl ⟨.inr _, _⟩ => rfl
+    | .inr _ => rfl
+  funext i
+  trans ∑ a, (∑ b, T.coord (mulSFstArg (mulSFstArg i a) b) *
+    S.coord (mulSSndArg (mulSFstArg i a) b h)) * U.coord (mulSSndArg i a h')
+  rfl
+  trans ∑ a, T.coord (mulSFstArg (mulSAssocIndexValue hy h h' i) a) *
+    (∑ b, S.coord (mulSFstArg (mulSSndArg (mulSAssocIndexValue hy h h' i) a h) b) *
+    U.coord (mulSSndArg (mulSSndArg (mulSAssocIndexValue hy h h' i) a h) b h'))
+  swap
+  rw [mapIso_apply_coord, mulS_coord_arg, indexValueIso_symm]
+  rfl
+  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 _ => ?_)
+  rw [mul_assoc]
+  refine Mathlib.Tactic.Ring.mul_congr rfl (Mathlib.Tactic.Ring.mul_congr ?_ rfl rfl) rfl
+  apply congrArg
+  funext c
+  by_cases hcy : c = y
+  · subst hcy
+    rw [mulSSndArg_on_mem, mulSFstArg_on_not_mem, mulSSndArg_on_mem]
+    rfl
+  · by_cases hcy' : c = y'
+    · subst hcy'
+      rw [mulSFstArg_on_mem, mulSSndArg_on_not_mem, mulSFstArg_on_mem]
+    · 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]
+      erw [Equiv.refl_apply]
+      rfl
+      exact hcy'
+      simpa using hcy
+
 end RealLorentzTensor

From 87f896550cbf3bf7e48330db26a3535885744330 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 19 Jul 2024 15:58:20 -0400
Subject: [PATCH 3/6] refactor: Lint spelling

---
 .../SpaceTime/LorentzTensor/Real/Basic.lean    | 18 +++++++++---------
 .../LorentzTensor/Real/Multiplication.lean     |  6 +++---
 2 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index aeddde7..36d49e7 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -27,7 +27,7 @@ This will relation should be made explicit in the future.
 /-! TODO: Generalize to maps into Lorentz tensors. -/
 
 /-- The possible `colors` of an index for a RealLorentzTensor.
- There are two possiblities, `up` and `down`. -/
+ There are two possibilities, `up` and `down`. -/
 inductive RealLorentzTensor.Colors where
   | up : RealLorentzTensor.Colors
   | down : RealLorentzTensor.Colors
@@ -88,7 +88,7 @@ lemma color_eq_dual_symm {μ ν : Colors} (h : μ = τ ν) : ν = τ μ :=
 /-- The color associated with an element of `x ∈ X` for a tensor `T`. -/
 def ch {X : Type} (x : X) (T : RealLorentzTensor d X) : Colors := T.color x
 
-/-- An equivalence of `ColorsIndex` types given an equality of a colors. -/
+/-- An equivalence of `ColorsIndex` types given an equality of colors. -/
 def colorsIndexCast {d : ℕ} {μ₁ μ₂ : RealLorentzTensor.Colors} (h : μ₁ = μ₂) :
     ColorsIndex d μ₁ ≃ ColorsIndex d μ₂ :=
   Equiv.cast (congrArg (ColorsIndex d) h)
@@ -281,7 +281,7 @@ lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl
 ## Sums
 
 -/
-/-- An equivalence splitting elements of `IndexValue d (Sum.elim TX TY)` into two components. -/
+/-- An equivalence that splits elements of `IndexValue d (Sum.elim TX TY)` into two components. -/
 def indexValueSumEquiv {X Y : Type} {TX : X → Colors} {TY : Y → Colors} :
     IndexValue d (Sum.elim TX TY) ≃ IndexValue d TX × IndexValue d TY where
   toFun i := (fun x => i (Sum.inl x), fun x => i (Sum.inr x))
@@ -366,7 +366,7 @@ lemma splitIndexValue_sum {T : Marked d X n} [Fintype X] [DecidableEq X]
     ∑ i, P (splitIndexValue i) = ∑ j, ∑ k, P (j, k) := by
   rw [Equiv.sum_comp splitIndexValue, Fintype.sum_prod_type]
 
-/-- Contruction of marked index values for the case of 1 marked index. -/
+/-- Construction of marked index values for the case of 1 marked index. -/
 def oneMarkedIndexValue {T : Marked d X 1} :
     ColorsIndex d (T.color (markedPoint X 0)) ≃ T.MarkedIndexValue where
   toFun x := fun i => match i with
@@ -378,7 +378,7 @@ def oneMarkedIndexValue {T : Marked d X 1} :
     fin_cases x
     rfl
 
-/-- Contruction of marked index values for the case of 2 marked index. -/
+/-- Construction of marked index values for the case of 2 marked index. -/
 def twoMarkedIndexValue (T : Marked d X 2) (x : ColorsIndex d (T.color (markedPoint X 0)))
     (y : ColorsIndex d <| T.color <| markedPoint X 1) :
     T.MarkedIndexValue := fun i =>
@@ -392,7 +392,7 @@ def unmarkFirstSet (X : Type) (n : ℕ) : (X ⊕ Fin n.succ) ≃ (X ⊕ Fin 1) 
     (((Fin.castOrderIso (Nat.succ_eq_one_add n)).toEquiv.trans finSumFinEquiv.symm)))
   (Equiv.sumAssoc _ _ _).symm
 
-/-- Unmark the first marked index of a marked thensor. -/
+/-- Unmark the first marked index of a marked tensor. -/
 def unmarkFirst {X : Type} : Marked d X n.succ ≃ Marked d (X ⊕ Fin 1) n :=
   mapIso d (unmarkFirstSet X n)
 
@@ -431,7 +431,7 @@ lemma markEmbeddingSet_on_not_mem {n : ℕ} (f : Fin n ↪ X) (x : X)
   rfl
   simpa using hx
 
-/-- Marks the indicies of tensor in the image of an embedding. -/
+/-- Marks the indices of tensor in the image of an embedding. -/
 @[simps!]
 def markEmbedding {n : ℕ} (f : Fin n ↪ X) :
     RealLorentzTensor d X ≃ Marked d {x // x ∈ (Finset.image f Finset.univ)ᶜ} n :=
@@ -458,7 +458,7 @@ lemma markEmbeddingSet_on_not_mem_indexValue_apply {n : ℕ}
   rw [markEmbeddingSet_on_not_mem f x hx]
 
 /-- An equivalence between the IndexValues for a tensor `T` and the corresponding
-  tensor with indicies maked by an embedding. -/
+  tensor with indices maked by an embedding. -/
 @[simps!]
 def markEmbeddingIndexValue {n : ℕ} (f : Fin n ↪ X) (T : RealLorentzTensor d X) :
     IndexValue d T.color ≃ IndexValue d (markEmbedding f T).color :=
@@ -568,7 +568,7 @@ def markSingle (x : X) : RealLorentzTensor d X ≃ Marked d {x' // x' ≠ x} 1 :
   (markEmbedding (embedSingleton x)).trans
   (mapIso d (Equiv.sumCongr (Equiv.subtypeEquivRight (fun x => by simp)) (Equiv.refl _)))
 
-/-- Equivalence between index values of a tensor and the corrsponding tensor with a single
+/-- Equivalence between index values of a tensor and the corresponding tensor with a single
   marked index. -/
 @[simps!]
 def markSingleIndexValue (T : RealLorentzTensor d X) (x : X) :
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
index 31c37f5..fe2df90 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
@@ -265,7 +265,7 @@ variable {n m : ℕ} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
   {X' Y' Z : Type} [Fintype X'] [DecidableEq X'] [Fintype Y'] [DecidableEq Y']
   [Fintype Z] [DecidableEq Z]
 
-/-- The multiplication of two real Lorentz Tensors along provided indices. -/
+/-- The multiplication of two real Lorentz Tensors along specified indices. -/
 @[simps!]
 def mulS (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (x : X) (y : Y)
     (h : T.color x = τ (S.color y)) : RealLorentzTensor d ({x' // x' ≠ x} ⊕ {y' // y' ≠ y}) :=
@@ -393,7 +393,7 @@ lemma mulS_symm (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y)
     mapIso d (Equiv.sumComm _ _) (mulS T S x y h) = mulS S T y x (color_eq_dual_symm h) := by
   rw [mulS, mulS, mul_symm]
 
-/-- An equivalence of types assocaited with multipying two consecutive indices,
+/-- An equivalence of types associated with multiplying two consecutive indices,
 with the second index appearing on the left. -/
 def mulSSplitLeft {y y' : Y} (hy : y ≠ y') (z : Z) :
     {yz // yz ≠ (Sum.inl ⟨y, hy⟩ : {y'' // y'' ≠ y'} ⊕ {z' // z' ≠ z})} ≃
@@ -405,7 +405,7 @@ def mulSSplitLeft {y y' : Y} (hy : y ≠ y') (z : Z) :
       (Equiv.subtypeSubtypeEquivSubtypeInter _ _)) <|
   Equiv.subtypeUnivEquiv (fun a => by simp)
 
-/-- An equivalence of types assocaited with multipying two consecutive indices with the
+/-- An equivalence of types associated with multiplying two consecutive indices with the
 second index appearing on the right. -/
 def mulSSplitRight {y y' : Y} (hy : y ≠ y') (z : Z) :
     {yz // yz ≠ (Sum.inr ⟨y', hy.symm⟩ : {z' // z' ≠ z} ⊕ {y'' // y'' ≠ y})} ≃

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

---
 .../LorentzTensor/Real/Multiplication.lean    | 44 ++++++++-----------
 1 file changed, 18 insertions(+), 26 deletions(-)

diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
index fe2df90..d3f0cc0 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Multiplication.lean
@@ -141,7 +141,6 @@ lemma mul_mapIso {X Y Z : Type} (T : Marked d X 1) (S : Marked d Y 1) (f : X ≃
     rw [mapIso_apply_coord, mapIso_apply_coord]
     refine Mathlib.Tactic.Ring.mul_congr ?_ ?_ rfl
     · apply congrArg
-      simp only [IndexValue]
       exact (Equiv.symm_apply_eq splitIndexValue).mpr rfl
     · apply congrArg
       exact (Equiv.symm_apply_eq splitIndexValue).mpr rfl
@@ -212,40 +211,38 @@ lemma mul_unmarkedLorentzAction (T : Marked d X 1) (S : Marked d Y 1)
       T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))*
        toTensorRepMat Λ (indexValueSumEquiv i).2 k *
       S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
-  apply Finset.sum_congr rfl (fun x _ => ?_)
-  rw [Finset.sum_mul_sum ]
-  apply Finset.sum_congr rfl (fun j _ => ?_)
-  apply Finset.sum_congr rfl (fun k _ => ?_)
-  ring
+  · apply Finset.sum_congr rfl (fun x _ => ?_)
+    rw [Finset.sum_mul_sum ]
+    apply Finset.sum_congr rfl (fun j _ => ?_)
+    apply Finset.sum_congr rfl (fun k _ => ?_)
+    ring
   rw [Finset.sum_comm]
   trans ∑ j, ∑ k, ∑ x, (toTensorRepMat Λ (indexValueSumEquiv i).1 j *
       T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))*
        toTensorRepMat Λ (indexValueSumEquiv i).2 k *
       S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
-  apply Finset.sum_congr rfl (fun j _ => ?_)
-  rw [Finset.sum_comm]
+  · exact Finset.sum_congr rfl (fun j _ => Finset.sum_comm)
   trans ∑ j, ∑ k,
     ((toTensorRepMat Λ (indexValueSumEquiv i).1 j) * toTensorRepMat Λ (indexValueSumEquiv i).2 k)
     * ∑ x, (T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))
     * S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
-  apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
-  rw [Finset.mul_sum]
-  apply Finset.sum_congr rfl (fun x _ => ?_)
-  ring
+  · apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
+    rw [Finset.mul_sum]
+    apply Finset.sum_congr rfl (fun x _ => ?_)
+    ring
   trans ∑ j, ∑ k, toTensorRepMat Λ i (indexValueSumEquiv.symm (j, k)) *
     ∑ x, (T.coord (splitIndexValue.symm (j, oneMarkedIndexValue x)))
       * S.coord (splitIndexValue.symm (k, oneMarkedIndexValue $ colorsIndexDualCast h x))
   apply Finset.sum_congr rfl (fun j _ => Finset.sum_congr rfl (fun k _ => ?_))
-  rw [toTensorRepMat_of_indexValueSumEquiv']
-  congr
-  simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply, mul_color]
+  · rw [toTensorRepMat_of_indexValueSumEquiv']
+    congr
+    simp only [IndexValue, Finset.mem_univ, Prod.mk.eta, Equiv.symm_apply_apply, mul_color]
   trans ∑ p, toTensorRepMat Λ i p *
     ∑ x, (T.coord (splitIndexValue.symm ((indexValueSumEquiv p).1, oneMarkedIndexValue x)))
     * S.coord (splitIndexValue.symm ((indexValueSumEquiv p).2,
       oneMarkedIndexValue $ colorsIndexDualCast h x))
-  erw [← Equiv.sum_comp indexValueSumEquiv.symm]
-  rw [Fintype.sum_prod_type]
-  rfl
+  · erw [← Equiv.sum_comp indexValueSumEquiv.symm]
+    exact Eq.symm Fintype.sum_prod_type
   rfl
 
 /-- The Lorentz action commutes with multiplication. -/
@@ -403,7 +400,7 @@ def mulSSplitLeft {y y' : Y} (hy : y ≠ y') (z : Z) :
       (Equiv.subtypeEquivRight (fun a => by
         obtain ⟨a, p⟩ := a; simp only [ne_eq, Sum.inl.injEq, Subtype.mk.injEq])).trans
       (Equiv.subtypeSubtypeEquivSubtypeInter _ _)) <|
-  Equiv.subtypeUnivEquiv (fun a => by simp)
+  Equiv.subtypeUnivEquiv (fun a => Sum.inr_ne_inl)
 
 /-- An equivalence of types associated with multiplying two consecutive indices with the
 second index appearing on the right. -/
@@ -411,7 +408,7 @@ def mulSSplitRight {y y' : Y} (hy : y ≠ y') (z : Z) :
     {yz // yz ≠ (Sum.inr ⟨y', hy.symm⟩ : {z' // z' ≠ z} ⊕ {y'' // y'' ≠ y})} ≃
     {z' // z' ≠ z} ⊕ {y'' // y'' ≠ y' ∧ y'' ≠ y} :=
    Equiv.subtypeSum.trans <|
-  Equiv.sumCongr (Equiv.subtypeUnivEquiv (fun a => by simp)) <|
+  Equiv.sumCongr (Equiv.subtypeUnivEquiv (fun a => Sum.inl_ne_inr)) <|
   (Equiv.subtypeEquivRight (fun a => by
     obtain ⟨a, p⟩ := a; simp only [ne_eq, Sum.inr.injEq, Subtype.mk.injEq])).trans <|
   ((Equiv.subtypeSubtypeEquivSubtypeInter _ _).trans
@@ -449,12 +446,7 @@ lemma mulS_assoc (T : RealLorentzTensor d X) (S : RealLorentzTensor d Y) (U : Re
     (x : X) (y y' : Y) (hy : y ≠ y') (z : Z) (h : T.color x = τ (S.color y))
     (h' : S.color y' = τ (U.color z)) : mulS (mulS T S x y h) U (Sum.inr ⟨y', hy.symm⟩) z h' =
     mapIso d (mulSAssocIso x hy z) (mulS T (mulS S U y' z h') x (Sum.inl ⟨y, hy⟩) h) := by
-  apply ext ?_ ?_
-  · funext a
-    match a with
-    | .inl ⟨.inl _, _⟩ => rfl
-    | .inl ⟨.inr _, _⟩ => rfl
-    | .inr _ => rfl
+  apply ext (mulS_assoc_color _ _ _) ?_
   funext i
   trans ∑ a, (∑ b, T.coord (mulSFstArg (mulSFstArg i a) b) *
     S.coord (mulSSndArg (mulSFstArg i a) b h)) * U.coord (mulSSndArg i a h')

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 5/6] 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'

From b0f1ae79dbe3df721ea869047762f448bf1c9292 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 19 Jul 2024 16:19:58 -0400
Subject: [PATCH 6/6] refactor: add newline

---
 HepLean/SpaceTime/LorentzTensor/Real/Basic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index 36d49e7..23f52e7 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -281,6 +281,7 @@ lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl
 ## Sums
 
 -/
+
 /-- An equivalence that splits elements of `IndexValue d (Sum.elim TX TY)` into two components. -/
 def indexValueSumEquiv {X Y : Type} {TX : X → Colors} {TY : Y → Colors} :
     IndexValue d (Sum.elim TX TY) ≃ IndexValue d TX × IndexValue d TY where