refactor: Index notation

HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Basic.lean

@@ -254,6 +254,104 @@ lemma fromFinMap_numIndices {n : ℕ} (f : Fin n → Index X) :
     (fromFinMap f).length = n := by
   simp [fromFinMap, length]
 
+/-!
+
+## Appending index lists.
+
+-/
+
+section append
+
+variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
+variable (l l2 l3 : IndexList X)
+
+instance : HAppend (IndexList X) (IndexList X) (IndexList X) where
+  hAppend := fun l l2 => {val := l.val ++ l2.val}
+
+lemma append_assoc : l ++ l2 ++ l3 = l ++ (l2 ++ l3) := by
+  apply ext
+  change l.val ++ l2.val ++ l3.val = l.val ++ (l2.val ++ l3.val)
+  exact List.append_assoc l.val l2.val l3.val
+
+def appendEquiv {l l2 : IndexList X} : Fin l.length ⊕ Fin l2.length ≃ Fin (l ++ l2).length :=
+  finSumFinEquiv.trans (Fin.castOrderIso (List.length_append _ _).symm).toEquiv
+
+def appendInl : Fin l.length ↪ Fin (l ++ l2).length where
+  toFun := appendEquiv ∘ Sum.inl
+  inj' := by
+    intro i j h
+    simp [Function.comp] at h
+    exact h
+
+def appendInr : Fin l2.length ↪ Fin (l ++ l2).length where
+  toFun := appendEquiv ∘ Sum.inr
+  inj' := by
+    intro i j h
+    simp [Function.comp] at h
+    exact h
+
+@[simp]
+lemma appendInl_appendEquiv :
+    (l.appendInl l2).trans appendEquiv.symm.toEmbedding =
+    {toFun := Sum.inl, inj' := Sum.inl_injective} := by
+  ext i
+  simp [appendInl]
+
+@[simp]
+lemma appendInr_appendEquiv :
+    (l.appendInr l2).trans appendEquiv.symm.toEmbedding =
+    {toFun := Sum.inr, inj' := Sum.inr_injective} := by
+  ext i
+  simp [appendInr]
+
+@[simp]
+lemma append_val {l l2 : IndexList X} : (l ++ l2).val = l.val ++ l2.val := by
+  rfl
+
+@[simp]
+lemma idMap_append_inl {l l2 : IndexList X} (i : Fin l.length) :
+    (l ++ l2).idMap (appendEquiv (Sum.inl i)) = l.idMap i := by
+  simp [appendEquiv, idMap]
+  rw [List.getElem_append_left]
+  rfl
+
+@[simp]
+lemma idMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) :
+    (l ++ l2).idMap (appendEquiv (Sum.inr i)) = l2.idMap i := by
+  simp [appendEquiv, idMap, IndexList.length]
+  rw [List.getElem_append_right]
+  simp
+  omega
+  omega
+
+@[simp]
+lemma colorMap_append_inl {l l2 : IndexList X} (i : Fin l.length) :
+    (l ++ l2).colorMap (appendEquiv (Sum.inl i)) = l.colorMap i := by
+  simp [appendEquiv, colorMap, IndexList.length]
+  rw [List.getElem_append_left]
+
+@[simp]
+lemma colorMap_append_inl' :
+    (l ++ l2).colorMap ∘ appendEquiv ∘ Sum.inl = l.colorMap := by
+  funext i
+  simp
+
+@[simp]
+lemma colorMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) :
+    (l ++ l2).colorMap (appendEquiv (Sum.inr i)) = l2.colorMap i := by
+  simp [appendEquiv, colorMap, IndexList.length]
+  rw [List.getElem_append_right]
+  simp
+  omega
+  omega
+
+@[simp]
+lemma colorMap_append_inr' :
+    (l ++ l2).colorMap ∘ appendEquiv ∘ Sum.inr = l2.colorMap := by
+  funext i
+  simp
+
+end append
 
 end IndexList
 

HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/Color.lean

@@ -20,20 +20,143 @@ a Tensor Color structure.
 namespace IndexNotation
 
 
