diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
index de080d4..046bc5b 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
@@ -343,11 +343,20 @@ lemma getDual_neq_self (i : l.contrSubtype) : i ≠ l.getDual i := by
   indices. -/
 def HasNoContr : Prop := ∀ i, l.NoContr i
 
-lemma hasNoContr_is_empty (h : l.HasNoContr) : IsEmpty l.contrSubtype := by
+lemma contrSubtype_is_empty_of_hasNoContr (h : l.HasNoContr) : IsEmpty l.contrSubtype := by
   rw [_root_.isEmpty_iff]
   intro a
   exact h a.1 a.1 (fun _ => a.2 (h a.1)) rfl
 
+lemma hasNoContr_id_inj (h : l.HasNoContr) : Function.Injective l.idMap := fun i j => by
+  simpa using (h i j).mt
+
+lemma hasNoContr_color_eq_of_id_eq (h : l.HasNoContr) (i j : Fin l.length) :
+    l.idMap i = l.idMap j → l.colorMap i = l.colorMap j := by
+  intro h1
+  apply l.hasNoContr_id_inj h at h1
+  rw [h1]
+
 /-!
 
 ## The contracted index list
@@ -378,6 +387,34 @@ lemma contrIndexList_hasNoContr : HasNoContr l.contrIndexList := by
   simp only [Fin.coe_cast, ne_eq]
   exact Fin.val_ne_of_ne h
 
+/-- Contracting indices on a index list that has no contractions does nothing. -/
+@[simp]
+lemma contrIndexList_of_hasNoContr (h : HasNoContr l) : l.contrIndexList = l := by
+  simp only [contrIndexList, List.get_eq_getElem]
+  have hn : (@Finset.univ (Fin (List.length l)) (Fin.fintype (List.length l))).card =
+      (Finset.filter l.NoContr Finset.univ).card := by
+    rw [Finset.filter_true_of_mem (fun a _ => h a)]
+  have hx : (Finset.filter l.NoContr Finset.univ).card = (List.length l) := by
+    rw [← hn]
+    exact Finset.card_fin (List.length l)
+  apply List.ext_get
+  simpa [fromFinMap, noContrFinset] using hx
+  intro n h1 h2
+  simp only [noContrFinset, noContrSubtypeEquiv, OrderIso.toEquiv_symm, Equiv.symm_trans_apply,
+    RelIso.coe_fn_toEquiv, Equiv.subtypeEquivRight_symm_apply_coe, fromFinMap, List.get_eq_getElem,
+    OrderIso.symm_symm, Finset.coe_orderIsoOfFin_apply, List.getElem_map, Fin.getElem_list,
+    Fin.cast_mk]
+  simp only [Finset.filter_true_of_mem (fun a _ => h a)]
+  congr
+  rw [(Finset.orderEmbOfFin_unique' _
+    (fun x => Finset.mem_univ ((Fin.castOrderIso hx).toOrderEmbedding x))).symm]
+  rfl
+
+/-- Applying contrIndexlist is equivalent to applying it once. -/
+@[simp]
+lemma contrIndexList_contrIndexList : l.contrIndexList.contrIndexList = l.contrIndexList :=
+  l.contrIndexList.contrIndexList_of_hasNoContr (l.contrIndexList_hasNoContr)
+
 /-!
 
 ## Pairs of contracting indices
@@ -388,6 +425,11 @@ lemma contrIndexList_hasNoContr : HasNoContr l.contrIndexList := by
 def contrPairSet : Set (l.contrSubtype × l.contrSubtype) :=
   {p | p.1.1 < p.2.1 ∧ l.idMap p.1.1 = l.idMap p.2.1}
 
+instance : DecidablePred fun x => x ∈ l.contrPairSet := fun _ =>
+  And.decidable
+
+instance : Fintype l.contrPairSet := setFintype _
+
 lemma getDual_lt_self_mem_contrPairSet {i : l.contrSubtype}
     (h : (l.getDual i).1 < i.1) : (l.getDual i, i) ∈ l.contrPairSet :=
   And.intro h (l.getDual_id i).symm
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean
index 773378e..d81b26c 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexListColor.lean
@@ -43,7 +43,7 @@ instance : Coe (IndexListColor 𝓒) (IndexList 𝓒.Color) := ⟨fun x => x.val
 lemma indexListColorProp_of_hasNoContr {s : IndexList 𝓒.Color} (h : s.HasNoContr) :
     IndexListColorProp 𝓒 s := by
   simp [IndexListColorProp]
