refactor: Index notation, computablity

HepLean/AnomalyCancellation/PureU1/BasisLinear.lean

@@ -76,9 +76,10 @@ lemma sum_of_vectors {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
     (∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) :=
   sum_of_anomaly_free_linear (fun i => f i) j
 
+/-! TODO: replace `Finsupp.equivFunOnFinite` here with `Finsupp.linearEquivFunOnFinite`. -/
 /-- The coordinate map for the basis. -/
 noncomputable
-def coordinateMap : ((PureU1 n.succ).LinSols) ≃ₗ[ℚ] Fin n →₀ ℚ where
+def coordinateMap : (PureU1 n.succ).LinSols ≃ₗ[ℚ] Fin n →₀ ℚ where
   toFun S := Finsupp.equivFunOnFinite.invFun (S.1 ∘ Fin.castSucc)
   map_add' S T := Finsupp.ext (congrFun rfl)
   map_smul' a S := Finsupp.ext (congrFun rfl)

HepLean/SpaceTime/LorentzTensor/Basic.lean

@@ -308,6 +308,10 @@ def mapIso {c : 𝓣.ColorMap X} {d : 𝓣.ColorMap Y} (e : X ≃ Y) (h : c.MapI
   (PiTensorProduct.reindex R _ e) ≪≫ₗ
   (PiTensorProduct.congr (fun y => 𝓣.colorModuleCast (by rw [h]; simp)))
 
+lemma mapIso_ext {c : 𝓣.ColorMap X} {d : 𝓣.ColorMap Y} (e e' : X ≃ Y)  (h : c.MapIso e d)
+    (h' : c.MapIso e' d) (he : e = e') : 𝓣.mapIso e h = 𝓣.mapIso e' h' := by
+  simp [he]
+
 @[simp]
 lemma mapIso_trans (e : X ≃ Y) (e' : Y ≃ Z) (h : cX.MapIso e cY) (h' : cY.MapIso e' cZ) :
     (𝓣.mapIso e h ≪≫ₗ 𝓣.mapIso e' h') = 𝓣.mapIso (e.trans e') (h.trans h') := by

HepLean/SpaceTime/LorentzTensor/EinsteinNotation/Basic.lean

@@ -6,6 +6,8 @@ Authors: Joseph Tooby-Smith
 import Mathlib.LinearAlgebra.StdBasis
 import HepLean.SpaceTime.LorentzTensor.Basic
 import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic
+import Mathlib.LinearAlgebra.DirectSum.Finsupp
+import Mathlib.LinearAlgebra.Finsupp
 /-!
 
 # Einstein notation for real tensors
@@ -28,8 +30,8 @@ instance : Fintype einsteinTensorColor.Color := Unit.fintype
 
 instance : DecidableEq einsteinTensorColor.Color := instDecidableEqPUnit
 
-variable {R : Type} [CommSemiring R]
 
+variable {R : Type} [CommSemiring R]
 
 /-- The `TensorStructure` associated with `n`-dimensional tensors. -/
 noncomputable def einsteinTensor (R : Type) [CommSemiring R] (n : ℕ) : TensorStructure R where
@@ -76,14 +78,37 @@ noncomputable def einsteinTensor (R : Type) [CommSemiring R] (n : ℕ) : TensorS
       simp only [tmul_zero]
       exact id (Ne.symm hi)
 
-instance : IndexNotation einsteinTensorColor.Color where
-  charList := {'ᵢ'}
-  notaEquiv :=
-    ⟨fun _ => ⟨'ᵢ', Finset.mem_singleton.mpr rfl⟩,
-    fun _ => Unit.unit,
-    fun _ => rfl,
-    by
-      intro c
-      have hc2 := c.2
-      simp only [↓Char.isValue, Finset.mem_singleton] at hc2
-      exact SetCoe.ext (id (Eq.symm hc2))⟩
+namespace einsteinTensor
+
+open TensorStructure
+
+noncomputable section
+
+instance : OfNat einsteinTensorColor.Color 0 := ⟨PUnit.unit⟩
+instance : OfNat (einsteinTensor R n).Color 0 := ⟨PUnit.unit⟩
+
+@[simp]
+lemma ofNat_inst_eq : @einsteinTensor.instOfNatColorOfNatNat R _ n =
+    einsteinTensor.instOfNatColorEinsteinTensorColorOfNatNat := rfl
+
+/-- A vector from an Einstein tensor with one index. -/
+def toVec : (einsteinTensor R n).Tensor ![Unit.unit] ≃ₗ[R] Fin n → R :=
+  PiTensorProduct.subsingletonEquiv 0
+
+/-- A matrix from an Einstein tensor with two indices. -/
+def toMatrix : (einsteinTensor R n).Tensor ![Unit.unit, Unit.unit] ≃ₗ[R] Matrix (Fin n) (Fin n) R :=
+  ((einsteinTensor R n).mapIso ((Fin.castOrderIso
+    (by rfl :  (Nat.succ 0).succ = Nat.succ 0 + Nat.succ 0)).toEquiv.trans
+      finSumFinEquiv.symm) (by funext x; fin_cases x; rfl; rfl)).trans <|
+  ((einsteinTensor R n).tensoratorEquiv ![0] ![0]).symm.trans <|
+  (TensorProduct.congr ((PiTensorProduct.subsingletonEquiv 0))
+    ((PiTensorProduct.subsingletonEquiv 0))).trans <|
+  (TensorProduct.congr (Finsupp.linearEquivFunOnFinite R R (Fin n)).symm
+    (Finsupp.linearEquivFunOnFinite R R (Fin n)).symm).trans <|
+  (finsuppTensorFinsupp' R (Fin n) (Fin n)).trans <|
+  (Finsupp.linearEquivFunOnFinite R R (Fin n × Fin n)).trans <|
+  (LinearEquiv.curry R (Fin n) (Fin n))
+
+end
+
+end einsteinTensor

HepLean/SpaceTime/LorentzTensor/EinsteinNotation/IndexNotation.lean

@@ -0,0 +1,131 @@
+/-
+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.TensorIndex
+import HepLean.SpaceTime.LorentzTensor.IndexNotation.IndexString
+import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.Basic
+/-!
+
+# Index notation for Einstein tensors
+
+
+-/
+
+instance : IndexNotation einsteinTensorColor.Color where
+  charList := {'ᵢ'}
+  notaEquiv :=
+    ⟨fun _ => ⟨'ᵢ', Finset.mem_singleton.mpr rfl⟩,
+    fun _ => Unit.unit,
+    fun _ => rfl,
+    by
+      intro c
+      have hc2 := c.2
+      simp only [↓Char.isValue, Finset.mem_singleton] at hc2
+      exact SetCoe.ext (id (Eq.symm hc2))⟩
+
+namespace einsteinTensor
+
+open einsteinTensorColor
+open IndexNotation IndexString
+open TensorStructure TensorIndex
+
+variable {R : Type} [CommSemiring R] {n m : ℕ}
+
+instance : IndexNotation (einsteinTensor R n).Color := instIndexNotationColorEinsteinTensorColor
+instance : DecidableEq (einsteinTensor R n).Color := instDecidableEqColorEinsteinTensorColor
+
+
+@[simp]
+lemma indexNotation_eq_color : @einsteinTensor.instIndexNotationColor R _ n =
+    instIndexNotationColorEinsteinTensorColor := by
+  rfl
+
+@[simp]
+lemma decidableEq_eq_color : @einsteinTensor.instDecidableEqColor R _ n  =
+    instDecidableEqColorEinsteinTensorColor := by
+  rfl
+
+@[simp]
+lemma einsteinTensor_color : (einsteinTensor R n).Color = einsteinTensorColor.Color := by
+  rfl
+
+@[simp]
+lemma toTensorColor_eq : (einsteinTensor R n).toTensorColor = einsteinTensorColor := by
+  rfl
+
+
+/-- The construction of a tensor index from a tensor and a string satisfying conditions
+  which can be automatically checked. This is a modified version of
+  `TensorStructure.TensorIndex.mkDualMap` specific to real Lorentz tensors. -/
+noncomputable def fromIndexStringColor {R : Type} [CommSemiring R]  {cn : Fin n → einsteinTensorColor.Color}
+    (T : (einsteinTensor R m).Tensor cn) (s : String)
+    (hs : listCharIsIndexString einsteinTensorColor.Color s.toList = true)
+    (hn : n = (toIndexList' s hs).length)
+    (hD : (toIndexList' s hs).withDual = (toIndexList' s hs).withUniqueDual)
+    (hC : IndexList.ColorCond.bool (toIndexList' s hs))
+    (hd : TensorColor.ColorMap.DualMap.boolFin'
+      (toIndexList' s hs).colorMap (cn ∘ Fin.cast hn.symm)) :
+    (einsteinTensor R m).TensorIndex :=
+  TensorStructure.TensorIndex.mkDualMap T ⟨(toIndexList' s hs), hD,
+      IndexList.ColorCond.iff_bool.mpr hC⟩ hn
+      (TensorColor.ColorMap.DualMap.boolFin'_DualMap hd)
+
+@[simp]
+lemma fromIndexStringColor_indexList {R : Type} [CommSemiring R] {cn : Fin n → einsteinTensorColor.Color}
+    (T : (einsteinTensor R m).Tensor cn) (s : String)
+    (hs : listCharIsIndexString einsteinTensorColor.Color s.toList = true)
+    (hn : n = (toIndexList' s hs).length)
+    (hD : (toIndexList' s hs).withDual = (toIndexList' s hs).withUniqueDual)
+    (hC : IndexList.ColorCond.bool (toIndexList' s hs))
+    (hd : TensorColor.ColorMap.DualMap.boolFin'
+      (toIndexList' s hs).colorMap (cn ∘ Fin.cast hn.symm)) :
+    (fromIndexStringColor T s hs hn hD hC hd).toIndexList = toIndexList' s hs := by
+  rfl
+
+
+/-- A tactic used to prove `boolFin` for real Lornetz tensors. -/
+macro "dualMapTactic" : tactic =>
+    `(tactic| {
+    simp only [toTensorColor_eq]
+    decide })
+
+
+/-- Notation for the construction of a tensor index from a tensor and a string.
+  Conditions are checked automatically. -/
+notation:20 T "|" S:21 => fromIndexStringColor T S
+  (by decide)
+  (by decide) (by decide)
+  (by decide)
+  (by dualMapTactic)
+
+/-- A tactics used to prove `colorPropBool` for real Lorentz tensors. -/
+macro "prodTactic" : tactic =>
+    `(tactic| {
+    apply (ColorIndexList.AppendCond.iff_bool _ _).mpr
+    change @ColorIndexList.AppendCond.bool einsteinTensorColor
+      instIndexNotationColorEinsteinTensorColor instDecidableEqColorEinsteinTensorColor _ _
+    simp only [prod_toIndexList, indexNotation_eq_color, fromIndexStringColor, mkDualMap,
+      toTensorColor_eq, decidableEq_eq_color]
+    decide})
+
+lemma mem_fin_list (n : ℕ) (i : Fin n) : i ∈ Fin.list n := by
+  have h1' : (Fin.list n)[i] = i := Fin.getElem_list _ _
+  exact h1' ▸ List.getElem_mem _ _ _
+
+instance (n : ℕ) (i : Fin n) : Decidable (i ∈ Fin.list n) :=
+  isTrue (mem_fin_list n i)
+
+
+
+/-- The product of Real Lorentz tensors. Conditions on indices are checked automatically. -/
+notation:10 T "⊗ᵀ" S:11 => TensorIndex.prod T S (by prodTactic)
+/-- An example showing the allowed constructions. -/
+example (T : (einsteinTensor R n).Tensor ![Unit.unit, Unit.unit]) : True := by
+  let _ := T|"ᵢ₂ᵢ₃"
+  let _ := T|"ᵢ₁ᵢ₂" ⊗ᵀ T|"ᵢ₂ᵢ₁"
+  let _ := T|"ᵢ₁ᵢ₂" ⊗ᵀ T|"ᵢ₂ᵢ₁" ⊗ᵀ T|"ᵢ₃ᵢ₄"
+  exact trivial
+
+end einsteinTensor

HepLean/SpaceTime/LorentzTensor/EinsteinNotation/lemmas.lean

@@ -0,0 +1,46 @@
+/-
+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.EinsteinNotation.IndexNotation
+/-!
+
+# Lemmas regarding Einstein tensors
+
+
+-/
+set_option profiler true
+namespace einsteinTensor
+
+open einsteinTensorColor
+open IndexNotation IndexString
+open TensorStructure TensorIndex
+
+variable {R : Type} [CommSemiring R] {n m : ℕ}
+
+/-! TODO: Fix notation here. -/
+set_option maxHeartbeats 0
+lemma swap_eq_transpose (T : (einsteinTensor R n).Tensor ![Unit.unit, Unit.unit]) :
+     (T|"ᵢ₁ᵢ₂") ≈ ((toMatrix.symm (toMatrix T).transpose)|"ᵢ₂ᵢ₁") := by
+  apply And.intro
+  apply And.intro
+  · simp only [toTensorColor_eq, indexNotation_eq_color, ColorIndexList.contr,
+      fromIndexStringColor_indexList, IndexList.contrIndexList_length]
+    decide
+  apply And.intro
+  · simp only [toTensorColor_eq, indexNotation_eq_color, ColorIndexList.contr,
+      fromIndexStringColor_indexList, IndexList.contrIndexList_length]
+    rw [IndexList.withUniqueDualInOther_eq_univ_iff_forall]
+    intro x
+    have h1 : (toIndexList' "ᵢ₁ᵢ₂" (by decide) : IndexList einsteinTensorColor.Color).contrIndexList.length
+      = 2 := by
+      decide
+    sorry
+
+
+
+  sorry
+
+end einsteinTensor

HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean

@@ -192,6 +192,24 @@ lemma ext (h : l.val = l2.val) : l = l2 := by
   cases l2
   simp_all
 
+def cons (i : Index X) : IndexList X := {val := i :: l.val}
+
+@[simp]
+lemma cons_val (i : Index X) : (l.cons i).val = i :: l.val := by
+  rfl
+
+@[simp]
+lemma cons_length (i : Index X) : (l.cons i).length = l.length + 1 := by
+  rfl
+
+def induction {P : IndexList X → Prop } (h_nil : P {val := ∅})
+  (h_cons : ∀ (x : Index X) (xs : IndexList X), P xs → P (xs.cons x)) (l : IndexList X) : P l := by
+  cases' l  with val
+  induction val with
+  | nil => exact h_nil
+  | cons x xs ih =>
+    exact h_cons x ⟨xs⟩ ih
+
 /-- The map of from `Fin s.numIndices` into colors associated to an index list. -/
 def colorMap : Fin l.length → X :=
   fun i => (l.val.get i).toColor

HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean

@@ -357,14 +357,32 @@ lemma contr_contr : l.contr.contr = l.contr := by
 @[simp]
 lemma contr_contr_idMap (i : Fin l.contr.contr.length) :
     l.contr.contr.idMap i = l.contr.idMap (Fin.cast (by simp) i) := by
-  simp [contr]
+  simp only [contr, contrIndexList_idMap, Fin.cast_trans]
   apply congrArg
-  simp [withoutDualEquiv]
+  simp only [withoutDualEquiv, RelIso.coe_fn_toEquiv, Finset.coe_orderIsoOfFin_apply,
+    EmbeddingLike.apply_eq_iff_eq]
   have h1 : l.contrIndexList.withoutDual = Finset.univ := by
     have hx := l.contrIndexList.withDual_union_withoutDual
     have hx2 := l.contrIndexList_withDual
     simp_all
-  simp [h1]
+  simp only [h1]
+  rw [orderEmbOfFin_univ]
+  rfl
+  rw [h1]
+  simp
+
+@[simp]
+lemma contr_contr_colorMap (i : Fin l.contr.contr.length) :
+    l.contr.contr.colorMap i = l.contr.colorMap (Fin.cast (by simp) i) := by
+  simp only [contr, contrIndexList_colorMap, Fin.cast_trans]
+  apply congrArg
+  simp only [withoutDualEquiv, RelIso.coe_fn_toEquiv, Finset.coe_orderIsoOfFin_apply,
+    EmbeddingLike.apply_eq_iff_eq]
+  have h1 : l.contrIndexList.withoutDual = Finset.univ := by
+    have hx := l.contrIndexList.withDual_union_withoutDual
+    have hx2 := l.contrIndexList_withDual
+    simp_all
+  simp only [h1]
   rw [orderEmbOfFin_univ]
   rfl
   rw [h1]

HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean

@@ -89,8 +89,10 @@ def dualEquiv : l.withDual ⊕ Fin l.withoutDual.card ≃ Fin l.length :=
 /-- The index list formed from `l` by selecting only those indices in `l` which
   do not have a dual. -/
 def contrIndexList : IndexList X where
-  val := (Fin.list l.withoutDual.card).map (fun i => l.val.get (l.withoutDualEquiv i).1)
+  val := List.ofFn (fun i => l.val.get (l.withoutDualEquiv i).1)
 
+def contrIndexList' : IndexList X where
+  val :=  l.val.filter (fun i => ¬ (l.val.any (fun j => i ≠ j ∧ i.id = j.id)))
 @[simp]
 lemma contrIndexList_length : l.contrIndexList.length = l.withoutDual.card := by
   simp [contrIndexList, withoutDual, length]
@@ -410,6 +412,18 @@ lemma withUniqueDualInOther_eq_univ_trans (h : l.withUniqueDualInOther l2 = Fins
   rw [← hs']
   exact Eq.symm (Option.eq_some_of_isSome hs)
 
+lemma withUniqueDualInOther_eq_univ_iff_forall :
+      l.withUniqueDualInOther l2 = Finset.univ ↔
+      ∀ (x : Fin l.length),
+      l.getDual? x = none ∧
+      (l.getDualInOther? l2 x).isSome = true ∧
+        ∀ (j : Fin l2.length), l.AreDualInOther l2 x j → some j = l.getDualInOther? l2 x := by
+  rw [Finset.eq_univ_iff_forall]
+  simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome,
+    Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, Finset.mem_filter, Finset.mem_univ,
+    true_and]
+
+
 end IndexList
 
 end IndexNotation

HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean

@@ -22,190 +22,6 @@ namespace IndexNotation
 
 variable (X : Type) [IndexNotation X] [Fintype X] [DecidableEq X]
 
-/-!
-
-## Lists of characters forming a string of indices.
-
--/
-
-/-- A lemma used to show terminiation of recursive definitions which follow.
-  It says that the length of `List.dropWhile _ l.tail` is less then the length of
-  `l` when `l` is non-empty. -/
-lemma dropWhile_isIndexSpecifier_length_lt (l : List Char) (hl : l ≠ []) :
-    (List.dropWhile (fun c => !isNotationChar X c) l.tail).length < l.length := by
-  let ld := l.tail.dropWhile (fun c => ¬ isNotationChar X c)
-  let lt := l.tail.takeWhile (fun c => ¬ isNotationChar X c)
-  simp only [gt_iff_lt]
-  have h2 : lt ++ ld = l.tail := by
-    exact List.takeWhile_append_dropWhile _ _
-  have h3 := congrArg List.length h2
-  rw [List.length_append] at h3
-  have h4 : l.length ≠ 0 := by
-    simp_all only [ne_eq, Bool.not_eq_true, Bool.decide_eq_false, List.takeWhile_append_dropWhile,
-      List.length_tail, List.length_eq_zero, not_false_eq_true]
-  have h5 : l.tail.length < l.length := by
-    rw [List.length_tail]
-    omega
-  have h6 : ld.length < l.length := by
-    omega
-  simpa [ld] using h6
-
-/-- The proposition for a list of characters to be an index string. -/
-def listCharIndexString (l : List Char) : Prop :=
-  if h : l = [] then True
-  else
-    let sfst := l.head h
-    if ¬ isNotationChar X sfst then False
-    else
-      let lt := l.tail.takeWhile (fun c => ¬ isNotationChar X c)
-      let ld := l.tail.dropWhile (fun c => ¬ isNotationChar X c)
-      if ¬ listCharIndexTail sfst lt then False
-      else listCharIndexString ld
-termination_by l.length
-decreasing_by
-  simpa [ld, InvImage] using dropWhile_isIndexSpecifier_length_lt X l h
-
-/-- A bool version of `listCharIndexString` for computation. -/
-def listCharIndexStringBool (l : List Char) : Bool :=
-  if h : l = [] then true
-  else
-    let sfst := l.head h
-    if ¬ isNotationChar X sfst then false
-    else
-      let lt := l.tail.takeWhile (fun c => ¬ isNotationChar X c)
-      let ld := l.tail.dropWhile (fun c => ¬ isNotationChar X c)
-      if ¬ listCharIndexTail sfst lt then false
-      else listCharIndexStringBool ld
-termination_by l.length
-decreasing_by
-  simpa [ld, InvImage] using dropWhile_isIndexSpecifier_length_lt X l h
-
-lemma listCharIndexString_iff (l : List Char) : listCharIndexString X l
-    ↔ (if h : l = [] then True else
-    let sfst := l.head h
-    if ¬ isNotationChar X sfst then False
-    else
-      let lt := l.tail.takeWhile (fun c => ¬ isNotationChar X c)
-      let ld := l.tail.dropWhile (fun c => ¬ isNotationChar X c)
-      if ¬ listCharIndexTail sfst lt then False
-      else listCharIndexString X ld) := by
-  rw [listCharIndexString]
-
-lemma listCharIndexString_iff_bool (l : List Char) :
-    listCharIndexString X l ↔ listCharIndexStringBool X l = true := by
-  rw [listCharIndexString, listCharIndexStringBool]
-  by_cases h : l = []
-  simp [h]
-  simp [h]
-  intro _ _
-  exact listCharIndexString_iff_bool _
-termination_by l.length
-decreasing_by
-  simpa [InvImage] using dropWhile_isIndexSpecifier_length_lt X l h
-
-instance : Decidable (listCharIndexString X l) :=
-  @decidable_of_decidable_of_iff _ _
-    ((listCharIndexStringBool X l).decEq true)
-      (listCharIndexString_iff_bool X l).symm
-
-/-!
-
-## Returning the chars of first index from chars of string of indices.
-
-In particular from a list of characters which form an index string,
-to a list of characters which forms an index.
-
--/
-
-/-- If a list of characters corresponds to an index string, then its head is an
-  index specifier. -/
-lemma listCharIndexString_head_isIndexSpecifier (l : List Char) (h : listCharIndexString X l)
-    (hl : l ≠ []) : isNotationChar X (l.head hl) := by
-  by_contra
-  rw [listCharIndexString] at h
-  simp_all only [↓reduceDIte, Bool.false_eq_true, not_false_eq_true, ↓reduceIte]
-
-/-- The tail of the first index in a list of characters corresponds to an index string
-  (junk on other lists). -/
-def listCharIndexStringHeadIndexTail (l : List Char) : List Char :=
-  l.tail.takeWhile (fun c => ¬ isNotationChar X c)
-
-/-- The tail of the first index in a list of characters corresponds to an index string
-  is the tail of a list of characters corresponding to an index specified by the head. -/
-lemma listCharIndexStringHeadIndexTail_listCharIndexTail (l : List Char)
-    (h : listCharIndexString X l) (hl : l ≠ []) :
-    listCharIndexTail (l.head hl) (listCharIndexStringHeadIndexTail X l) := by
-  by_contra
-  have h1 := listCharIndexString_head_isIndexSpecifier X l h hl
-  rw [listCharIndexString] at h
-  simp_all only [not_true_eq_false, Bool.not_eq_true, Bool.decide_eq_false, ite_not, if_false_right,
-    ite_false, dite_false]
-  obtain ⟨left, _⟩ := h
-  rename_i x _
-  simp [listCharIndexStringHeadIndexTail] at x
-  simp_all only [Bool.false_eq_true]
-
-/-- The first list of characters which form a index, from a list of characters
-  which form a string of indices. -/
-def listCharIndexStringHeadIndex (l : List Char) : List Char :=
-  if h : l = [] then []
-  else l.head h :: listCharIndexStringHeadIndexTail X l
-
-lemma listCharIndexStringHeadIndex_listCharIndex (l : List Char) (h : listCharIndexString X l) :
-    listCharIndex X (listCharIndexStringHeadIndex X l) := by
-  by_cases h1 : l = []
-  · subst h1
-    simp [listCharIndex, listCharIndexStringHeadIndex]
-  · simp [listCharIndexStringHeadIndex, listCharIndex, h1]
-    apply And.intro
-    exact listCharIndexString_head_isIndexSpecifier X l h h1
-    exact listCharIndexStringHeadIndexTail_listCharIndexTail X l h h1
-
-/-!
-
-## Dropping chars of first index from chars of string of indices.
-
--/
-
-/-- The list of characters obtained by dropping the first block which
-  corresponds to an index. -/
-def listCharIndexStringDropHeadIndex (l : List Char) : List Char :=
-  l.tail.dropWhile (fun c => ¬ isNotationChar X c)
-
-lemma listCharIndexStringDropHeadIndex_listCharIndexString (l : List Char)
-    (h : listCharIndexString X l) :
-    listCharIndexString X (listCharIndexStringDropHeadIndex X l) := by
-  by_cases h1 : l = []
-  · subst h1
-    simp [listCharIndexStringDropHeadIndex, listCharIndexString]
-  · simp [listCharIndexStringDropHeadIndex, h1]
-    rw [listCharIndexString] at h
-    simp_all only [↓reduceDIte, Bool.not_eq_true, Bool.decide_eq_false, ite_not, if_false_right,
-      if_false_left, Bool.not_eq_false]
-
-/-!
-
-## Chars of all indices from char of string of indices
-
--/
-
-/-- Given a list list of characters corresponding to an index string, the list
-  of lists of characters which correspond to an index and are non-zero corresponding
-  to that index string. -/
-def listCharIndexStringTolistCharIndex (l : List Char) (h : listCharIndexString X l) :
-    List ({lI : List Char // listCharIndex X lI ∧ lI ≠ []}) :=
-  if hl : l = [] then [] else
-    ⟨listCharIndexStringHeadIndex X l, by
-      apply And.intro (listCharIndexStringHeadIndex_listCharIndex X l h)
-      simp [listCharIndexStringHeadIndex]
-      exact hl⟩ ::
-    (listCharIndexStringTolistCharIndex (listCharIndexStringDropHeadIndex X l)
-        (listCharIndexStringDropHeadIndex_listCharIndexString X l h))
-termination_by l.length
-decreasing_by
-  rename_i h1
-  simpa [InvImage, listCharIndexStringDropHeadIndex] using
-    dropWhile_isIndexSpecifier_length_lt X l hl
 
 /-!
 
@@ -213,8 +29,17 @@ decreasing_by
 
 -/
 
+def stringToPreIndexList (l : List Char) : List (List Char) :=
+  let indexHeads := l.filter (fun c => isNotationChar X c)
+  let indexTails := l.splitOnP (fun c => isNotationChar X c)
+  let l' := List.zip indexHeads indexTails.tail
+  l'.map fun x => x.1 :: x.2
+
+def listCharIsIndexString (l : List Char) : Bool :=
+  (stringToPreIndexList X l).all fun l => (listCharIndex X l && l ≠ [])
+
 /-- A string of indices to be associated with a tensor. For example, `ᵘ⁰ᵤ₂₆₀ᵘ³`. -/
-def IndexString : Type := {s : String // listCharIndexStringBool X s.toList = true}
+def IndexString : Type := {s : String // listCharIsIndexString X s.toList = true}
 
 namespace IndexString
 
@@ -229,18 +54,22 @@ variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X]
 /-- The character list associated with a index string. -/
 def toCharList (s : IndexString X) : List Char := s.val.toList
 
-/-- The char list of an index string satisfies `listCharIndexString`. -/
-lemma listCharIndexString (s : IndexString X) : listCharIndexString X s.toCharList := by
-  rw [listCharIndexString_iff_bool]
-  exact s.prop
+/-! TODO: Move. -/
+def charListToOptionIndex (l : List Char) : Option (Index X) :=
+  if h : listCharIndex X l && l ≠ [] then
+    some (Index.ofCharList l (by simpa using h))
+  else
+    none
 
 /-- The indices associated to an index string. -/
 def toIndexList (s : IndexString X) : IndexList X :=
-  {val := (listCharIndexStringTolistCharIndex X s.toCharList (listCharIndexString s)).map
-    fun x => Index.ofCharList x.1 x.2}
+  {val :=
+    (stringToPreIndexList X s.toCharList).filterMap fun l => charListToOptionIndex l}
+
+
 
 /-- The formation of an index list from a string `s` statisfying `listCharIndexStringBool`. -/
-def toIndexList' (s : String) (hs : listCharIndexStringBool X s.toList = true) : IndexList X :=
+def toIndexList' (s : String) (hs : listCharIsIndexString X s.toList = true) : IndexList X :=
   toIndexList ⟨s, hs⟩
 
 end IndexString
@@ -264,7 +93,7 @@ open IndexNotation ColorIndexList IndexString
 /-- The construction of a tensor index from a tensor and a string satisfing conditions which are
   easy to check automatically. -/
 noncomputable def fromIndexString (T : 𝓣.Tensor cn) (s : String)
-    (hs : listCharIndexStringBool 𝓣.toTensorColor.Color s.toList = true)
+    (hs : listCharIsIndexString 𝓣.toTensorColor.Color s.toList = true)
     (hn : n = (toIndexList' s hs).length)
     (hD : (toIndexList' s hs).withDual = (toIndexList' s hs).withUniqueDual)
     (hC : IndexList.ColorCond (toIndexList' s hs))

HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean

@@ -62,6 +62,13 @@ namespace ContrPerm
 
 variable {l l' l2 l3 : ColorIndexList 𝓒}
 
+lemma of_perm (h : l.contr.val.Perm l'.contr.val) : l.ContrPerm l' := by
+  apply And.intro
+  exact List.Perm.length_eq h
+  apply And.intro
+  sorry
+  sorry
+
 @[symm]
 lemma symm (h : ContrPerm l l') : ContrPerm l' l := by
   rw [ContrPerm] at h ⊢
@@ -85,16 +92,16 @@ lemma trans (h1 : ContrPerm l l2) (h2 : ContrPerm l2 l3) : ContrPerm l l3 := by
   funext i
   simp only [Function.comp_apply]
   have h1' := congrFun h1.2.2 ⟨i, by simp [h1.2.1]⟩
-  simp at h1'
+  simp only [Function.comp_apply] at h1'
   rw [← h1']
   have h2' := congrFun h2.2.2 ⟨
     ↑((l.contr.getDualInOtherEquiv l2.contr.toIndexList) ⟨↑i, by simp [h1.2.1]⟩), by simp [h2.2.1]⟩
-  simp at h2'
+  simp only [Function.comp_apply] at h2'
   rw [← h2']
   apply congrArg
   simp only [getDualInOtherEquiv, Equiv.coe_fn_mk]
   rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff]
-  simp [AreDualInOther]
+  simp only [AreDualInOther, getDualInOther?_id]
   rw [h2.2.1]
   simp
 
@@ -108,8 +115,8 @@ lemma contr_self : ContrPerm l l.contr := by
   simp only [contr_contr, true_and]
   have h1 := @refl _ _ l
   apply And.intro h1.2.1
-  erw [contr_contr]
-  exact h1.2.2
+  rw [show l.contr.contr = l.contr by simp]
+  simp only [getDualInOtherEquiv_self_refl, Equiv.coe_refl, CompTriple.comp_eq]
 
 @[simp]
 lemma self_contr : ContrPerm l.contr l := by

HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean

@@ -269,6 +269,9 @@ lemma rel_contr (T : 𝓣.TensorIndex) : T ≈ T.contr := by
     Fin.symm_castOrderIso, mapIso_mapIso]
   trans 𝓣.mapIso (Equiv.refl _) (by rfl) T.contr.tensor
   simp only [contr_toColorIndexList, mapIso_refl, LinearEquiv.refl_apply]
+  apply congrFun
+  apply congrArg
+  apply congrArg
   rfl
 
 lemma smul_equiv {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ ≈ T₂) (r : R) : r • T₁ ≈ r • T₂ := by
@@ -424,15 +427,15 @@ lemma add_comm {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) : T₁ +[h
   simp only [contr_toColorIndexList, add_toColorIndexList, contr_add_tensor, add_tensor,
     addCondEquiv, map_add, mapIso_mapIso, colorMap', contrPermEquiv_symm]
   rw [_root_.add_comm]
-  congr 1
+  apply Mathlib.Tactic.LinearCombination.add_pf
   · apply congrFun
     apply congrArg
-    congr 1
+    apply mapIso_ext
     rw [← contrPermEquiv_self_contr, ← contrPermEquiv_self_contr, contrPermEquiv_trans,
       contrPermEquiv_trans]
   · apply congrFun
     apply congrArg
-    congr 1
+    apply mapIso_ext
     rw [← contrPermEquiv_self_contr, ← contrPermEquiv_self_contr, contrPermEquiv_trans,
       contrPermEquiv_trans]
 
@@ -442,7 +445,7 @@ lemma add_rel_left {T₁ T₁' T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂)
   apply And.intro ContrPerm.refl
   intro h
   simp only [contr_add_tensor, add_tensor, map_add]
-  congr 1
+  apply Mathlib.Tactic.LinearCombination.add_pf
   rw [h'.to_eq]
   simp only [contr_toColorIndexList, add_toColorIndexList, colorMap', addCondEquiv,
     contrPermEquiv_symm, mapIso_mapIso, contrPermEquiv_trans, contrPermEquiv_refl, Equiv.refl_symm,
@@ -463,10 +466,20 @@ lemma add_assoc' {T₁ T₂ T₃ : 𝓣.TensorIndex} {h' : AddCond T₂ T₃} (h
   simp only [add_toColorIndexList, add_tensor, contr_toColorIndexList, addCondEquiv,
     contr_add_tensor, map_add, mapIso_mapIso]
   rw [_root_.add_assoc]
-  congr
-  rw [← contrPermEquiv_self_contr, ← contrPermEquiv_self_contr]
-  rw [contrPermEquiv_trans, contrPermEquiv_trans, contrPermEquiv_trans]
-  erw [← contrPermEquiv_self_contr, contrPermEquiv_trans]
+  apply Mathlib.Tactic.LinearCombination.add_pf
+  · apply congrFun
+    apply congrArg
+    apply mapIso_ext
+    rw [← contrPermEquiv_self_contr, ← contrPermEquiv_self_contr]
+    rw [contrPermEquiv_trans, contrPermEquiv_trans, contrPermEquiv_trans]
+  · apply Mathlib.Tactic.LinearCombination.add_pf
+    apply congrFun
+    apply congrArg
+    apply mapIso_ext
+    rw [← contrPermEquiv_self_contr, contrPermEquiv_trans, ← contrPermEquiv_self_contr,
+      contrPermEquiv_trans, contrPermEquiv_trans]
+    rfl
+
 
 open AddCond in
 lemma add_assoc {T₁ T₂ T₃ : 𝓣.TensorIndex} {h' : AddCond T₁ T₂} (h : AddCond (T₁ +[h'] T₂) T₃) :

HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean

@@ -45,6 +45,8 @@ instance : IndexNotation realTensorColor.Color where
 namespace realLorentzTensor
 
 open realTensorColor
+open IndexNotation IndexString
+open TensorStructure TensorIndex
 
 variable {d : ℕ}
 
@@ -69,10 +71,6 @@ lemma realLorentzTensor_color : (realLorentzTensor d).Color = realTensorColor.Co
 lemma toTensorColor_eq : (realLorentzTensor d).toTensorColor = realTensorColor := by
   rfl
 
-open IndexNotation IndexString
-
-open TensorStructure TensorIndex
-
 /-- The construction of a tensor index from a tensor and a string satisfying conditions
   which can be automatically checked. This is a modified version of
   `TensorStructure.TensorIndex.mkDualMap` specific to real Lorentz tensors. -/

HepLean/SpaceTime/LorentzTensor/RisingLowering.lean

@@ -68,6 +68,16 @@ lemma boolFin_DualMap {c₁ c₂ : 𝓒.ColorMap (Fin n)} (h : boolFin c₁ c₂
     apply List.getElem_mem
   exact h x (h2 _)
 
+def boolFin' (c₁ c₂ : 𝓒.ColorMap (Fin n)) : Bool :=
+  ∀ (i : Fin n), 𝓒.colorQuot (c₁ i) = 𝓒.colorQuot (c₂ i)
+
+lemma boolFin'_DualMap {c₁ c₂ : 𝓒.ColorMap (Fin n)} (h : boolFin' c₁ c₂ = true) :
+    DualMap c₁ c₂ := by
+  simp [boolFin'] at h
+  simp [DualMap]
+  funext x
+  exact h x
+
 lemma refl : DualMap c₁ c₁ := by
   simp [DualMap]