+namespace IndexList
+
+variable {𝓒 : TensorColor}
+variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
+variable (l l2 l3 : IndexList 𝓒.Color)
+
+def ColorCond : Prop := Option.map l.colorMap ∘
+  l.getDual? = Option.map (𝓒.τ ∘ l.colorMap) ∘
+  Option.guard fun i => (l.getDual? i).isSome
+
+namespace ColorCond
+variable {l l2 l3 : IndexList 𝓒.Color}
+lemma iff_withDual :
+    l.ColorCond ↔ ∀ (i : l.withDual), 𝓒.τ
+    (l.colorMap ((l.getDual? i).get (l.withDual_isSome i))) = l.colorMap i := by
+  refine Iff.intro (fun h i => ?_) (fun h => ?_)
+  · have h' := congrFun h i
+    simp at h'
+    rw [show l.getDual? i = some ((l.getDual? i).get (l.withDual_isSome i)) by simp] at h'
+    have h'' : (Option.guard (fun i => (l.getDual? i).isSome = true) ↑i) = i := by
+      apply Option.guard_eq_some.mpr
+      simp [l.withDual_isSome i]
+    rw [h'', Option.map_some', Option.map_some'] at h'
+    simp at h'
+    rw [h']
+    exact 𝓒.τ_involutive (l.colorMap i)
+  · funext i
+    by_cases hi : (l.getDual? i).isSome
+    · have h'' : (Option.guard (fun i => (l.getDual? i).isSome = true) ↑i) = i := by
+        apply Option.guard_eq_some.mpr
+        simp
+        exact  hi
+      simp only [Function.comp_apply, h'', Option.map_some']
+      rw [show l.getDual? ↑i = some ((l.getDual? i).get hi) by simp]
+      rw [Option.map_some']
+      simp
+      have hii := h ⟨i, by simp [withDual, hi]⟩
+      simp at hii
+      rw [← hii]
+      exact (𝓒.τ_involutive _).symm
+    · simp [Option.guard, hi]
+      exact Option.not_isSome_iff_eq_none.mp hi
+
+lemma iff_on_isSome : l.ColorCond ↔ ∀ (i : Fin l.length) (h : (l.getDual? i).isSome), 𝓒.τ
+    (l.colorMap ((l.getDual? i).get h)) = l.colorMap i := by
+  rw [iff_withDual]
+  simp
+
+lemma assoc (h : ColorCond (l ++ l2 ++ l3)) :
+    ColorCond (l ++ (l2 ++ l3)) := by
+  rw [← append_assoc]
+  exact h
+
+lemma inl (h : ColorCond (l ++ l2)) : ColorCond l := by
+  rw [iff_withDual] at h ⊢
+  intro i
+  have hi' := h ⟨appendEquiv (Sum.inl i), by
+    rw [inl_mem_withDual_append_iff]
+    simp_all⟩
+  have hn : (Option.map (appendEquiv ∘ Sum.inl) (l.getDual? ↑i) : Option (Fin (l ++ l2).length)) =
+        some (appendEquiv (Sum.inl ((l.getDual? i).get (l.withDual_isSome i)))) := by
+    trans Option.map (appendEquiv ∘ Sum.inl) (some ((l.getDual? i).get (l.withDual_isSome i)))
+    simp
+    rw [Option.map_some']
+    simp
+  simpa [hn] using hi'
+
+lemma symm (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond (l ++ l2)) :
+    ColorCond (l2 ++ l) := by
+  rw [iff_on_isSome] at h ⊢
+  intro j hj
+  obtain ⟨k, hk⟩ := appendEquiv.surjective j
+  subst hk
+  rw [append_withDual_eq_withUniqueDual_symm] at hu
+  rw [← mem_withDual_iff_isSome, ← hu] at hj
+  match k with
+  | Sum.inl k =>
+    have hn := l2.append_inl_not_mem_withDual_of_withDualInOther l k hj
+    by_cases hk' : (l2.getDual? k).isSome
+    · simp_all
+      have hk'' := h (appendEquiv (Sum.inr k))
+      simp at hk''
+      simp_all
+    · simp_all
+      have hn' : (l2.getDualInOther? l k).isSome := by
+        simp_all
+      have hk'' := h (appendEquiv (Sum.inr k))
+      simp at hk''
+      simp_all
+  | Sum.inr k =>
+    have hn := l2.append_inr_not_mem_withDual_of_withDualInOther l k hj
+    by_cases hk' : (l.getDual? k).isSome
+    · simp_all
+      have hk'' := h (appendEquiv (Sum.inl k))
+      simp at hk''
+      simp_all
+    · simp_all
+      have hn' : (l.getDualInOther? l2 k).isSome := by
+        simp_all
+      have hk'' := h (appendEquiv (Sum.inl k))
+      simp at hk''
+      simp_all
+
+lemma inr  (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond (l ++ l2)) :
+    ColorCond l2 := inl (symm hu h)
+
+end ColorCond
+
+
+
+end IndexList
+
+
 variable (𝓒 : TensorColor)
 variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
 
 structure ColorIndexList (𝓒 : TensorColor) [IndexNotation 𝓒.Color] extends IndexList 𝓒.Color where
   unique_duals : toIndexList.withDual = toIndexList.withUniqueDual
-  dual_color : (Option.map toIndexList.colorMap) ∘ toIndexList.getDual?
+  dual_color : IndexList.ColorCond toIndexList
-    = (Option.map (𝓒.τ ∘ toIndexList.colorMap)) ∘
-      Option.guard (fun i => (toIndexList.getDual? i).isSome)
 
 namespace ColorIndexList
 
 variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color]
 
 variable (l l2 : ColorIndexList 𝓒)
+open IndexList
+
+def empty : ColorIndexList 𝓒 where
+  val := ∅
+  unique_duals := by
+    rfl
+  dual_color := by
+    rfl
+
+@[simp]
+def colorMap' : 𝓒.ColorMap (Fin l.length) :=
+  l.colorMap
 
 @[ext]
 lemma ext {l l' : ColorIndexList 𝓒} (h : l.val = l'.val) : l = l' := by
@@ -68,8 +191,7 @@ lemma contr_contr : l.contr.contr = l.contr := by
 
 -/
 
-def contrEquiv :
+def contrEquiv : (l.withUniqueDualLT ⊕ l.withUniqueDualLT) ⊕ Fin l.contr.length ≃ Fin l.length :=
-    (l.withUniqueDualLT ⊕ l.withUniqueDualLT) ⊕ Fin l.contr.length ≃ Fin l.length :=
   (Equiv.sumCongr (l.withUniqueLTGTEquiv) (Equiv.refl _)).trans <|
   (Equiv.sumCongr (Equiv.subtypeEquivRight (by
   simp [l.unique_duals])) (Fin.castOrderIso l.contrIndexList_length).toEquiv).trans <|
@@ -81,8 +203,64 @@ def contrEquiv :
 
 -/
 
-def append (h : (l.toIndexList ++ l2.toIndexList).withUniqueDual =
+
-     (l.toIndexList ++ l2.toIndexList).withDual ) : ColorIndexList 𝓒 := by
+def AppendCond : Prop :=
+  (l.toIndexList ++ l2.toIndexList).withUniqueDual = (l.toIndexList ++ l2.toIndexList).withDual
+  ∧ ColorCond (l.toIndexList ++ l2.toIndexList)
+
+namespace AppendCond
+
+variable {l l2 l3 : ColorIndexList 𝓒}
+
+lemma symm (h : AppendCond l l2) : AppendCond l2 l := by
+  apply And.intro _ (h.2.symm h.1)
+  rw [append_withDual_eq_withUniqueDual_symm]
+  exact h.1
+
+end AppendCond
+
+def append (h : AppendCond l l2) : ColorIndexList 𝓒 where
+  toIndexList := l.toIndexList ++ l2.toIndexList
+  unique_duals := h.1.symm
+  dual_color := h.2
+
+scoped[IndexNotation.ColorIndexList] notation l " ++["h"] " l2 => append l l2 h
+
+@[simp]
+lemma append_toIndexList (h : AppendCond l l2) :
+    (l ++[h] l2).toIndexList = l.toIndexList ++ l2.toIndexList := by
+  rfl
+
+namespace AppendCond
+
+variable {l l2 l3 : ColorIndexList 𝓒}
+
+lemma inr (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) :
+    AppendCond l2 l3 := by
+  apply And.intro
+  · have h1 := h'.1
+    simp at h1
+    rw [append_assoc] at h1
+    exact l.append_withDual_eq_withUniqueDual_inr (l2.toIndexList ++ l3.toIndexList) h1
+  · have h1 := h'.2
+    simp at h1
+    rw [append_assoc] at h1
+    refine ColorCond.inr ?_ h1
+    rw [← append_assoc]
+    exact h'.1
+
+lemma assoc (h : AppendCond l l2) (h' : AppendCond (l ++[h] l2) l3) :
+    AppendCond l (l2 ++[h.inr h'] l3) := by
+  apply And.intro
+  · simp
+    rw [← append_assoc]
+    simpa using h'.1
+  · simp
+    rw [← append_assoc]
+    exact h'.2
+
+
+end AppendCond
 
 end ColorIndexList
 

HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/DualInOther.lean

@@ -41,7 +41,6 @@ def getDualInOther? (i : Fin l.length) : Option (Fin l2.length) :=
   Fin.find (fun j => l.AreDualInOther l2 i j)
 
 
-
 /-!
 
 ## With dual other.
@@ -51,6 +50,11 @@ def getDualInOther? (i : Fin l.length) : Option (Fin l2.length) :=
 def withDualInOther : Finset (Fin l.length) :=
   Finset.filter (fun i => (l.getDualInOther? l2 i).isSome) Finset.univ
 
+@[simp]
+lemma mem_withInDualOther_iff_isSome (i : Fin l.length) :
+    i ∈ l.withDualInOther l2 ↔ (l.getDualInOther? l2 i).isSome := by
+  simp only [withDualInOther, getDualInOther?, Finset.mem_filter, Finset.mem_univ, true_and]
+
 lemma mem_withInDualOther_iff_exists :
     i ∈ l.withDualInOther l2 ↔ ∃ (j : Fin l2.length), l.AreDualInOther l2 i j := by
   simp [withDualInOther, Finset.mem_filter, Finset.mem_univ, getDualInOther?]

HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/UniqueDual.lean

@@ -31,11 +31,23 @@ def withUniqueDual : Finset (Fin l.length) :=
   Finset.filter (fun i => i ∈ l.withDual ∧
     ∀ j, l.AreDualInSelf i j → j = l.getDual? i) Finset.univ
 
+@[simp]
+lemma mem_withDual_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) :
+    i ∈ l.withDual := by
+  simp only [withUniqueDual, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ,
+    true_and] at h
+  simpa using h.1
+
+@[simp]
+lemma mem_withUniqueDual_isSome (i : Fin l.length) (h : i ∈ l.withUniqueDual) :
+    (l.getDual? i).isSome := by
+  simpa using mem_withDual_of_mem_withUniqueDual l i h
+
 lemma mem_withDual_of_withUniqueDual (i : l.withUniqueDual) :
     i.1 ∈ l.withDual := by
   have hi := i.2
-  simp [withUniqueDual, Finset.mem_filter, Finset.mem_univ] at hi
+  simp only [withUniqueDual, Finset.mem_filter, Finset.mem_univ] at hi
-  exact hi.1
+  exact hi.2.1
 
 def fromWithUnique (i : l.withUniqueDual) : l.withDual :=
   ⟨i.1, l.mem_withDual_of_withUniqueDual i⟩
@@ -61,6 +73,100 @@ lemma eq_of_areDualInSelf_withUniqueDual {j k : Fin l.length} (i : l.withUniqueD
   have hk' := all_dual_eq_getDual_of_withUniqueDual l i k hk
   rw [hj', hk']
 
+/-!
+
+## Properties of getDual?
+
+-/
+
+lemma all_dual_eq_getDual?_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) :
+    ∀ j, l.AreDualInSelf i j → j = l.getDual? i := by
+  simp [withUniqueDual] at h
+  exact fun j hj => h.2 j hj
+
+lemma some_eq_getDual?_of_withUniqueDual_iff (i j : Fin l.length) (h : i ∈ l.withUniqueDual) :
+    l.AreDualInSelf i j ↔ some j = l.getDual? i := by
+  apply Iff.intro
+  intro h'
+  exact all_dual_eq_getDual?_of_mem_withUniqueDual l i h j h'
+  intro h'
+  have hj : j = (l.getDual? i).get (mem_withUniqueDual_isSome l i h) :=
+    Eq.symm (Option.get_of_mem (mem_withUniqueDual_isSome l i h) (id (Eq.symm h')))
+  subst hj
+  exact (getDual?_get_areDualInSelf l i (mem_withUniqueDual_isSome l i h)).symm
+
+@[simp]
+lemma eq_getDual?_get_of_withUniqueDual_iff (i j : Fin l.length) (h : i ∈ l.withUniqueDual) :
+    l.AreDualInSelf i j ↔ j = (l.getDual? i).get (mem_withUniqueDual_isSome l i h) := by
+  rw [l.some_eq_getDual?_of_withUniqueDual_iff i j h]
+  refine Iff.intro (fun h' => ?_) (fun h' => ?_)
+  exact Eq.symm (Option.get_of_mem (mem_withUniqueDual_isSome l i h) (id (Eq.symm h')))
+  simp [h']
+
+@[simp]
+lemma getDual?_get_getDual?_get_of_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) :
+    (l.getDual? ((l.getDual? i).get (mem_withUniqueDual_isSome l i h))).get
+      (l.getDual?_getDual?_get_isSome i (mem_withUniqueDual_isSome l i h)) = i := by
+  by_contra hn
+  have h' : l.AreDualInSelf i  ((l.getDual? ((l.getDual? i).get (mem_withUniqueDual_isSome l i h))).get (
+      getDual?_getDual?_get_isSome l i (mem_withUniqueDual_isSome l i h))) := by
+    simp [AreDualInSelf, hn]
+    exact fun a => hn (id (Eq.symm a))
+  simp [h] at h'
+
+@[simp]
+lemma getDual?_getDual?_get_of_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) :
+    l.getDual? ((l.getDual? i).get (mem_withUniqueDual_isSome l i h)) = some i := by
+  nth_rewrite 3 [← l.getDual?_get_getDual?_get_of_withUniqueDual i h]
+  simp
+
+@[simp]
+lemma getDual?_getDual?_of_withUniqueDual (i : Fin l.length) (h : i ∈ l.withUniqueDual) :
+    (l.getDual? i).bind l.getDual? = some i := by
+  have h1 : (l.getDual? i) = some ((l.getDual? i).get (mem_withUniqueDual_isSome l i h)) := by simp
+  nth_rewrite 1 [h1]
+  rw [Option.some_bind']
+  simp [h]
+
+@[simp]
+lemma getDual?_get_of_mem_withUnique_mem (i : Fin l.length) (h : i ∈ l.withUniqueDual) :
+    (l.getDual? i).get (l.mem_withUniqueDual_isSome i h) ∈ l.withUniqueDual := by
+  simp [withUniqueDual, h]
+  intro j hj
+  have h1 : i = j := by
+    by_contra hn
+    have h' : l.AreDualInSelf i j := by
+      simp [AreDualInSelf, hn]
+      simp_all [AreDualInSelf, getDual, fromWithUnique]
+    simp [h] at h'
+    subst h'
+    simp_all [getDual]
+  subst h1
+  exact Eq.symm (getDual?_getDual?_get_of_withUniqueDual l i h)
+
+/-!
+
+## The equivalence defined by getDual?
+
+-/
+
+def getDualEquiv : l.withUniqueDual ≃ l.withUniqueDual where
+  toFun x := ⟨(l.getDual? x).get (l.mem_withUniqueDual_isSome x.1 x.2), by simp⟩
+  invFun x := ⟨(l.getDual? x).get (l.mem_withUniqueDual_isSome x.1 x.2), by simp⟩
+  left_inv x := SetCoe.ext (by simp)
+  right_inv x := SetCoe.ext (by simp)
+
+@[simp]
+lemma getDualEquiv_involutive : Function.Involutive l.getDualEquiv := by
+  intro x
+  simp [getDualEquiv, fromWithUnique]
+
+
+/-!
+
+## Properties of getDual! etc.
+
+-/
 lemma eq_getDual_of_withUniqueDual_iff (i : l.withUniqueDual) (j : Fin l.length) :
     l.AreDualInSelf i j ↔ j = l.getDual! i := by
   apply Iff.intro
@@ -101,45 +207,6 @@ lemma getDual?_getDual_of_withUniqueDual (i : l.withUniqueDual) :
   rw [getDual?_eq_some_getDual!]
   simp
 
-@[simp]
-lemma getDual?_getDual?_of_withUniqueDualInOther (i : l.withUniqueDual) :
-    (l.getDual? i).bind l.getDual? = some i := by
-  rw [getDual?_eq_some_getDual! l i]
-  simp
-
-
-lemma getDual_of_withUniqueDual_mem (i : l.withUniqueDual) :
-    l.getDual! i ∈ l.withUniqueDual := by
-  simp [withUniqueDual]
-  apply And.intro (getDual_mem_withDual l ⟨↑i, mem_withDual_of_withUniqueDual l i⟩)
-  intro j hj
-  have h1 : i = j := by
-    by_contra hn
-    have h' : l.AreDualInSelf i j := by
-      simp [AreDualInSelf, hn]
-      simp_all [AreDualInSelf, getDual, fromWithUnique]
-    rw [eq_getDual_of_withUniqueDual_iff] at h'
-    subst h'
-    simp_all [getDual]
-  subst h1
-  rfl
-
-def getDualEquiv : l.withUniqueDual ≃ l.withUniqueDual where
-  toFun x := ⟨l.getDual x, l.getDual_of_withUniqueDual_mem x⟩
-  invFun x := ⟨l.getDual x, l.getDual_of_withUniqueDual_mem x⟩
-  left_inv x := SetCoe.ext (by
-    simp only [Subtype.coe_eta, getDual_getDual_of_withUniqueDual]
-    rfl)
-  right_inv x := SetCoe.ext (by
-    simp only [Subtype.coe_eta, getDual_getDual_of_withUniqueDual]
-    rfl)
-
-@[simp]
-lemma getDualEquiv_involutive : Function.Involutive l.getDualEquiv := by
-  intro x
-  simp [getDualEquiv, fromWithUnique]
-
-
 /-!
 
 ## Equality of withUnqiueDual and withDual
@@ -153,17 +220,19 @@ lemma withUnqiueDual_eq_withDual_iff_unique_forall :
   · intro h i j hj
     rw [@Finset.ext_iff] at h
     simp [withUniqueDual] at h
-    exact h i i.2 j hj
+    refine h i ?_ j hj
+    simp
   · intro h
     apply Finset.ext
     intro i
     apply Iff.intro
     · intro hi
       simp [withUniqueDual] at hi
-      exact hi.1
+      simpa using hi.1
     · intro hi
       simp [withUniqueDual]
-      apply And.intro hi
+      apply And.intro
+      simpa using hi
       intro j hj
       exact h ⟨i, hi⟩ j hj
 
@@ -176,15 +245,14 @@ lemma withUnqiueDual_eq_withDual_iff :
     · have hii : i ∈ l.withUniqueDual := by
         simp_all only
       change (l.getDual? i).bind l.getDual?  = _
-      rw [getDual?_getDual?_of_withUniqueDualInOther l ⟨i, hii⟩]
+      simp [hii]
-      simp
       symm
       rw [Option.guard_eq_some]
-      exact ⟨rfl, hi⟩
+      exact ⟨rfl, by simpa using hi⟩
     · rw [getDual?_eq_none_on_not_mem l i hi]
       simp
       symm
-      simpa only [Option.guard, ite_eq_right_iff, imp_false] using hi
+      simpa [Option.guard, ite_eq_right_iff, imp_false] using hi
   · intro h
     rw [withUnqiueDual_eq_withDual_iff_unique_forall]
     intro i j hj
@@ -194,8 +262,8 @@ lemma withUnqiueDual_eq_withDual_iff :
       simp at hj'
       rw [hj']
       symm
-      rw [Option.guard_eq_some]
+      rw [Option.guard_eq_some, hi]
-      exact ⟨rfl, l.mem_withDual_iff_exists.mpr ⟨i, hj.symm⟩⟩
+      exact ⟨rfl, rfl⟩
     · exact hi.symm
     · have hj' := h j
       rw [hi] at hj'

HepLean/SpaceTime/LorentzTensor/IndexNotation/Indices/UniqueDualInOther.lean

@@ -45,6 +45,14 @@ lemma mem_withDualInOther_of_withUniqueDualInOther (i : l.withUniqueDualInOther
     true_and] at hi
   exact hi.2.2.1
 
+@[simp]
+lemma mem_withUniqueDualInOther_isSome (i : Fin l.length) (hi : i ∈ l.withUniqueDualInOther l2) :
+    (l.getDualInOther? l2 i).isSome := by
+  simp only [withUniqueDualInOther, Finset.mem_filter, Finset.mem_univ, true_and] at hi
+  have hi2 := hi.2.1
+  simpa using hi2
+
+
 def fromWithUniqueDualInOther (i : l.withUniqueDualInOther l2) : l.withDualInOther l2 :=
   ⟨i.1, l.mem_withDualInOther_of_withUniqueDualInOther l2 i⟩
 

HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexListColor
+import HepLean.SpaceTime.LorentzTensor.IndexNotation.Indices.Color
 import HepLean.SpaceTime.LorentzTensor.Basic
 import HepLean.SpaceTime.LorentzTensor.RisingLowering
 import HepLean.SpaceTime.LorentzTensor.Contraction
@@ -32,43 +32,54 @@ 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 where
+structure TensorIndex extends ColorIndexList 𝓣.toTensorColor where
-  /-- The list of indices. -/
-  index : IndexListColor 𝓣.toTensorColor
   /-- The underlying tensor. -/
-  tensor : 𝓣.Tensor index.1.colorMap
+  tensor : 𝓣.Tensor toIndexList.colorMap
 
 namespace TensorIndex
-open TensorColor IndexListColor
+
+open TensorColor ColorIndexList
+
 variable {𝓣 : TensorStructure R} [IndexNotation 𝓣.Color] [Fintype 𝓣.Color] [DecidableEq 𝓣.Color]
 variable {n m : ℕ} {cn : Fin n → 𝓣.Color} {cm : Fin m → 𝓣.Color}
 
-lemma index_eq_colorMap_eq {T₁ T₂ : 𝓣.TensorIndex} (hi : T₁.index = T₂.index) :
+lemma colormap_mapIso {T₁ T₂ : 𝓣.TensorIndex} (hi : T₁.toColorIndexList = T₂.toColorIndexList) :
-    (T₂.index).1.colorMap = (T₁.index).1.colorMap ∘ (Fin.castOrderIso (by rw [hi])).toEquiv := by
+    ColorMap.MapIso (Fin.castOrderIso (by simp [IndexList.length, hi])).toEquiv
-  funext i
+    T₁.colorMap T₂.colorMap := by
-  congr 1
+  cases T₁; cases T₂
-  rw [hi]
+  simp [ColorMap.MapIso]
-  simp only [RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply]
+  simp at hi
-  exact
+  rename_i a b c d
-    (Fin.heq_ext_iff (congrArg IndexList.numIndices (congrArg Subtype.val (id (Eq.symm hi))))).mpr
+  cases a
+  cases c
+  rename_i a1 a2 a3 a4 a5 a6
+  cases a1
+  cases a4
+  simp_all
+  simp at hi
+  subst hi
   rfl
 
-lemma ext (T₁ T₂ : 𝓣.TensorIndex) (hi : T₁.index = T₂.index)
+lemma ext {T₁ T₂ : 𝓣.TensorIndex} (hi : T₁.toColorIndexList = T₂.toColorIndexList)
-    (h : T₁.tensor = 𝓣.mapIso (Fin.castOrderIso (by rw [hi])).toEquiv
+    (h : T₁.tensor = 𝓣.mapIso (Fin.castOrderIso (by simp [IndexList.length, hi])).toEquiv
-    (index_eq_colorMap_eq hi) T₂.tensor) : T₁ = T₂ := by
+    (colormap_mapIso hi.symm) T₂.tensor) : T₁ = T₂ := by
   cases T₁; cases T₂
+  simp at h
+  simp_all
   simp at hi
   subst hi
   simp_all
 
-lemma index_eq_of_eq {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ = T₂) : T₁.index = T₂.index := by
+
+lemma index_eq_of_eq {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ = T₂) :
+    T₁.toColorIndexList = T₂.toColorIndexList := by
   cases h
   rfl
 
 @[simp]
 lemma tensor_eq_of_eq {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ = T₂) : T₁.tensor =
     𝓣.mapIso (Fin.castOrderIso (by rw [index_eq_of_eq h])).toEquiv
-    (index_eq_colorMap_eq (index_eq_of_eq h)) T₂.tensor := by
+    (colormap_mapIso (index_eq_of_eq h).symm) T₂.tensor := by
   have hi := index_eq_of_eq h
   cases T₁
   cases T₂
@@ -78,10 +89,10 @@ lemma tensor_eq_of_eq {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ = T₂) : T₁.te
 
 /-- 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)
+def mkDualMap (T : 𝓣.Tensor cn) (l : ColorIndexList 𝓣.toTensorColor) (hn : n = l.1.length)
     (hd : ColorMap.DualMap l.1.colorMap (cn ∘ Fin.cast hn.symm)) :
     𝓣.TensorIndex where
-  index := l
+  toColorIndexList := l
   tensor :=
       𝓣.mapIso (Equiv.refl _) (ColorMap.DualMap.split_dual' (by simp [hd])) <|
       𝓣.dualize (ColorMap.DualMap.split l.1.colorMap (cn ∘ Fin.cast hn.symm)) <|