-  haveI : IsEmpty (s.contrSubtype) := s.hasNoContr_is_empty h
+  haveI : IsEmpty (s.contrSubtype) := s.contrSubtype_is_empty_of_hasNoContr h
   simp
 
 /-!
@@ -73,7 +73,7 @@ lemma contrPairSet_dual_snd_lt_self (x : l.1.contrPairSet) :
   rw [← l.contrPairSet_fst_eq_dual_snd]
   exact x.2.1
 
-/-- An equivalence between two coppies of `𝓒.contrPairSet s` and `𝓒.contrSubtype s`.
+/-- An equivalence between two coppies of `l.1.contrPairSet` and `l.1.contrSubtype`.
   This equivalence exists due to the ordering on pairs in `𝓒.contrPairSet s`. -/
 def contrPairEquiv : l.1.contrPairSet ⊕ l.1.contrPairSet ≃ l.1.contrSubtype where
   toFun x :=
@@ -141,20 +141,123 @@ lemma splitContr_map :
 def contr : IndexListColor 𝓒 :=
   ⟨l.1.contrIndexList, indexListColorProp_of_hasNoContr l.1.contrIndexList_hasNoContr⟩
 
+/-- Contracting twice is equivalent to contracting once. -/
+@[simp]
+lemma contr_contr : l.contr.contr = l.contr := by
+  apply Subtype.ext
+  exact l.1.contrIndexList_contrIndexList
+
+@[simp]
+lemma contr_numIndices : l.contr.1.numIndices = l.1.noContrFinset.card :=
+  l.1.contrIndexList_numIndices
+
+lemma contr_colorMap :
+    l.1.colorMap ∘ l.splitContr.symm ∘ Sum.inr = l.contr.1.colorMap ∘
+    (Fin.castOrderIso l.contr_numIndices.symm).toEquiv.toFun := by
+  funext x
+  simp only [Function.comp_apply, colorMap, List.get_eq_getElem, contr, contrIndexList, fromFinMap,
+    Equiv.toFun_as_coe, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Fin.coe_cast,
+    List.getElem_map, Fin.getElem_list, Fin.cast_mk, Fin.eta]
+  rfl
+
+/-! TODO: Prove applying contr twice equals applying it once. -/
 /-!
 
-## Equivalence relation on IndexListColor
+## Equivalence relation on IndexListColor due to permutation
 
 -/
 
 /-- Two index lists are related if there contracted lists have the same id's for indices,
   and the color of indices with the same id sit are the same.
   This will allow us to add and compare tensors. -/
-def rel (s1 s2 : IndexListColor 𝓒) : Prop :=
+def PermContr (s1 s2 : IndexListColor 𝓒) : Prop :=
   List.Perm (s1.contr.1.map Index.id) (s2.contr.1.map Index.id)
-  ∧ ∀ (l1 : s1.contr.1.toPosFinset)
-      (l2 : s2.contr.1.toPosFinset),
-      l1.1.2.id = l2.1.2.id → l1.1.2.toColor = l2.1.2.toColor
+  ∧ ∀ (i : Fin s1.contr.1.length) (j : Fin s2.contr.1.length),
+      s1.contr.1.idMap i = s2.contr.1.idMap j →
+      s1.contr.1.colorMap i = s2.contr.1.colorMap j
+
+lemma PermContr.refl : Reflexive (@PermContr 𝓒 _) := by
+  intro l
+  simp only [PermContr, List.Perm.refl, true_and]
+  have h1 : l.contr.1.HasNoContr := l.1.contrIndexList_hasNoContr
+  exact fun i j a => hasNoContr_color_eq_of_id_eq (↑l.contr) h1 i j a
+
+lemma PermContr.symm : Symmetric (@PermContr 𝓒 _) :=
+  fun _ _ h => And.intro (List.Perm.symm h.1) fun i j hij => (h.2 j i hij.symm).symm
+
+/-- Given an index in `s1` the index in `s2` related by `PermContr` with the same id. -/
+def PermContr.get {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) (i : Fin s1.contr.1.length) :
+    Fin s2.contr.1.length :=
+  (Fin.find (fun j => s1.contr.1.idMap i = s2.contr.1.idMap j)).get (by
+    rw [Fin.isSome_find_iff]
+    have h2 : s1.contr.1.idMap i ∈ (List.map Index.id s2.contr.1) := by
+      rw [← List.Perm.mem_iff h.1]
+      simp only [List.mem_map]
+      use s1.contr.1.get i
+      simp_all only [true_and, List.get_eq_getElem]
+      apply And.intro
+      · exact List.getElem_mem (s1.contr.1) (↑i) i.isLt
+      · rfl
+    simp only [List.mem_map] at h2
+    obtain ⟨j, hj1, hj2⟩ := h2
+    obtain ⟨j', hj'⟩ := List.mem_iff_get.mp hj1
+    use j'
+    rw [← hj2]
+    simp [idMap, hj']
+    change _ = (s2.contr.1.get j').id
+    rw [hj'])
+
+lemma PermContr.some_get_eq_find {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
+    (i : Fin s1.contr.1.length) :
+    Fin.find (fun j => s1.contr.1.idMap i = s2.contr.1.idMap j) = some (h.get i) := by
+  simp [PermContr.get]
+
+lemma PermContr.get_id {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
+    (i : Fin s1.contr.1.length) :
+    s2.contr.1.idMap (h.get i) = s1.contr.1.idMap i := by
+  have h1 := h.some_get_eq_find i
+  rw [Fin.find_eq_some_iff] at h1
+  exact h1.1.symm
+
+lemma PermContr.get_unique {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
+    {i : Fin s1.contr.1.length} {j : Fin s2.contr.1.length}
+    (hij : s1.contr.1.idMap i = s2.contr.1.idMap j) :
+    j = h.get i := by
+  by_contra hn
+  refine (?_ : ¬ s2.contr.1.NoContr j) (s2.1.contrIndexList_hasNoContr j)
+  simp [NoContr]
+  use PermContr.get h i
+  apply And.intro hn
+  rw [← hij, PermContr.get_id]
+
+@[simp]
+lemma PermContr.get_symm_apply_get_apply {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
+    (i : Fin s1.contr.1.length) : h.symm.get (h.get i) = i :=
+  (h.symm.get_unique (h.get_id i)).symm
+
+lemma PermContr.get_apply_get_symm_apply {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2)
+    (i : Fin s2.contr.1.length) : h.get (h.symm.get i) = i :=
+  (h.get_unique (h.symm.get_id i)).symm
+
+/-- Equivalence of indexing types for two `IndexListColor` related by `PermContr`. -/
+def PermContr.toEquiv {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
+    Fin s1.contr.1.length ≃ Fin s2.contr.1.length where
+  toFun := h.get
+  invFun := h.symm.get
+  left_inv x := by
+    simp
+  right_inv x := by
+    simp
+
+lemma PermContr.toEquiv_symm {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
+    h.toEquiv.symm = h.symm.toEquiv := by
+  rfl
+
+lemma PermContr.toEquiv_colorMap {s1 s2 : IndexListColor 𝓒} (h : PermContr s1 s2) :
+    s2.contr.1.colorMap = s1.contr.1.colorMap ∘ h.toEquiv.symm := by
+  funext x
+  refine (h.2 _ _ ?_).symm
+  simp [← h.get_id, toEquiv]
 
 /-! TODO: Show that `rel` is indeed an equivalence relation. -/
 
@@ -166,16 +269,28 @@ def rel (s1 s2 : IndexListColor 𝓒) : Prop :=
 
 /-- Appending two `IndexListColor` whose correpsonding appended index list
   satisfies `IndexListColorProp`. -/
-def append (s1 s2 : IndexListColor 𝓒) (h : IndexListColorProp 𝓒 (s1.1 ++ s2.1)) :
+def prod (s1 s2 : IndexListColor 𝓒) (h : IndexListColorProp 𝓒 (s1.1 ++ s2.1)) :
     IndexListColor 𝓒 := ⟨s1.1 ++ s2.1, h⟩
 
-@[simp]
-lemma append_length {s1 s2 : IndexListColor 𝓒} (h : IndexListColorProp 𝓒 (s1.1 ++ s2.1))
-    (h1 : n = s1.1.length) (h2 : m = s2.1.length) :
-    n + m = (append s1 s2 h).1.length := by
-  erw [List.length_append]
-  simp only [h1, h2]
+lemma prod_numIndices {s1 s2 : IndexListColor 𝓒} :
+    (s1.1 ++ s2.1).numIndices = s1.1.numIndices + s2.1.numIndices :=
+  List.length_append s1.1 s2.1
 
+lemma prod_colorMap {s1 s2 : IndexListColor 𝓒} (h : IndexListColorProp 𝓒 (s1.1 ++ s2.1)) :
+    Sum.elim s1.1.colorMap s2.1.colorMap =
+    (s1.prod s2 h).1.colorMap ∘ ((Fin.castOrderIso prod_numIndices).toEquiv.trans
+    finSumFinEquiv.symm).symm := by
+  funext x
+  match x with
+  | Sum.inl x =>
+    simp [prod, colorMap, fromFinMap]
+    rw [List.getElem_append_left]
+  | Sum.inr x =>
+    simp [prod, colorMap, fromFinMap]
+    rw [List.getElem_append_right]
+    simp [numIndices]
+    simp [numIndices]
+    simp [numIndices]
 end IndexListColor
 
 end IndexNotation
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean
index 80b63fb..f640dc7 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean
@@ -5,6 +5,8 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexListColor
 import HepLean.SpaceTime.LorentzTensor.Basic
+import HepLean.SpaceTime.LorentzTensor.RisingLowering
+import HepLean.SpaceTime.LorentzTensor.Contraction
 /-!
 
 # The structure of a tensor with a string of indices
@@ -12,6 +14,8 @@ import HepLean.SpaceTime.LorentzTensor.Basic
 -/
 
 namespace TensorStructure
+noncomputable section
+
 open TensorColor
 open IndexNotation
 
@@ -25,22 +29,86 @@ variable {d : ℕ} {X Y Y' Z W : Type} [Fintype X] [DecidableEq X] [Fintype Y] [
 variable [IndexNotation 𝓣.Color] [Fintype 𝓣.Color] [DecidableEq 𝓣.Color]
 
 /-- The structure an tensor with a index specification e.g. `ᵘ¹ᵤ₂`. -/
-structure TensorIndex (cn : Fin n → 𝓣.Color) where
-  /-- The underlying tensor. -/
-  tensor : 𝓣.Tensor cn
+structure TensorIndex where
   /-- The list of indices. -/
   index : IndexListColor 𝓣.toTensorColor
-  /-- The number of indices matches the number of vector spaces in the tensor. -/
-  nat_eq : n = index.1.length
-  /-- The equivalence classes of colors of the tensor and the index list agree. -/
-  quot_eq : 𝓣.colorQuot ∘ index.1.colorMap ∘ Fin.cast nat_eq = 𝓣.colorQuot ∘ cn
+  /-- The underlying tensor. -/
+  tensor : 𝓣.Tensor index.1.colorMap
 
 namespace TensorIndex
-
+open TensorColor
 variable {𝓣 : TensorStructure R} [IndexNotation 𝓣.Color] [Fintype 𝓣.Color] [DecidableEq 𝓣.Color]
-variable {n m : ℕ} {cn : Fin n → 𝓣.Color} {cm : Fin m → 𝓣.Color} (T : TensorIndex 𝓣 cn)
+variable {n m : ℕ} {cn : Fin n → 𝓣.Color} {cm : Fin m → 𝓣.Color}
 
+lemma index_eq_colorMap_eq {T₁ T₂ : 𝓣.TensorIndex} (hi : T₁.index = T₂.index) :
+    (T₂.index).1.colorMap = (T₁.index).1.colorMap ∘ (Fin.castOrderIso (by rw [hi])).toEquiv := by
+  funext i
+  congr 1
+  rw [hi]
+  simp only [RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply]
+  exact
+    (Fin.heq_ext_iff (congrArg IndexList.numIndices (congrArg Subtype.val (id (Eq.symm hi))))).mpr
+      rfl
+
+lemma ext (T₁ T₂ : 𝓣.TensorIndex) (hi : T₁.index = T₂.index)
+    (h : T₁.tensor = 𝓣.mapIso (Fin.castOrderIso (by rw [hi])).toEquiv
+    (index_eq_colorMap_eq hi) T₂.tensor) : T₁ = T₂ := by
+  cases T₁; cases T₂
+  simp at hi
+  subst hi
+  simp_all
+
+/-- The construction of a `TensorIndex` from a tensor, a IndexListColor, and a condition
+  on the dual maps. -/
+def mkDualMap (T : 𝓣.Tensor cn) (l : IndexListColor 𝓣.toTensorColor) (hn : n = l.1.length)
+    (hd : DualMap l.1.colorMap (cn ∘ Fin.cast hn.symm)) :
+    𝓣.TensorIndex where
+  index := l
+  tensor :=
+      𝓣.mapIso (Equiv.refl _) (DualMap.split_dual' (by simp [hd])) <|
+      𝓣.dualize (DualMap.split l.1.colorMap (cn ∘ Fin.cast hn.symm)) <|
+      (𝓣.mapIso (Fin.castOrderIso hn).toEquiv rfl T : 𝓣.Tensor (cn ∘ Fin.cast hn.symm))
+
+/-- The contraction of indices in a `TensorIndex`. -/
+def contr (T : 𝓣.TensorIndex) : 𝓣.TensorIndex where
+  index := T.index.contr
+  tensor :=
+      𝓣.mapIso (Fin.castOrderIso T.index.contr_numIndices.symm).toEquiv
+      T.index.contr_colorMap <|
+      𝓣.contr (T.index.splitContr).symm T.index.splitContr_map T.tensor
+
+/-- The tensor product of two `TensorIndex`. -/
+def prod (T₁ T₂ : 𝓣.TensorIndex)
+    (h : IndexListColorProp 𝓣.toTensorColor (T₁.index.1 ++ T₂.index.1)) : 𝓣.TensorIndex where
+  index := T₁.index.prod T₂.index h
+  tensor :=
+      𝓣.mapIso ((Fin.castOrderIso (IndexListColor.prod_numIndices)).toEquiv.trans
+        (finSumFinEquiv.symm)).symm
+      (IndexListColor.prod_colorMap h) <|
+      𝓣.tensoratorEquiv _ _ (T₁.tensor ⊗ₜ[R] T₂.tensor)
+
+/-- The scalar multiplication of a `TensorIndex` by an element of `R`. -/
+def smul (r : R) (T : 𝓣.TensorIndex) : 𝓣.TensorIndex where
+  index := T.index
+  tensor := r • T.tensor
+
+/-- The addition of two `TensorIndex` given the condition that, after contraction,
+  their index lists are the same. -/
+def add (T₁ T₂ : 𝓣.TensorIndex) (h : IndexListColor.PermContr T₁.index T₂.index) :
+    𝓣.TensorIndex where
+  index := T₁.index.contr
+  tensor :=
+    let T1 := T₁.contr.tensor
+    let T2 :𝓣.Tensor (T₁.contr.index).1.colorMap :=
+      𝓣.mapIso h.toEquiv.symm h.toEquiv_colorMap T₂.contr.tensor
+    T1 + T2
+
+/-- An (equivalence) relation on two `TensorIndex` given that after contraction,
+  the two underlying tensors are the equal. -/
+def Rel (T₁ T₂ : 𝓣.TensorIndex) : Prop :=
+  T₁.index.PermContr T₂.index ∧ ∀ (h : T₁.index.PermContr T₂.index),
+  T₁.contr.tensor = 𝓣.mapIso h.toEquiv.symm h.toEquiv_colorMap T₂.contr.tensor
 
 end TensorIndex
-
+end
 end TensorStructure
diff --git a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
index 7a95683..180502a 100644
--- a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
+++ b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean
@@ -232,3 +232,77 @@ lemma dualize_equivariant_apply (e : C ⊕ P ≃ X) (g : G) (x : 𝓣.Tensor cX)
 end TensorStructure
 
 end
+namespace TensorColor
+
+variable {𝓒 : TensorColor} [DecidableEq 𝓒.Color] [Fintype 𝓒.Color]
+
+variable {d : ℕ} {X Y Y' Z W C P : Type} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
+  [Fintype Y'] [DecidableEq Y'] [Fintype Z] [DecidableEq Z] [Fintype W] [DecidableEq W]
+  [Fintype C] [DecidableEq C] [Fintype P] [DecidableEq P]
+
+/-!
+
+## Dual maps
+
+-/
+
+/-- Two color maps are said to be dual if their quotents are dual. -/
+def DualMap (c₁ : X → 𝓒.Color) (c₂ : X → 𝓒.Color) : Prop :=
+  𝓒.colorQuot ∘ c₁ = 𝓒.colorQuot ∘ c₂
+
+namespace DualMap
+
+variable {c₁ c₂ c₃ : X → 𝓒.Color}
+
+lemma refl : DualMap c₁ c₁ := by
+  simp [DualMap]
+
+lemma symm (h : DualMap c₁ c₂) : DualMap c₂ c₁ := by
+  rw [DualMap] at h ⊢
+  exact h.symm
+
+lemma trans (h : DualMap c₁ c₂) (h' : DualMap c₂ c₃) : DualMap c₁ c₃ := by
+  rw [DualMap] at h h' ⊢
+  exact h.trans h'
+
+/-- The splitting of `X` given two color maps based on the equality of the color. -/
+def split (c₁ c₂ : X → 𝓒.Color) : { x // c₁ x ≠ c₂ x} ⊕ { x // c₁ x = c₂ x} ≃ X :=
+  ((Equiv.Set.sumCompl {x | c₁ x = c₂ x}).symm.trans (Equiv.sumComm _ _)).symm
+
+lemma dual_eq_of_neq (h : DualMap c₁ c₂) {x : X} (h' : c₁ x ≠ c₂ x) :
+    𝓒.τ (c₁ x) = c₂ x := by
+  rw [DualMap] at h
+  have h1 := congrFun h x
+  simp [colorQuot, HasEquiv.Equiv, Setoid.r, colorRel] at h1
+  simp_all only [ne_eq, false_or]
+  exact 𝓒.τ_involutive (c₂ x)
+
+@[simp]
+lemma split_dual (h : DualMap c₁ c₂) :
+    Sum.elim (𝓒.τ ∘ c₁ ∘ (split c₁ c₂) ∘ Sum.inl) (c₁ ∘ (split c₁ c₂) ∘ Sum.inr)
+    ∘ (split c₁ c₂).symm = c₂ := by
+  rw [Equiv.comp_symm_eq]
+  funext x
+  match x with
+  | Sum.inl x =>
+    exact h.dual_eq_of_neq x.2
+  | Sum.inr x =>
+    exact x.2
+
+@[simp]
+lemma split_dual' (h : DualMap c₁ c₂) :
+    Sum.elim (𝓒.τ ∘ c₂ ∘ (split c₁ c₂) ∘ Sum.inl) (c₂ ∘ (split c₁ c₂) ∘ Sum.inr) ∘
+    (split c₁ c₂).symm = c₁ := by
+  rw [Equiv.comp_symm_eq]
+  funext x
+  match x with
+  | Sum.inl x =>
+    change 𝓒.τ (c₂ x) = c₁ x
+    rw [← h.dual_eq_of_neq x.2]
+    exact (𝓒.τ_involutive (c₁ x))
+  | Sum.inr x =>
+    exact x.2.symm
+
+end DualMap
+
+end TensorColor