diff --git a/Physlib.lean b/Physlib.lean
index d8e7ea52a..f2e70fd4f 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -404,9 +404,12 @@ public import Physlib.Relativity.Tensors.Conjugation.Basic
 public import Physlib.Relativity.Tensors.Constructors
 public import Physlib.Relativity.Tensors.Contraction.Basic
 public import Physlib.Relativity.Tensors.Contraction.Basis
+public import Physlib.Relativity.Tensors.Contraction.CrossToEnd
+public import Physlib.Relativity.Tensors.Contraction.CrossToSlot
 public import Physlib.Relativity.Tensors.Contraction.Products
 public import Physlib.Relativity.Tensors.Contraction.Pure
 public import Physlib.Relativity.Tensors.Contraction.SuccSuccAbove
+public import Physlib.Relativity.Tensors.Contraction.UnitTensorContraction
 public import Physlib.Relativity.Tensors.Dual
 public import Physlib.Relativity.Tensors.Elab
 public import Physlib.Relativity.Tensors.Evaluation
diff --git a/Physlib/Relativity/Tensors/Basic.lean b/Physlib/Relativity/Tensors/Basic.lean
index fad9622ff..2b73a5e67 100644
--- a/Physlib/Relativity/Tensors/Basic.lean
+++ b/Physlib/Relativity/Tensors/Basic.lean
@@ -628,6 +628,12 @@ lemma permT_eq_zero_iff {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
   funext x
   simp [IsReindexing.inv_apply_apply]
 
+/-- `permT` is injective. -/
+lemma permT_injective {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
+    {σ : Fin m → Fin n} (h : IsReindexing c c1 σ) :
+    Function.Injective (permT (S := S) σ h) :=
+  (injective_iff_map_eq_zero' _).mpr (permT_eq_zero_iff h)
+
 /-!
 ## field
 -/
diff --git a/Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean b/Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean
new file mode 100644
index 000000000..2878a66b6
--- /dev/null
+++ b/Physlib/Relativity/Tensors/Contraction/CrossToEnd.lean
@@ -0,0 +1,387 @@
+/-
+Copyright (c) 2026 Andrea Pari. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrea Pari
+-/
+module
+
+public import Physlib.Relativity.Tensors.Contraction.Products
+/-!
+
+# Cross contraction at named slots
+
+## i. Overview
+
+`contrT` contracts two slots of a single tensor. Contracting a slot of one tensor against a slot of
+another (`T^{μν} u_ν`, `g_{μν} v^ν`) is `prodT` then `contrT`, which leaves every call site to
+locate the two post-product slots and discharge the distinctness and `τ`-duality goals.
+
+`crossToEnd i j hc` performs that contraction at named slots `i` and `j`, with
+`hc : S.τ (cA i) = cB j` recording their `τ`-duality. The output color is
+`Fin.append (cA ∘ i.succAbove) (cB ∘ j.succAbove)`: every slot of `cA` except `i`, in order, then
+every slot of `cB` except `j`. These are the survivors. Any slot is reachable:
+`crossToEnd 2 0 _ R u` reads as `R_{μνρσ} u^ρ`. The survivors are appended rather than interleaved,
+and appending is associative, so both bracketings of a chain produce the same survivor list in the
+same order.
+
+The complementary convention keeps the replacement index in place. Contracting slot `1` of
+`![c₀, c₁, c₂, c₃]` against a rank-two `![S.τ c₁, d]` gives `![c₀, c₂, c₃, d]` here and
+`![c₀, d, c₂, c₃]` there; that operation is `crossToSlot`, built on this substrate in
+`Physlib.Relativity.Tensors.Contraction.CrossToSlot`.
+
+## ii. Key results
+
+- `TensorSpecies.Tensor.crossToEnd` : the slot-addressed cross contraction.
+- `TensorSpecies.Tensor.crossToEnd_two` : at rank two on each factor, a plain `contrT` of the
+    product on slots `1, 2`.
+- `TensorSpecies.Tensor.crossToEnd_equivariant` : the contraction commutes with the `G`-action.
+- `TensorSpecies.Tensor.crossToEnd_assoc_rankTwo` : rebracket the chain
+    `A —(iA·0)— B —(last·0)— C` at rank-two `B` and `C`, up to `permT id`. Not full associativity.
+- `TensorSpecies.Tensor.crossToEnd_permT_left` / `crossToEnd_permT_right` : move a relabelling of
+    the left or right factor through the contraction, the contracted slot moving with it.
+
+## iii. Table of contents
+
+- A. Slot-addressed cross contraction
+- B. Equivariance
+- C. Rebracketing the metric chain
+- D. Permutation commutators
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace TensorSpecies
+
+variable {k : Type} [CommRing k] {C : Type} {G : Type} [Group G]
+    {V : C → Type} [∀ c, AddCommGroup (V c)] [∀ c, Module k (V c)]
+    {basisIdx : C → Type} [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)]
+    {rep : (c : C) → Representation k G (V c)} {b : (c : C) → Module.Basis (basisIdx c) k (V c)}
+    {S : TensorSpecies k C G V basisIdx rep b}
+
+namespace Tensor
+
+open Fin
+
+/-!
+
+## A. Slot-addressed cross contraction
+
+-/
+
+/-- Slot-addressed cross contraction: contract slot `i` of `t1` against slot `j` of `t2`. The
+  survivors are `t1`'s slots except `i` followed by `t2`'s slots except `j`, so the output color is
+  a clean `Fin (nA + nB) → C` and a chain composes without recasts. -/
+noncomputable def crossToEnd {nA nB : ℕ} {cA : Fin (nA + 1) → C} {cB : Fin (nB + 1) → C}
+    (i : Fin (nA + 1)) (j : Fin (nB + 1)) (hc : S.τ (cA i) = cB j) :
+    Tensor S cA →ₗ[k] Tensor S cB →ₗ[k]
+      Tensor S (Fin.append (cA ∘ i.succAbove) (cB ∘ j.succAbove)) :=
+  LinearMap.compr₂ prodT <|
+    permT id
+      (by
+        refine ⟨Function.bijective_id, fun m => ?_⟩
+        simp only [id_eq, Function.comp_apply]
+        refine Fin.addCases (fun a => ?_) (fun a => ?_) m
+        · rw [Fin.succSuccAbove_castAdd_natAdd_apply_castAdd i j a]
+          simp only [Fin.append_left, Function.comp_apply]
+        · rw [Fin.succSuccAbove_castAdd_natAdd_apply_natAdd i j a]
+          simp only [Fin.append_right, Function.comp_apply]) ∘ₗ
+    contrT (nA + nB)
+      (Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega) (Fin.castAdd (nB + 1) i))
+      (Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega) (Fin.natAdd (nA + 1) j))
+      (by
+        refine ⟨Fin.ne_of_val_ne ?_, ?_⟩
+        · simp only [Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd]; omega
+        · simp only [Function.comp_apply, Fin.cast_cast, Fin.cast_eq_self,
+            Fin.append_left, Fin.append_right]
+          exact hc) ∘ₗ
+    permT (Fin.cast (show (nA + nB) + 1 + 1 = (nA + 1) + (nB + 1) by omega))
+      (IsReindexing.fin_cast_isReindexing _ _ (by omega))
+
+/-- Cross-contracting the last slot of a rank-2 tensor `A` with the `0`-slot of a rank-2 tensor `B`
+  is a plain `contrT` of their product on the middle slots `1, 2`, up to a color recast. Discharging
+  the slot arithmetic once lets a `contrT`-level identity lift to `crossToEnd` by one rewrite. -/
+lemma crossToEnd_two {cA cB : Fin 2 → C} (h : S.τ (cA (Fin.last 1)) = cB 0)
+    (A : Tensor S cA) (B : Tensor S cB) :
+    crossToEnd (Fin.last 1) (0 : Fin 2) h A B
+      = permT (id : Fin 2 → Fin 2) (IsReindexing.on_id.mpr (fun i => by fin_cases i <;> rfl))
+          (contrT 2 (1 : Fin 4) (2 : Fin 4)
+            (by
+              refine ⟨by decide, ?_⟩
+              rw [show (1 : Fin 4) = Fin.castAdd 2 (1 : Fin 2) from rfl,
+                  show (2 : Fin 4) = Fin.natAdd 2 (0 : Fin 2) from rfl,
+                  Fin.append_left, Fin.append_right]
+              exact h)
+            (prodT A B)) := by
+  simp only [crossToEnd, LinearMap.compr₂_apply, LinearMap.comp_apply]
+  rw [contrT_permT, contrT_congr (n := 2) 1 2 _ (by rfl) (by rfl)]
+  simp only [permT_permT, CompTriple.comp_eq]
+  refine permT_congr ?_ rfl
+  ext i
+  fin_cases i <;> rfl
+
+/-!
+
+## B. Equivariance
+
+`crossToEnd i j hc` is the curried bilinear map `LinearMap.compr₂ prodT` post-composed with the
+linear `permT`/`contrT` factors, so additivity, scalar multiplication, and finite sums in either
+argument are already the generic `map_add`/`map_smul`/`map_sum` and need no lemmas of their own.
+
+-/
+
+/-- Cross contraction is `G`-equivariant, each of `prodT`, `contrT` and `permT` being so. -/
+@[simp]
+lemma crossToEnd_equivariant {nA nB : ℕ} {cA : Fin (nA + 1) → C} {cB : Fin (nB + 1) → C}
+    (i : Fin (nA + 1)) (j : Fin (nB + 1)) (hc : S.τ (cA i) = cB j) (g : G)
+    (t1 : Tensor S cA) (t2 : Tensor S cB) :
+    crossToEnd i j hc (g • t1) (g • t2) = g • crossToEnd i j hc t1 t2 := by
+  simp only [crossToEnd, LinearMap.compr₂_apply, LinearMap.comp_apply, prodT_equivariant,
+    contrT_equivariant, permT_equivariant]
+
+/-!
+
+## C. Rebracketing the metric chain
+
+Both bracketings reduce to one product contracted at its two seams in opposite order, then drop to
+the pure-tensor level, so the seam permutation never crosses a contraction under `whnf`;
+`Pure.permP_dropPair_dropPair_congr` closes the step.
+
+-/
+
+/-- Rebracket the chain `A —(iA·0)— B —(last·0)— C` for rank-two `B` and `C`: contracting `A·B`
+  first and then `·C` equals contracting `B·C` first and then `A·`, up to the color recast
+  `permT id`.
+
+  Not full associativity: only `A`'s attachment slot `iA` is free. `B`'s rank two is what makes the
+  statement possible, the second contraction being addressed at `Fin.last nA`, the slot `B`'s unique
+  survivor occupies in `A·B`. Other slots are reached by conjugating with the `permT` commutators.
+
+  With `A := T`, `B := g`, `C := g⁻¹` this reassociates `(T·g)·g⁻¹` to `T·(g·g⁻¹)`, after which
+  `g·g⁻¹` collapses to the unit tensor: the step behind raising then lowering a named index. -/
+lemma crossToEnd_assoc_rankTwo {nA : ℕ}
+    {cA : Fin (nA + 1) → C} {cB cC : Fin 2 → C}
+    (iA : Fin (nA + 1))
+    (hc1 : S.τ (cA iA) = cB 0)
+    (hc2 : S.τ (cB (Fin.last 1)) = cC 0)
+    (tA : Tensor S cA) (tB : Tensor S cB) (tC : Tensor S cC) :
+    crossToEnd (Fin.last nA) 0
+        (by
+          rw [show (Fin.last nA : Fin (nA + 1)) = Fin.natAdd nA (Fin.last 0) from
+              Fin.ext (by simp), Fin.append_right, Function.comp_apply, Fin.succAbove_zero,
+            Fin.succ_last]
+          exact hc2)
+        (crossToEnd iA 0 hc1 tA tB) tC =
+      permT id
+        (IsReindexing.on_id.mpr fun i => by
+          refine Fin.addCases (fun a => ?_) (fun a => ?_) i
+          · simp only [Fin.append_left, Function.comp_apply, Fin.succAbove_last,
+              show a.castSucc = Fin.castAdd 1 a from rfl, Fin.append_left]
+          · simp only [Fin.append_right, Function.comp_apply, Fin.succAbove_zero]
+            fin_cases a
+            rfl)
+        (crossToEnd iA 0
+          (by
+            rw [show (0 : Fin (1 + 1)) = Fin.castAdd 1 (0 : Fin 1) from rfl, Fin.append_left,
+              Function.comp_apply, Fin.succAbove_last, Fin.castSucc_zero]
+            exact hc1)
+          tA
+          (crossToEnd (Fin.last 1) 0 hc2 tB tC)) := by
+  simp only [crossToEnd, LinearMap.compr₂_apply, LinearMap.comp_apply, permT_permT]
+  conv_rhs => rw [prodT_permT_right, prodT_contrT_snd]
+  conv_lhs => rw [prodT_permT_left, prodT_contrT_fst]
+  rw [prodT_swap tC, prodT_permT_left]
+  conv_rhs => rw [prodT_permT_right, prodT_assoc' tA tB tC]
+  simp only [permT_permT]
+  generalize (prodT (prodT tA tB) tC) = X
+  conv_lhs => rw [contrT_permT]
+  conv_rhs => rw [contrT_permT]
+  simp only [permT_permT]
+  conv_lhs => rw [contrT_permT]
+  conv_rhs => rw [contrT_permT]
+  simp only [permT_permT]
+  conv_rhs => rw [contrT_permT]
+  simp only [permT_permT]
+  apply induction_on_pure (t := X)
+  · intro p
+    simp only [contrT_pure, permT_pure, Pure.contrP, map_smul]
+    rw [smul_smul, smul_smul]
+    -- Index-map facts used only by this proof, kept local rather than exported. They are `clear`ed
+    -- before the closing `grind`, which would otherwise ingest them as candidate facts.
+    have happend_swap_val : ∀ (n n2 : ℕ) (x : Fin (n2 + n)),
+        (Fin.append (Fin.natAdd n) (Fin.castAdd n2) x).val =
+          if x.val < n2 then n + x.val else x.val - n2 := by
+      intro n n2 x
+      refine Fin.addCases (fun i => ?_) (fun i => ?_) x
+      · simp [Fin.append_left]
+      · simp [Fin.append_right]
+    have happend_castAdd_cast : ∀ (na nb n2 : ℕ) (heq : na = nb),
+        Fin.append (Fin.castAdd n2 ∘ Fin.cast heq) (Fin.natAdd nb) =
+          Fin.cast (show na + n2 = nb + n2 by omega) := by
+      intro na nb n2 heq
+      subst heq
+      simpa using Fin.append_castAdd_natAdd_eq_id
+    have happend_natAdd_cast : ∀ (na nb n2 : ℕ) (heq : na = nb),
+        Fin.append (Fin.castAdd nb) (Fin.natAdd n2 ∘ Fin.cast heq) =
+          Fin.cast (show n2 + na = n2 + nb by omega) := by
+      intro na nb n2 heq
+      subst heq
+      simpa using Fin.append_castAdd_natAdd_eq_id
+    apply congrArg₂ (fun r t => r • t)
+    · -- Coefficients.
+      simp only [Pure.contrPCoeff_dropPair]
+      rw [mul_comm]
+      apply congrArg₂ (fun x y : k => x * y)
+      all_goals apply Pure.contrPCoeff_congr p
+      all_goals apply Fin.ext
+      all_goals
+        simp only [Nat.add_eq, Function.id_comp, Function.comp_id, Function.comp_apply,
+          Fin.cast_castAdd_left, Fin.cast_natAdd_left,
+          Fin.funPredPredAbove, Fin.succSuccAbove_predPredAbove,
+          Fin.append_right, happend_swap_val,
+          Fin.append_castAdd_natAdd_eq_id, id_eq, happend_castAdd_cast,
+          happend_natAdd_cast, Fin.succSuccAbove_val, Fin.val_castAdd,
+          Fin.val_natAdd, Fin.val_last, Fin.val_cast, Fin.val_zero]
+        split_ifs <;> omega
+    · -- Slot maps.
+      apply congrArg Pure.toTensor
+      apply Pure.permP_dropPair_dropPair_congr p
+      intro m
+      -- The `funPredPredAbove` layers are nested, so they must be peeled one at a time; one
+      -- combined `simp` set thrashes `whnf` instead.
+      iterate 3
+        try simp only [Function.comp_apply, id_eq]
+        try simp only [Fin.funPredPredAbove]
+        try simp only [Fin.succSuccAbove_predPredAbove]
+      apply Fin.ext
+      -- Pinning a block injection to a literal slot `⟨v, _⟩` is stated at `Fin` level, not at
+      -- `.val` level, so that a rewrite replaces the composite before `Fin.succSuccAbove_val`
+      -- builds its `ite` conditions on it, keeping the generated `Decidable` instances in sync.
+      have hcast_castAdd : ∀ {n m N : ℕ} (h : n + m = N) {i : Fin n} {v : ℕ} (hv : i.val = v),
+          Fin.cast h (Fin.castAdd m i) = ⟨v, by have := i.isLt; omega⟩ := by
+        intro n m N h i v hv
+        exact Fin.ext (by simp [hv])
+      have hcast_natAdd : ∀ {n m N : ℕ} (h : n + m = N) {i : Fin m} {v : ℕ} (hv : n + i.val = v),
+          Fin.cast h (Fin.natAdd n i) = ⟨v, by have := i.isLt; omega⟩ := by
+        intro n m N h i v hv
+        exact Fin.ext (by simp [hv])
+      -- Pin each slot to a literal `⟨v, _⟩`, innermost first, so that `succSuccAbove_val` fires.
+      rw [hcast_castAdd (i := Fin.last nA) (v := nA) _ rfl,
+        hcast_natAdd (n := nA + 1) (i := (0 : Fin (1 + 1))) (v := nA + 1) _
+          (by simp only [Fin.val_zero, Nat.add_zero]),
+        hcast_castAdd (i := iA) (v := (iA : ℕ)) _ rfl,
+        Fin.natAdd_mk (1 + 1) (iA : ℕ),
+        Fin.natAdd_mk (1 + 1) (nA + 1),
+        hcast_castAdd (i := Fin.last 1) (v := 1) _ rfl,
+        hcast_natAdd (n := 1 + 1) (i := (0 : Fin (1 + 1))) (v := 1 + 1) _
+          (by simp only [Fin.val_zero, Nat.add_zero]),
+        Fin.natAdd_mk (nA + 1) 1,
+        Fin.natAdd_mk (nA + 1) (1 + 1)]
+      simp only [Function.comp_id]
+      rw [Fin.append_castAdd_natAdd_eq_id]
+      simp only [Nat.add_eq, id_eq, happend_swap_val, happend_castAdd_cast,
+        happend_natAdd_cast, Fin.succSuccAbove_val, Fin.val_cast]
+      -- Four nested reinsertion conditionals; the split budget is `SuccSuccAbove`'s. The spent
+      -- index-map hypotheses are dropped first: `grind` ingests the local context, and leaving
+      -- them in costs it more than twice the elaboration time.
+      clear happend_swap_val happend_castAdd_cast happend_natAdd_cast hcast_castAdd hcast_natAdd
+      grind (splits := 20)
+  · intro r t ht; simp only [map_smul, ht]
+  · intro t1 t2 h1 h2; simp only [map_add, h1, h2]
+
+/-!
+
+## D. Permutation commutators
+
+Moving a relabelling of one factor through the slot-addressed contraction. The relabelling `σ` need
+not fix the contracted slot, so it carries the contraction from slot `i` to slot `σ i` and restricts
+to the survivors as a map `σ'` filling the square `(σ i).succAbove ∘ σ' = σ ∘ i.succAbove`. Taking
+`σ'` as an argument rather than deriving it lets a caller supply the survivor map it wants (`id`, a
+swap-induced map) instead of an opaque composite.
+
+-/
+
+/-- Left commutator: contracting slot `i` of `permT σ t1` equals contracting slot `σ i` of `t1`,
+  then relabelling the survivors by `σ'`. The square `hσ'` records how `σ'` carries the complement
+  of `i` to the complement of `σ i`, and implies its bijectivity. -/
+lemma crossToEnd_permT_left {nA nB : ℕ} {cA cA' : Fin (nA + 1) → C}
+    {cB : Fin (nB + 1) → C}
+    (i : Fin (nA + 1)) (j : Fin (nB + 1))
+    (σ : Fin (nA + 1) → Fin (nA + 1)) (σ' : Fin nA → Fin nA)
+    (hσ : IsReindexing cA cA' σ)
+    (hσ' : (σ i).succAbove ∘ σ' = σ ∘ i.succAbove)
+    (hc : S.τ (cA' i) = cB j)
+    (t1 : Tensor S cA) (t2 : Tensor S cB) :
+    crossToEnd i j hc (permT σ hσ t1) t2 =
+      permT (Fin.append (Fin.castAdd nB ∘ σ') (Fin.natAdd nA))
+        (IsReindexing.append_congr_left (cB ∘ j.succAbove)
+          (IsReindexing.succAbove_of_succAbove_eq i hσ hσ'))
+        (crossToEnd (σ i) j (by rw [hσ.2 i]; exact hc) t1 t2) := by
+  simp only [crossToEnd, LinearMap.compr₂_apply, LinearMap.comp_apply]
+  rw [prodT_permT_left]
+  simp only [permT_permT]
+  generalize prodT t1 t2 = X
+  apply induction_on_pure (t := X)
+  · intro p
+    simp only [contrT_pure, permT_pure, Pure.contrP, map_smul]
+    congr 1
+    · simp only [Pure.contrPCoeff_permP]
+      apply Pure.contrPCoeff_congr <;> (apply Fin.ext; simp)
+    · apply congrArg Pure.toTensor
+      apply Pure.permP_dropPair_permP_congr p
+      intro m
+      simp only [Function.comp_apply, id_eq]
+      refine Fin.addCases (fun a => ?_) (fun b => ?_) m
+      · rw [Fin.succSuccAbove_castAdd_natAdd_apply_castAdd i j a, Fin.append_left,
+          Function.comp_apply, Fin.append_left, Function.comp_apply,
+          Fin.succSuccAbove_castAdd_natAdd_apply_castAdd (σ i) j _,
+          show (σ i).succAbove (σ' a) = σ (i.succAbove a) from congrFun hσ' a]
+      · rw [Fin.succSuccAbove_castAdd_natAdd_apply_natAdd i j b, Fin.append_right,
+          Fin.append_right, Fin.succSuccAbove_castAdd_natAdd_apply_natAdd (σ i) j b]
+  · intro r t ht; simp only [map_smul, ht]
+  · intro t1 t2 h1 h2; simp only [map_add, h1, h2]
+
+/-- Right commutator, the mirror of `crossToEnd_permT_left`: contracting slot `j` of `permT σ t2`
+  equals contracting slot `σ j` of `t2`, then relabelling the survivors by `σ'`. -/
+lemma crossToEnd_permT_right {nA nB : ℕ} {cA : Fin (nA + 1) → C}
+    {cB cB' : Fin (nB + 1) → C}
+    (i : Fin (nA + 1)) (j : Fin (nB + 1))
+    (σ : Fin (nB + 1) → Fin (nB + 1)) (σ' : Fin nB → Fin nB)
+    (hσ : IsReindexing cB cB' σ)
+    (hσ' : (σ j).succAbove ∘ σ' = σ ∘ j.succAbove)
+    (hc : S.τ (cA i) = cB' j)
+    (t1 : Tensor S cA) (t2 : Tensor S cB) :
+    crossToEnd i j hc t1 (permT σ hσ t2) =
+      permT (Fin.append (Fin.castAdd nB) (Fin.natAdd nA ∘ σ'))
+        (IsReindexing.append_congr_right (cA ∘ i.succAbove)
+          (IsReindexing.succAbove_of_succAbove_eq j hσ hσ'))
+        (crossToEnd i (σ j) (by rw [hσ.2 j]; exact hc) t1 t2) := by
+  simp only [crossToEnd, LinearMap.compr₂_apply, LinearMap.comp_apply]
+  rw [prodT_permT_right]
+  simp only [permT_permT]
+  generalize prodT t1 t2 = X
+  apply induction_on_pure (t := X)
+  · intro p
+    simp only [contrT_pure, permT_pure, Pure.contrP, map_smul]
+    congr 1
+    · simp only [Pure.contrPCoeff_permP]
+      apply Pure.contrPCoeff_congr <;> (apply Fin.ext; simp)
+    · apply congrArg Pure.toTensor
+      apply Pure.permP_dropPair_permP_congr p
+      intro m
+      simp only [Function.comp_apply, id_eq]
+      refine Fin.addCases (fun a => ?_) (fun b => ?_) m
+      · rw [Fin.succSuccAbove_castAdd_natAdd_apply_castAdd i j a, Fin.append_left,
+          Fin.append_left, Fin.succSuccAbove_castAdd_natAdd_apply_castAdd i (σ j) a]
+      · rw [Fin.succSuccAbove_castAdd_natAdd_apply_natAdd i j b, Fin.append_right,
+          Function.comp_apply, Fin.append_right, Function.comp_apply,
+          Fin.succSuccAbove_castAdd_natAdd_apply_natAdd i (σ j) _,
+          show (σ j).succAbove (σ' b) = σ (j.succAbove b) from congrFun hσ' b]
+  · intro r t ht; simp only [map_smul, ht]
+  · intro t1 t2 h1 h2; simp only [map_add, h1, h2]
+
+end Tensor
+
+end TensorSpecies
diff --git a/Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean b/Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean
new file mode 100644
index 000000000..c91c25763
--- /dev/null
+++ b/Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean
@@ -0,0 +1,151 @@
+/-
+Copyright (c) 2026 Andrea Pari. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrea Pari
+-/
+module
+
+public import Physlib.Relativity.Tensors.Contraction.CrossToEnd
+/-!
+
+# Result-to-slot contraction against a rank-2 tensor
+
+## i. Overview
+
+`crossToEnd` deposits the surviving index of a slot contraction at the end of the survivor list.
+Raising and lowering a named index instead wants the replacement to stay *in place*: contracting
+slot `i` of `t` against a rank-2 tensor `M` (a metric, the unit tensor) should return `t` with only
+slot `i`'s color changed, `T^{μ}{}_{νρ} ↦ T_{μνρ}`. `crossToSlot i j hc M` is that operation, and
+`crossToSlot_eq_crossToEnd` is the one place the two conventions meet.
+
+This module stays at the `CommRing` altitude of `crossToEnd`; the `RCLike` round trips built on the
+operation live with the unit-tensor collapse theory in
+`Physlib.Relativity.Tensors.Contraction.UnitTensorContraction`.
+
+## ii. Key results
+
+- `TensorSpecies.Tensor.crossToSlot` : contract slot `i` against slot `j` of a rank-2 tensor and
+    rotate the survivor back into position `i`; raising and lowering a named index.
+- `TensorSpecies.Tensor.crossToSlot_eq_crossToEnd` : the bridge to the result-to-end convention.
+- `TensorSpecies.Tensor.crossToSlotInv` : the returning half of a round trip, the contraction
+    against the second factor with the round trip's color cast absorbed.
+- `TensorSpecies.Tensor.crossToSlot_permT_right_id` : an identity reindexing of the rank-2 tensor
+    passes through the contraction.
+- `TensorSpecies.Tensor.crossToSlot_equivariant` : the contraction commutes with the `G`-action.
+
+## iii. Table of contents
+
+- A. The result-to-slot contraction
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace TensorSpecies
+
+variable {k : Type} [CommRing k] {C : Type} {G : Type} [Group G]
+    {V : C → Type} [∀ c, AddCommGroup (V c)] [∀ c, Module k (V c)]
+    {basisIdx : C → Type} [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)]
+    {rep : (c : C) → Representation k G (V c)} {b : (c : C) → Module.Basis (basisIdx c) k (V c)}
+    {S : TensorSpecies k C G V basisIdx rep b}
+
+namespace Tensor
+
+/-!
+
+## A. The result-to-slot contraction
+
+-/
+
+/-- The survivor color of `crossToEnd i j` against a rank-2 tensor of color `cM` is `c` with
+  slot `i` replaced by the surviving color `cM (j.succAbove 0)`, once the survivors are rotated
+  back by the inverse of the cycle `[i, last]`. -/
+lemma IsReindexing.crossToSlot_cycle {nA : ℕ} {c : Fin (nA + 1) → C} {cM : Fin 2 → C}
+    (i : Fin (nA + 1)) (j : Fin 2) :
+    IsReindexing
+      (Fin.append (c ∘ i.succAbove) (cM ∘ j.succAbove))
+      (Function.update c i (cM (j.succAbove 0)))
+      ⇑(Fin.cycleIcc i (Fin.last nA)).symm := by
+  refine ⟨(Fin.cycleIcc i (Fin.last nA)).symm.bijective, fun y => ?_⟩
+  obtain ⟨z, rfl⟩ : ∃ z, y = Fin.cycleIcc i (Fin.last nA) z :=
+    ⟨_, (Equiv.apply_symm_apply _ _).symm⟩
+  rw [Equiv.symm_apply_apply, ← Fin.append_succAbove_const_eq_cycleIcc i]
+  refine Fin.addCases (fun a => ?_) (fun a => ?_) z
+  · rw [Fin.append_left, Fin.append_left, Function.comp_apply,
+      Function.update_of_ne (Fin.succAbove_ne i a)]
+  · rw [Fin.append_right, Fin.append_right, Function.comp_apply, Function.update_self]
+    fin_cases a
+    rfl
+
+/-- Contract slot `i` of `t` against slot `j` of the rank-2 tensor `M`, whose `j`-slot color must
+  equal the dual color `τ (c i)` (propositionally, via `hc`), and rotate `M`'s surviving slot back
+  into position `i`. The result is `t` with slot `i` relabelled to `M`'s surviving color.
+
+  This is raising and lowering a named index; the metric case is `j = 0`,
+  `M = metricTensor (τ (c i))`. Because `hc` is propositional, a rank-2 tensor whose slot color
+  matches only up to an equality enters directly, with no transport. -/
+noncomputable def crossToSlot {nA : ℕ} {c : Fin (nA + 1) → C} {cM : Fin 2 → C}
+    (i : Fin (nA + 1)) (j : Fin 2) (hc : S.τ (c i) = cM j) (M : S.Tensor cM) :
+    S.Tensor c →ₗ[k] S.Tensor (Function.update c i (cM (j.succAbove 0))) :=
+  permT ⇑(Fin.cycleIcc i (Fin.last nA)).symm (IsReindexing.crossToSlot_cycle i j) ∘ₗ
+    (crossToEnd i j hc).flip M
+
+/-- The bridge between the two conventions: `crossToSlot i j hc M t` is `crossToEnd i j hc t M`
+  with the survivor rotated from the last slot back to slot `i` by the inverse cycle. -/
+lemma crossToSlot_eq_crossToEnd {nA : ℕ} {c : Fin (nA + 1) → C} {cM : Fin 2 → C}
+    (i : Fin (nA + 1)) (j : Fin 2) (hc : S.τ (c i) = cM j) (M : S.Tensor cM) (t : S.Tensor c) :
+    crossToSlot i j hc M t =
+      permT ⇑(Fin.cycleIcc i (Fin.last nA)).symm (IsReindexing.crossToSlot_cycle i j)
+        (crossToEnd i j hc t M) := rfl
+
+/-- Contract slot `i` of a tensor whose color there is `d` against `M'`, then absorb the color cast
+  the two `Function.update`s generate, landing back on `c`. This is the returning half of a
+  raise-then-lower round trip; absorbing the cast here is what keeps the round trip cast-free at
+  both ends. -/
+noncomputable def crossToSlotInv {nA : ℕ} {c : Fin (nA + 1) → C} {b d e : C} (i : Fin (nA + 1))
+    (he : c i = e) (hb : S.τ d = b) (M' : S.Tensor ![b, e]) :
+    S.Tensor (Function.update c i d) →ₗ[k] S.Tensor c :=
+  permT (id : Fin (nA + 1) → Fin (nA + 1))
+      (IsReindexing.on_id_symm (IsReindexing.update_update_of_eq (d := d) i he)) ∘ₗ
+    crossToSlot i (0 : Fin 2)
+      (by rw [Function.update_self]; exact hb : S.τ (Function.update c i d i) = b) M'
+
+/-- An identity reindexing of the rank-2 tensor becomes the corresponding identity reindexing of
+  the contracted output: the `crossToSlot`-level case of `crossToEnd_permT_right` where the rank-2
+  tensor's colors are only propositionally recast. -/
+lemma crossToSlot_permT_right_id {nA : ℕ} {c : Fin (nA + 1) → C} {cM cM' : Fin 2 → C}
+    (i : Fin (nA + 1)) (j : Fin 2) (hc : S.τ (c i) = cM' j)
+    (M : Tensor S cM) (hM : IsReindexing cM cM' (id : Fin 2 → Fin 2)) (t : Tensor S c) :
+    crossToSlot i j hc (permT (id : Fin 2 → Fin 2) hM M) t =
+      permT (id : Fin (nA + 1) → Fin (nA + 1))
+        (IsReindexing.on_id.mpr (fun a => by
+          by_cases ha : a = i
+          · subst ha
+            simpa using hM.2 (j.succAbove 0)
+          · simp [Function.update_of_ne ha]))
+        (crossToSlot i j (hc.trans (hM.2 j).symm) M t) := by
+  rw [crossToSlot_eq_crossToEnd, crossToSlot_eq_crossToEnd]
+  rw [crossToEnd_permT_right i j
+    (id : Fin 2 → Fin 2) id hM (by rfl)]
+  simp only [permT_permT]
+  apply permT_congr
+  · funext x
+    simpa only [Function.comp_apply, Function.comp_id, id_eq] using
+      congrFun Fin.append_castAdd_natAdd_eq_id ((Fin.cycleIcc i (Fin.last nA)).symm x)
+  · rfl
+
+/-- Cross contraction into a slot is `G`-equivariant, both constituents (`crossToEnd`, `permT`)
+  being so. -/
+@[simp]
+lemma crossToSlot_equivariant {nA : ℕ} {c : Fin (nA + 1) → C} {cM : Fin 2 → C}
+    (i : Fin (nA + 1)) (j : Fin 2) (hc : S.τ (c i) = cM j) (g : G)
+    (M : Tensor S cM) (t : Tensor S c) :
+    crossToSlot i j hc (g • M) (g • t) = g • crossToSlot i j hc M t := by
+  rw [crossToSlot_eq_crossToEnd, crossToSlot_eq_crossToEnd, crossToEnd_equivariant,
+    permT_equivariant]
+
+end Tensor
+
+end TensorSpecies
diff --git a/Physlib/Relativity/Tensors/Contraction/Products.lean b/Physlib/Relativity/Tensors/Contraction/Products.lean
index 0d95a6abb..3ccc999bf 100644
--- a/Physlib/Relativity/Tensors/Contraction/Products.lean
+++ b/Physlib/Relativity/Tensors/Contraction/Products.lean
@@ -153,6 +153,23 @@ lemma contrT_prodT_snd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
   rw [prodT_contrT_snd]
   simp
 
+/-- A contraction internal to the left factor commutes past the outer product with a right
+  spectator. The mirror of `prodT_contrT_snd`, obtained from it by `prodT_swap`, so the right-hand
+  side contracts the swapped product `prodT t1 t` and carries a block swap. -/
+lemma prodT_contrT_fst {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
+    {c1 : Fin n1 → C}
+    (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j)
+    (t : Tensor S c) (t1 : Tensor S c1) :
+    prodT (contrT n i j hij t) t1 =
+    permT _ IsReindexing.append_swap
+      (permT id (IsReindexing.append_succSuccAbove_natAdd i j) <|
+      contrT _
+        (Fin.natAdd n1 i)
+        (Fin.natAdd n1 j)
+        (by simpa using hij) <|
+      prodT t1 t) := by
+  rw [prodT_swap, prodT_contrT_snd]
+
 end Tensor
 
 end TensorSpecies
diff --git a/Physlib/Relativity/Tensors/Contraction/Pure.lean b/Physlib/Relativity/Tensors/Contraction/Pure.lean
index 87e256b57..8bd7bae9b 100644
--- a/Physlib/Relativity/Tensors/Contraction/Pure.lean
+++ b/Physlib/Relativity/Tensors/Contraction/Pure.lean
@@ -133,6 +133,60 @@ lemma dropPair_permP {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
   · simp [hσ.2]
   · simp [hσ.2]
 
+/-- Two `permP`–`dropPair`–`dropPair` towers over a common pure tensor agree once their composite
+  slot maps agree pointwise. Comparing two orders of dropping two pairs of slots this way keeps
+  every slot map an opaque variable, so the comparison closes by unification rather than by
+  `whnf`-reducing the color and index-map composites. -/
+lemma permP_dropPair_dropPair_congr {nP nOut : ℕ}
+    {c : Fin (nP + 1 + 1 + 1 + 1) → C} {cOut : Fin nOut → C} (p : Pure S c)
+    (aL bL : Fin (nP + 1 + 1 + 1 + 1)) (habL : aL ≠ bL)
+    (a2L b2L : Fin (nP + 1 + 1)) (hab2L : a2L ≠ b2L)
+    (σ1L : Fin nOut → Fin nP)
+    (h1L : IsReindexing ((c ∘ Fin.succSuccAbove aL bL) ∘ Fin.succSuccAbove a2L b2L) cOut σ1L)
+    (aR bR : Fin (nP + 1 + 1 + 1 + 1)) (habR : aR ≠ bR)
+    (a2R b2R : Fin (nP + 1 + 1)) (hab2R : a2R ≠ b2R)
+    (σ1R : Fin nOut → Fin nP)
+    (h1R : IsReindexing ((c ∘ Fin.succSuccAbove aR bR) ∘ Fin.succSuccAbove a2R b2R) cOut σ1R)
+    (hslot : ∀ m : Fin nOut,
+      Fin.succSuccAbove aL bL (Fin.succSuccAbove a2L b2L (σ1L m)) =
+      Fin.succSuccAbove aR bR (Fin.succSuccAbove a2R b2R (σ1R m))) :
+    permP σ1L h1L (dropPair a2L b2L hab2L (dropPair aL bL habL p)) =
+    permP σ1R h1R (dropPair a2R b2R hab2R (dropPair aR bR habR p)) := by
+  funext m
+  simp only [permP, dropPair]
+  exact congr_mid (cOut m) p _ _ (hslot m) (h1L.preserve_color m).symm
+    (h1R.preserve_color m).symm
+
+/-- Two `permP`–`dropPair`–`permP` towers over a common pure tensor agree once their composite
+  slot maps agree pointwise. The one-contraction, inner-relabelled sibling of
+  `permP_dropPair_dropPair_congr`. -/
+lemma permP_dropPair_permP_congr {nP nOut mL mR : ℕ}
+    {c : Fin nP → C} {cL : Fin (mL + 1 + 1) → C} {cR : Fin (mR + 1 + 1) → C}
+    {cOut : Fin nOut → C} (p : Pure S c)
+    (σ0L : Fin (mL + 1 + 1) → Fin nP) (h0L : IsReindexing c cL σ0L)
+    (aL bL : Fin (mL + 1 + 1)) (habL : aL ≠ bL)
+    (σ1L : Fin nOut → Fin mL)
+    (h1L : IsReindexing (cL ∘ Fin.succSuccAbove aL bL) cOut σ1L)
+    (σ0R : Fin (mR + 1 + 1) → Fin nP) (h0R : IsReindexing c cR σ0R)
+    (aR bR : Fin (mR + 1 + 1)) (habR : aR ≠ bR)
+    (σ1R : Fin nOut → Fin mR)
+    (h1R : IsReindexing (cR ∘ Fin.succSuccAbove aR bR) cOut σ1R)
+    (hslot : ∀ m : Fin nOut,
+      σ0L (Fin.succSuccAbove aL bL (σ1L m)) = σ0R (Fin.succSuccAbove aR bR (σ1R m))) :
+    permP σ1L h1L (dropPair aL bL habL (permP σ0L h0L p)) =
+    permP σ1R h1R (dropPair aR bR habR (permP σ0R h0R p)) := by
+  funext m
+  simp only [permP, dropPair]
+  -- Each side is a two-`cast` tower, one cast from the inner `permP` and one from the outer
+  -- `permP`-after-`dropPair`. `LinearEquiv.cast` is defeq to `_root_.cast`, so drop to the plain
+  -- cast, fuse the tower with `cast_cast`, and close with the single-cast lemma `congr_mid`.
+  change _root_.cast _ (_root_.cast _ (p _)) =
+    _root_.cast _ (_root_.cast _ (p _))
+  simp only [_root_.cast_cast]
+  exact congr_mid (cOut m) p _ _ (hslot m)
+    ((h0L.2 _).trans (h1L.2 m))
+    ((h0R.2 _).trans (h1R.2 m))
+
 /-!
 
 ## Contraction coefficient
@@ -146,6 +200,16 @@ noncomputable def contrPCoeff {n : ℕ} {c : Fin n → C}
     (i j : Fin n) (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) : k :=
   S.contr (c i) (p i ⊗ₜ (LinearEquiv.cast (R := k) (by simp [hij.2]) (p j)))
 
+/-- `contrPCoeff` is insensitive to its proof arguments once the two contracted slots agree. Lets a
+  coefficient comparison rewrite the slots without a `congr` search through the proof fields. -/
+lemma contrPCoeff_congr {n : ℕ} {c : Fin n → C} (p : Pure S c)
+    {i i' j j' : Fin n} (hi : i = i') (hj : j = j')
+    {hij : i ≠ j ∧ S.τ (c i) = c j} {hij' : i' ≠ j' ∧ S.τ (c i') = c j'} :
+    p.contrPCoeff i j hij = p.contrPCoeff i' j' hij' := by
+  subst hi
+  subst hj
+  rfl
+
 attribute [-simp] LinearEquiv.cast_apply
 
 @[simp]
diff --git a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean
index d5e1a0a6d..0f8af30f1 100644
--- a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean
+++ b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean
@@ -231,6 +231,38 @@ lemma succSuccAbove_natAdd_apply_castAdd {n n1 : ℕ}
   simp only [Fin.ext_iff, succSuccAbove_val, natAdd, castAdd]
   grind (splits := 20)
 
+/-- Reinserting a left-block survivor `a` after removing the `i`-th slot of the left block and the
+  `j`-th slot of the right block of `Fin ((nA + 1) + (nB + 1))`, the removal read at the contracted
+  length `(nA + nB) + 1 + 1`. Unlike `succSuccAbove_natAdd_apply_castAdd` the two holes straddle the
+  two blocks, so the statement carries the reshaping `Fin.cast`s. -/
+lemma succSuccAbove_castAdd_natAdd_apply_castAdd {nA nB : ℕ} (i : Fin (nA + 1)) (j : Fin (nB + 1))
+    (a : Fin nA) :
+    Fin.cast (show (nA + nB) + 1 + 1 = (nA + 1) + (nB + 1) by omega)
+        ((Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega)
+            (Fin.castAdd (nB + 1) i)).succSuccAbove
+          (Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega)
+            (Fin.natAdd (nA + 1) j)) (Fin.castAdd nB a))
+      = Fin.castAdd (nB + 1) (i.succAbove a) := by
+  apply Fin.ext
+  simp only [Fin.succSuccAbove_val, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd,
+    Fin.succAbove, Fin.lt_def, Fin.val_castSucc, Fin.val_succ, apply_ite Fin.val]
+  split_ifs <;> omega
+
+/-- Reinserting a right-block survivor, the mirror of
+  `Fin.succSuccAbove_castAdd_natAdd_apply_castAdd`. -/
+lemma succSuccAbove_castAdd_natAdd_apply_natAdd {nA nB : ℕ} (i : Fin (nA + 1)) (j : Fin (nB + 1))
+    (a : Fin nB) :
+    Fin.cast (show (nA + nB) + 1 + 1 = (nA + 1) + (nB + 1) by omega)
+        ((Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega)
+            (Fin.castAdd (nB + 1) i)).succSuccAbove
+          (Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega)
+            (Fin.natAdd (nA + 1) j)) (Fin.natAdd nA a))
+      = Fin.natAdd (nA + 1) (j.succAbove a) := by
+  apply Fin.ext
+  simp only [Fin.succSuccAbove_val, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, Fin.succAbove,
+    Fin.lt_def, Fin.val_castSucc, Fin.val_succ, apply_ite Fin.val]
+  split_ifs <;> omega
+
 lemma succSuccAbove_natAdd_image_range_castAdd {n n1 : ℕ}
     (i j : Fin (n + 1 + 1)) :
     (succSuccAbove (n := n1 + n) (Fin.natAdd n1 i) (Fin.natAdd n1 j)) ''
diff --git a/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean b/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean
new file mode 100644
index 000000000..2ea6cfc18
--- /dev/null
+++ b/Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean
@@ -0,0 +1,395 @@
+/-
+Copyright (c) 2026 Andrea Pari. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrea Pari
+-/
+module
+
+public import Physlib.Relativity.Tensors.Contraction.CrossToSlot
+public import Physlib.Relativity.Tensors.UnitTensor
+public import Physlib.Relativity.Tensors.Evaluation
+/-!
+
+# Contraction against the unit tensor
+
+## i. Overview
+
+The unit tensor is the identity for slot contraction: contracting any slot of `t` against
+`unitTensor` for that slot's color returns `t`, the slot relabelled to the survivor tail. That is
+what collapses "raise then lower" to the identity, a metric contracted against its dual becoming
+the unit tensor and then contracting away.
+
+`crossToEnd_unitTensor` is proved by decomposing `t` along its last slot (`eq_sum_evalT`) and
+transporting to an arbitrary slot with the transposition `swap i (last)`. On it the round trip
+against a matched pair is assembled in both conventions, and a pair collapsing in *both* orders
+makes the two contractions mutually inverse, which `crossToSlotEquiv` bundles as a linear
+equivalence between the two color assignments.
+
+Since `unitTensor` is `RCLike`-valued, this material sits over an `[RCLike k]` variable block, apart
+from the `CommRing` `crossToEnd`/`crossToSlot` algebra.
+
+## ii. Key results
+
+- `TensorSpecies.Tensor.crossToEnd_unitTensor` : the unit tensor is an identity for `crossToEnd`
+    at any named slot.
+- `TensorSpecies.Tensor.crossToEnd_round_trip_of_unit_slot` : two contractions against a pair that
+    collapses to the unit tensor return the original tensor, in result-to-end form.
+- `TensorSpecies.Tensor.crossToSlot_raise_lower_round_trip` : the round trip in result-to-slot
+    form, every color propositional.
+- `TensorSpecies.Tensor.crossToSlotEquiv` : raising and lowering a named index against a pair that
+    collapses in both orders, as a linear equivalence.
+
+## iii. Table of contents
+
+- A. The unit tensor as a slot-contraction identity
+- B. Round trips against a matched pair
+- C. Raising and lowering as an equivalence
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace TensorSpecies
+
+variable {k : Type} [RCLike k] {C : Type} {G : Type} [Group G]
+    {V : C → Type} [∀ c, AddCommGroup (V c)] [∀ c, Module k (V c)]
+    {basisIdx : C → Type} [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)]
+    {rep : (c : C) → Representation k G (V c)} {b : (c : C) → Module.Basis (basisIdx c) k (V c)}
+    {S : TensorSpecies k C G V basisIdx rep b}
+attribute [-simp] LinearEquiv.cast_apply
+
+namespace Tensor
+
+/-!
+
+## A. The unit tensor as a slot-contraction identity
+
+Contracting a named slot against `unitTensor` returns the tensor unchanged, the slot carried to the
+survivor tail by `move_last`.
+
+-/
+
+/-- Cross-contracting the last slot of the product `E ⊗ B` (with `B` rank one) against the unit
+  tensor for that slot's color returns `E ⊗ B` unchanged, the contracted slot carried to the end.
+  The rank-one spectator case that seeds `crossToEnd_unitTensor_slot`. -/
+private lemma crossToEnd_prodT_unitTensor {nV : ℕ} {cE : Fin nV → C} {cB : C}
+    (E : Tensor S cE) (B : Tensor S ![cB]) :
+    crossToEnd (Fin.last nV) (0 : Fin 2)
+        (by rw [show (Fin.last nV : Fin (nV + 1)) = Fin.natAdd nV 0 from Fin.ext (by simp)]; simp :
+          S.τ ((Fin.append cE ![cB]) (Fin.last nV)) = ![S.τ cB, cB] 0)
+        (prodT E B) (unitTensor cB) =
+      permT id (IsReindexing.on_id.mpr (fun i => by
+        refine Fin.addCases (fun j => ?_) (fun j => ?_) i
+        · simp only [Fin.append_left, Function.comp_apply, Fin.succAbove_last]
+          exact (Fin.append_left cE ![cB] j).symm
+        · simp only [Fin.append_right, Function.comp_apply, Fin.succAbove_zero]
+          fin_cases j
+          rfl)) (prodT E B) := by
+  simp only [crossToEnd, LinearMap.compr₂_apply, LinearMap.comp_apply]
+  rw [contrT_congr (n := nV + 1) (⟨nV, by omega⟩ : Fin (nV + 1 + 1 + 1))
+      (⟨nV + 1, by omega⟩ : Fin (nV + 1 + 1 + 1)) _ (Fin.ext (by simp)) (Fin.ext (by simp))]
+  rw [prodT_assoc E B (unitTensor cB)]
+  simp only [permT_permT]
+  rw [contrT_permT]
+  simp only [Fin.cast_eq_self, Function.comp_apply]
+  have hij : (0 : Fin 3) ≠ (1 : Fin 3) ∧
+      S.τ (Fin.append ![cB] ![S.τ cB, cB] 0) = Fin.append ![cB] ![S.τ cB, cB] 1 :=
+    ⟨by decide, by rfl⟩
+  have key : (contrT (nV + 1) (⟨nV, by omega⟩ : Fin (nV + 1 + 1 + 1)) ⟨nV + 1, by omega⟩
+        (by refine ⟨by simp [Fin.ext_iff], ?_⟩
+            rw [show (⟨nV, by omega⟩ : Fin (nV + 1 + 1 + 1))
+                    = Fin.natAdd nV (0 : Fin 3) from Fin.ext (by simp),
+                show (⟨nV + 1, by omega⟩ : Fin (nV + 1 + 1 + 1))
+                    = Fin.natAdd nV (1 : Fin 3) from Fin.ext (by simp)]
+            rw [Fin.append_right, Fin.append_right]; exact hij.2)
+        (prodT E (prodT B (unitTensor cB)))) =
+      (permT id (IsReindexing.on_id_symm (IsReindexing.append_succSuccAbove_natAdd (0:Fin 3) 1)))
+        (prodT E (contrT 1 0 1 hij (prodT B (unitTensor cB)))) :=
+    contrT_prodT_snd (0 : Fin 3) 1 hij (prodT B (unitTensor cB)) E
+  rw [contrT_single_unitTensor] at key
+  -- The `contrT_congr` pinning leaves slot proofs that match `key`'s only at `instances`
+  -- transparency; the trailing `permT_permT` needs the full `erw`.
+  rw (transparency := .instances) [key, permT_permT]
+  rw [prodT_permT_right, permT_permT]
+  erw [permT_permT]
+  apply permT_congr
+  · funext i
+    simp only [Function.comp_apply, id_eq, Fin.funPredPredAbove]
+    apply Fin.ext
+    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, CompTriple.comp_eq,
+      Fin.cast_eq_self, Fin.predPredAbove_succSuccAbove]
+    refine Fin.addCases (fun j => ?_) (fun j => ?_) i <;> simp [Fin.append_left, Fin.append_right]
+  · rfl
+
+/-- The boundary case of `crossToEnd_unitTensor`, proved by spectator decomposition along the last
+  slot (`eq_sum_evalT`). The last slot is threaded as a variable `i` with `hilast : i = last nA` so
+  that `crossToEnd_unitTensor` can apply it at the image of `i` under its transposition without a
+  dependent rewrite of the slot index. -/
+private lemma crossToEnd_unitTensor_slot {nA : ℕ} {cA : Fin (nA + 1) → C} {c : C}
+    {i : Fin (nA + 1)} (hilast : i = Fin.last nA) (hc : cA i = c) (t1 : Tensor S cA) :
+    crossToEnd i (0 : Fin 2) (by simp [hc] : S.τ (cA i) = ![S.τ c, c] 0) t1 (unitTensor c) =
+      permT (Fin.append i.succAbove (fun _ : Fin 1 => i)) (IsReindexing.move_last i hc) t1 := by
+  subst hilast
+  subst hc
+  rw [eq_sum_evalT t1, map_sum, LinearMap.sum_apply, map_sum]
+  refine Finset.sum_congr rfl (fun i _ => ?_)
+  change crossToEnd (Fin.last nA) 0 _
+    (permT (fun x => x) _
+      (prodT (evalT (Fin.last nA) i t1)
+        (basis ![cA (Fin.last nA)] (ComponentIdx.single.symm i))))
+    (unitTensor (S := S) (cA (Fin.last nA))) = _
+  rw [crossToEnd_permT_left (Fin.last nA) 0 (fun x => x) (fun x => x)
+    (IsReindexing.append_succ_last cA) (by rfl)]
+  rw [crossToEnd_prodT_unitTensor]
+  simp only [permT_permT]
+  refine permT_congr (funext fun x => ?_) rfl
+  refine Fin.addCases (fun j => ?_) (fun j => ?_) x
+  · simp only [Fin.append_left, Function.comp_apply, id_eq, Fin.succAbove_last]
+    rfl
+  · simp only [Fin.append_right, Function.comp_apply]
+    exact Fin.ext (by simp)
+
+/-- Contracting slot `i` of `t1` against the unit tensor for that slot's color returns `t1`, the
+  contracted slot relabelled by `move_last i`. The unit tensor acts as an identity for `crossToEnd`
+  at any named slot. -/
+lemma crossToEnd_unitTensor {nA : ℕ} {cA : Fin (nA + 1) → C} {c : C}
+    (i : Fin (nA + 1)) (hc : cA i = c) (t1 : Tensor S cA) :
+    crossToEnd i (0 : Fin 2) (by simp [hc] : S.τ (cA i) = ![S.τ c, c] 0) t1 (unitTensor c) =
+      permT (Fin.append i.succAbove (fun _ : Fin 1 => i)) (IsReindexing.move_last i hc) t1 := by
+  set τ : Fin (nA + 1) → Fin (nA + 1) := ⇑(Equiv.swap i (Fin.last nA)) with hτdef
+  have hτbij : Function.Bijective τ := (Equiv.swap i (Fin.last nA)).bijective
+  have hτi : τ i = Fin.last nA := Equiv.swap_apply_left i (Fin.last nA)
+  have hself : ∀ x, τ (τ x) = x := fun x => Equiv.swap_apply_self i (Fin.last nA) x
+  -- `τ` is injective, so it restricts to the survivors of `i`: some `τ'` fills the square
+  -- `(τ i).succAbove ∘ τ' = τ ∘ i.succAbove`.
+  obtain ⟨τ', hτ'⟩ : ∃ τ' : Fin nA → Fin nA, (τ i).succAbove ∘ τ' = τ ∘ i.succAbove :=
+    ⟨fun a => (Fin.exists_succAbove_eq (hτbij.1.ne (Fin.succAbove_ne i a))).choose,
+      funext fun a => (Fin.exists_succAbove_eq (hτbij.1.ne (Fin.succAbove_ne i a))).choose_spec⟩
+  have hre2 : IsReindexing cA (cA ∘ τ) τ := Tensor.IsReindexing.swap i (Fin.last nA)
+  have hre : IsReindexing (cA ∘ τ) cA τ :=
+    ⟨hτbij, fun x => by simp only [Function.comp_apply, hself]⟩
+  have ht1 : permT τ hre (permT τ hre2 t1) = t1 := by
+    rw [permT_permT]; exact permT_congr_eq_id _ _ _ (funext hself)
+  conv_lhs => rw [← ht1]
+  rw [crossToEnd_permT_left i (0 : Fin 2) τ τ' hre hτ' _
+      (permT τ hre2 t1) (unitTensor c),
+    crossToEnd_unitTensor_slot hτi (by simp only [Function.comp_apply, hself]; exact hc)
+      (permT τ hre2 t1), permT_permT, permT_permT]
+  refine permT_congr (funext fun x => ?_) rfl
+  refine Fin.addCases (fun a => ?_) (fun a => ?_) x
+  · simp only [Function.comp_apply, Fin.append_left]
+    rw [show (τ i).succAbove (τ' a) = τ (i.succAbove a) from congrFun hτ' a, hself]
+  · simp only [Function.comp_apply, Fin.append_right, hself]
+
+/-!
+
+## B. Round trips against a matched pair
+
+When two rank-2 tensors collapse to the unit tensor after their shared index is contracted,
+contracting a slot first against one and then against the other returns the original tensor.
+
+-/
+
+/-- The color list `crossToEnd` produces from a matched rank-2 pair `M : ![a, d]`, `M' : ![b, e]` is
+  the color list `![S.τ e, e]` of `unitTensor e`, via the identity slot map: the reindexing carried
+  by the collapse hypothesis `M · M' = δ` of the round trips below. Only the surviving colors `a`
+  and `e` enter, and `a` equals `S.τ e` only propositionally, so a pair whose colors match
+  propositionally enters with no transport. -/
+lemma IsReindexing.unitTensor_pair {a b d e : C} (h : S.τ e = a) :
+    IsReindexing (![S.τ e, e] : Fin 2 → C)
+      (Fin.append ((![a, d] : Fin 2 → C) ∘ (Fin.last 1).succAbove)
+        ((![b, e] : Fin 2 → C) ∘ (0 : Fin 2).succAbove))
+      (id : Fin 2 → Fin 2) :=
+  IsReindexing.on_id.mpr (fun j => by fin_cases j <;> first | exact h | rfl)
+
+/-- Round trip of two contractions against a matched pair, in result-to-end form. Contracting slot
+  `i` of `t` against `M₁`, then contracting the surviving `M₁`-index (deposited at slot `j`) against
+  `M₂`, returns `t` up to the cycle that moves the round-tripped slot from the end back to `i`,
+  whenever `M₁` and `M₂` collapse to the unit tensor. The last slot is threaded as a variable `j`
+  with `hj : j = last nA` so that a caller can apply it at a propositionally-last slot without a
+  dependent rewrite of the slot index. -/
+lemma crossToEnd_round_trip_of_unit_slot {nA : ℕ} {c : Fin (nA + 1) → C} {d : C}
+    (i j : Fin (nA + 1)) (hj : j = Fin.last nA)
+    (M₁ : Tensor S ![S.τ (c i), d]) (M₂ : Tensor S ![S.τ d, c i])
+    (hM : crossToEnd (Fin.last 1) (0 : Fin 2) rfl M₁ M₂ =
+      permT (id : Fin 2 → Fin 2) (IsReindexing.unitTensor_pair rfl)
+        (unitTensor (S := S) (c i)))
+    (t : Tensor S c) :
+    crossToEnd j (0 : Fin 2)
+        (by subst hj
+            rw [show (Fin.last nA : Fin (nA + 1)) = Fin.natAdd nA (0 : Fin 1) from
+                  Fin.ext (by simp), Fin.append_right]; rfl)
+        (crossToEnd i (0 : Fin 2) rfl t M₁) M₂ =
+      permT (Fin.append i.succAbove (fun _ : Fin 1 => i))
+        (by
+          subst hj
+          exact ⟨by
+            rw [Fin.append_succAbove_const_eq_cycleIcc i]
+            exact (Fin.cycleIcc i (Fin.last nA)).bijective,
+          fun x => by
+            refine Fin.addCases (fun a => ?_) (fun a => ?_) x
+            · simp only [Function.comp_apply, Fin.append_left, Fin.succAbove_last,
+                show (Fin.castSucc a : Fin (nA + 1)) = Fin.castAdd 1 a from rfl]
+            · fin_cases a
+              simp [Fin.append_right, Fin.succAbove_zero]⟩)
+        t := by
+  subst hj
+  rw [crossToEnd_assoc_rankTwo i rfl rfl t M₁ M₂]
+  rw [hM]
+  rw [crossToEnd_permT_right i (0 : Fin 2)
+    (id : Fin 2 → Fin 2) (fun x : Fin 1 => x)
+    (IsReindexing.on_id.mpr (fun i => by fin_cases i <;> rfl)) rfl]
+  -- The `id`-spelled map leaves the composite slot proof type-correct only at default
+  -- transparency, so `rw`/`simp` cannot key on it; `erw` matches up to defeq.
+  erw [crossToEnd_unitTensor (nA := nA) (cA := c) (c := c i) i rfl]
+  erw [permT_permT, permT_permT]
+  apply permT_congr
+  · funext x
+    refine Fin.addCases (fun a => ?_) (fun a => ?_) x
+    · simp [Fin.append_left]
+    · fin_cases a
+      simp [Fin.append_right, Function.comp_apply]
+  · rfl
+
+/-- Round trip for `crossToSlot` at an arbitrary slot, with the colors in their composite form.
+  The general-color statement `crossToSlot_raise_lower_round_trip` is obtained from this by
+  substituting its three color equalities. -/
+private lemma crossToSlot_round_trip_of_unit {nA : ℕ} {c : Fin (nA + 1) → C} {d : C}
+    (i : Fin (nA + 1))
+    (M₁ : Tensor S ![S.τ (c i), d]) (M₂ : Tensor S ![S.τ d, c i])
+    (hM : crossToEnd (Fin.last 1) (0 : Fin 2) rfl M₁ M₂ =
+      permT (id : Fin 2 → Fin 2) (IsReindexing.unitTensor_pair rfl)
+        (unitTensor (S := S) (c i)))
+    (t : Tensor S c) :
+    crossToSlot (S := S) i (0 : Fin 2)
+        (by rw [Function.update_self] : S.τ (Function.update c i d i) = S.τ d) M₂
+        (crossToSlot (S := S) i (0 : Fin 2) rfl M₁ t) =
+      permT (id : Fin (nA + 1) → Fin (nA + 1)) (IsReindexing.update_update_of_eq i rfl) t := by
+  have hcycle : (⇑(Fin.cycleIcc i (Fin.last nA)).symm) i = Fin.last nA :=
+    (Equiv.symm_apply_eq _).2 (Fin.cycleIcc_of_last (Fin.le_last i)).symm
+  -- The inverse cycle carries a reinserted survivor `i.succAbove a` back to its position `a` in
+  -- the survivor block.
+  have hcycle_succAbove : ∀ a : Fin nA,
+      (Fin.cycleIcc i (Fin.last nA)).symm (i.succAbove a) = Fin.castAdd 1 a := fun a =>
+    (Equiv.symm_apply_eq _).2
+      (by rw [← Fin.append_succAbove_const_eq_cycleIcc i, Fin.append_left])
+  rw [crossToSlot_eq_crossToEnd, crossToSlot_eq_crossToEnd]
+  -- `crossToSlot`'s output color reduces to the clean one only at default transparency, so `rw`
+  -- cannot key on the composite. Precompute the left commutator and `erw` it instead.
+  have hpl := crossToEnd_permT_left i (0 : Fin 2)
+    ⇑(Fin.cycleIcc i (Fin.last nA)).symm id (IsReindexing.crossToSlot_cycle i (0 : Fin 2))
+    (by
+      funext a
+      simp only [Function.comp_apply, id_eq]
+      rw [hcycle, hcycle_succAbove, Fin.succAbove_last]
+      rfl)
+    (show S.τ (Function.update c i d i) = ![S.τ d, c i] 0 by
+      rw [Function.update_self, Matrix.cons_val_zero])
+    (crossToEnd i (0 : Fin 2) rfl t M₁) M₂
+  erw [hpl]
+  erw [permT_permT]
+  rw [crossToEnd_round_trip_of_unit_slot i ((⇑(Fin.cycleIcc i (Fin.last nA)).symm) i)
+    hcycle M₁ M₂ hM t, permT_permT]
+  apply permT_congr
+  · funext x
+    simp only [Function.comp_id]
+    rw [Fin.append_castAdd_natAdd_eq_id]
+    simp [Function.comp_apply, Fin.append_succAbove_const_eq_cycleIcc]
+  · rfl
+
+/-- Raising then lowering a named index, with every color threaded propositionally. For a rank-2
+  metric `M : ![a, d]` and an inverse `M' : ![b, e]` collapsing to the unit tensor (`M · M' = δ`),
+  at any rank and any slot `i`: contracting slot `i` with `M`, then contracting the result with
+  `M'`, is the identity up to the `Function.update` color reindex.
+
+  No color is pinned to a composite. `ha : τ (c i) = a` places the metric's contracted slot,
+  `hb : τ d = b` the inverse's, and `he : c i = e` the surviving one, so a caller whose metric and
+  inverse sit at literal colors supplies them directly, with no transporting `permT` on either
+  factor. Lowering then raising is this same statement with `M` and `M'` exchanged and the reversed
+  collapse `M' · M = δ`; neither collapse follows from the other here. -/
+lemma crossToSlot_raise_lower_round_trip {nA : ℕ} {c : Fin (nA + 1) → C} {a b d e : C}
+    (i : Fin (nA + 1)) (he : c i = e) (ha : S.τ (c i) = a) (hb : S.τ d = b)
+    (M : Tensor S ![a, d]) (M' : Tensor S ![b, e])
+    (hM : crossToEnd (Fin.last 1) (0 : Fin 2) hb M M' =
+      permT (id : Fin 2 → Fin 2)
+        (IsReindexing.unitTensor_pair ((congrArg S.τ he.symm).trans ha))
+        (unitTensor (S := S) e))
+    (t : Tensor S c) :
+    crossToSlot (S := S) i (0 : Fin 2)
+        (by rw [Function.update_self]; exact hb : S.τ (Function.update c i d i) = b) M'
+        (crossToSlot (S := S) i (0 : Fin 2) ha M t) =
+      permT (id : Fin (nA + 1) → Fin (nA + 1)) (IsReindexing.update_update_of_eq i he) t := by
+  subst ha
+  subst hb
+  subst he
+  exact crossToSlot_round_trip_of_unit i M M' hM t
+
+/-!
+
+## C. Raising and lowering as an equivalence
+
+Both collapse orders are hypotheses here and each is used once: `M · M' = δ` gives one round trip
+by section B, `M' · M = δ` the other through injectivity of the lowering half.
+
+-/
+
+section RoundTripEquiv
+
+variable {nA : ℕ} {c : Fin (nA + 1) → C} {a b d e : C} (i : Fin (nA + 1))
+    (he : c i = e) (ha : S.τ (c i) = a) (hb : S.τ d = b)
+    (M : Tensor S ![a, d]) (M' : Tensor S ![b, e])
+    (hMM' : crossToEnd (Fin.last 1) (0 : Fin 2) hb M M' =
+      permT (id : Fin 2 → Fin 2)
+        (IsReindexing.unitTensor_pair ((congrArg S.τ he.symm).trans ha))
+        (unitTensor (S := S) e))
+    (hM'M : crossToEnd (Fin.last 1) (0 : Fin 2) ((congrArg S.τ he.symm).trans ha) M' M =
+      permT (id : Fin 2 → Fin 2) (IsReindexing.unitTensor_pair hb) (unitTensor (S := S) d))
+
+include hMM' in
+/-- Lowering undoes raising: `crossToSlot_raise_lower_round_trip` with the color cast absorbed into
+  `crossToSlotInv`. -/
+lemma crossToSlotInv_crossToSlot (t : Tensor S c) :
+    crossToSlotInv i he hb M' (crossToSlot i (0 : Fin 2) ha M t) = t := by
+  simp only [crossToSlotInv, LinearMap.coe_comp, Function.comp_apply]
+  -- Unfolding `crossToSlotInv` leaves the inner slot proof at the clean color `b` where the goal
+  -- wants the composite `![b, e] 0`, so `rw` cannot key on the round trip; `erw` matches.
+  erw [crossToSlot_raise_lower_round_trip i he ha hb M M' hMM' t, permT_permT]
+  exact permT_congr_eq_id _ _ _ rfl
+
+include hMM' hM'M in
+/-- Raising undoes lowering. The reversed collapse `M' · M = δ` is the round trip at the color
+  list `Function.update c i d` with the pair exchanged, which gives the lowering half a left
+  inverse and hence injectivity; that upgrades `crossToSlotInv_crossToSlot` to a two-sided
+  inverse. -/
+lemma crossToSlot_crossToSlotInv (t : Tensor S (Function.update c i d)) :
+    crossToSlot i (0 : Fin 2) ha M (crossToSlotInv i he hb M' t) = t := by
+  have hswap := crossToSlot_raise_lower_round_trip (S := S) (c := Function.update c i d) i
+    (by simp : Function.update c i d i = d)
+    (by rw [Function.update_self]; exact hb : S.τ (Function.update c i d i) = b)
+    ((congrArg S.τ he.symm).trans ha) M' M hM'M
+  have hgi : Function.Injective (crossToSlot (S := S) i (0 : Fin 2)
+      (show S.τ (Function.update c i d i) = b by rw [Function.update_self]; exact hb) M') := by
+    intro x y hxy
+    exact permT_injective _ (by rw [← hswap x, ← hswap y, hxy])
+  have hinj : Function.Injective (crossToSlotInv (S := S) i he hb M') := by
+    simp only [crossToSlotInv, LinearMap.coe_comp]
+    exact (permT_injective _).comp hgi
+  exact Function.LeftInverse.rightInverse_of_injective
+    (crossToSlotInv_crossToSlot i he ha hb M M' hMM') hinj t
+
+/-- Raising and lowering a named index against a mutually inverse pair, as a linear equivalence: the
+  two color assignments `c` and `Function.update c i d` carry the same tensors. `M` and `M'` are
+  matched only propositionally and `d` is unrelated to `c i`, so this covers a metric pairing two
+  unrelated colors as well as a metric and its inverse at `S.τ (c i)`. -/
+noncomputable def crossToSlotEquiv : Tensor S c ≃ₗ[k] Tensor S (Function.update c i d) :=
+  LinearEquiv.mk (crossToSlot i (0 : Fin 2) ha M) (crossToSlotInv i he hb M').toFun
+    (crossToSlotInv_crossToSlot i he ha hb M M' hMM')
+    (crossToSlot_crossToSlotInv i he ha hb M M' hMM' hM'M)
+
+end RoundTripEquiv
+
+end Tensor
+
+end TensorSpecies
diff --git a/Physlib/Relativity/Tensors/Dual.lean b/Physlib/Relativity/Tensors/Dual.lean
index 4771c2077..fa88ec66c 100644
--- a/Physlib/Relativity/Tensors/Dual.lean
+++ b/Physlib/Relativity/Tensors/Dual.lean
@@ -6,10 +6,49 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Physlib.Relativity.Tensors.MetricTensor
+public import Physlib.Relativity.Tensors.Contraction.UnitTensorContraction
 /-!
 
 # Dual tensors
 
+## i. Overview
+
+The metric tensor identifies a tensor with the one obtained by dualising the color of a single
+index: contracting slot `i` of `t` against `metricTensor (S.τ (c i))` returns a tensor of color
+`Function.update c i (S.τ (c i))`, leaving every other slot alone. This is the raising and lowering
+of a named index, `T^{μν} ↦ T_{μ}{}^{ν}`. `toDualMapAtIndex i` is that contraction, `crossToSlot`
+against the metric, at every rank and every named slot.
+
+A metric contracted against the metric at the dual color collapses to the unit tensor, in both
+orders. So the contraction back against `metricTensor (c i)`, `fromDualMapAtIndex i`, inverts it,
+and the two assemble into the linear equivalence `toDualAtIndex i`: the two color assignments
+carry the same information. Dualising the same index twice returns the original tensor, up to the
+reindexing of the colors.
+
+## ii. Key results
+
+- `TensorSpecies.Tensor.toDualMapAtIndex` : dualise the color of the index `i` by contracting with
+    the metric tensor.
+- `TensorSpecies.Tensor.fromDualMapAtIndex` : the returning contraction, against the metric tensor
+    at `c i`.
+- `TensorSpecies.Tensor.toDualMapAtIndex_toDualMapAtIndex` : dualising the index `i` twice returns
+    the original tensor.
+- `TensorSpecies.Tensor.toDualMapAtIndex_equivariant` : dualising an index commutes with the
+    `G`-action.
+- `TensorSpecies.Tensor.toDualAtIndex` : raising and lowering the index `i` as a linear
+    equivalence.
+
+## iii. Table of contents
+
+- A. Dualising a named index
+- B. Contracting a metric against its dual
+- C. Dualising twice
+- D. The returning contraction
+- E. Equivariance
+- F. Raising and lowering as an equivalence
+
+## iv. References
+
 -/
 
 @[expose] public section
@@ -21,141 +60,155 @@ variable {k : Type} [RCLike k] {C : Type} {G : Type} [Group G]
     {basisIdx : C → Type} [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)]
     {rep : (c : C) → Representation k G (V c)} {b : (c : C) → Module.Basis (basisIdx c) k (V c)}
     {S : TensorSpecies k C G V basisIdx rep b}
-attribute [-simp] LinearEquiv.cast_apply
 
 namespace Tensor
 
-/-- The linear map taking a tensor based on the color `S.τ c` to a tensor
-  based on the color `c`, defined by contraction with the metric tensor. -/
-noncomputable def fromDualMap {c : C} : S.Tensor ![S.τ c] →ₗ[k] S.Tensor ![c] where
-  toFun t := permT id (by simp; rfl)
-    (contrT 1 1 2 (by simp; rfl) (prodT (metricTensor c) t))
-  map_add' t1 t2 := by
-    simp
-  map_smul' r t := by
-    simp
-
-lemma fromDualMap_apply {c : C} (t : S.Tensor ![S.τ c]) :
-    fromDualMap t = permT id (by simp; rfl)
-      (contrT 1 1 2 (by simp; rfl) (prodT (metricTensor c) t)) := by
-  rfl
-
-/-- The linear map taking a tensor based on the color `c` to a tensor
-  based on the color `S.τ c`, defined by contraction with the metric tensor. -/
-noncomputable def toDualMap {c : C} : S.Tensor ![c] →ₗ[k] S.Tensor ![S.τ c] where
-  toFun t := permT id (by
-    simp; rfl) (contrT 1 1 2 (by
-    change _ ∧ S.τ (S.τ c) = c
-    simp) (prodT (metricTensor (S.τ c)) t))
-  map_add' t1 t2 := by
-    simp
-  map_smul' r t := by
-    simp
-
-lemma toDualMap_apply {c : C} (t : S.Tensor ![c]) :
-    toDualMap t = permT id (by
-      simp; rfl) (contrT 1 1 2 (by
-      change _ ∧ S.τ (S.τ c) = c
-      simp) (prodT (metricTensor (S.τ c)) t)) := by
-  rfl
-
-set_option backward.isDefEq.respectTransparency false in
+/-!
+
+## A. Dualising a named index
+
+-/
+
+/-- The linear map between `S.Tensor c` and `S.Tensor (Function.update c i (S.τ (c i)))`
+  formed by contracting the index `i` with the metric tensor. -/
+noncomputable def toDualMapAtIndex : {n : ℕ} → {c : Fin n → C} → (i : Fin n) →
+    S.Tensor c →ₗ[k] S.Tensor (Function.update c i (S.τ (c i)))
+  | 0, _, i => i.elim0
+  | _ + 1, c, i => crossToSlot i (0 : Fin 2) rfl (metricTensor (S := S) (S.τ (c i)))
+
+/-!
+
+## B. Contracting a metric against its dual
+
+-/
+
+/-- The metric tensor at `S.τ c` contracted with the metric tensor at `c` is the unit tensor
+  at `c`. -/
+lemma crossToEnd_dual_metricTensor_metricTensor {c : C} :
+    crossToEnd (Fin.last 1) (0 : Fin 2) (S.τ_τ_apply c) (metricTensor (S := S) (S.τ c))
+        (metricTensor (S := S) c) =
+      permT (id : Fin 2 → Fin 2) (IsReindexing.unitTensor_pair rfl) (unitTensor (S := S) c) := by
+  rw [crossToEnd_two, contrT_dual_metricTensor_metricTensor, permT_permT]
+  exact permT_congr rfl rfl
+
+/-- The metric tensor at `c` contracted with the metric tensor at `S.τ c` is the unit tensor
+  at `S.τ c`. -/
+lemma crossToEnd_metricTensor_metricTensor_eq_dual_unit {c : C} :
+    crossToEnd (Fin.last 1) (0 : Fin 2) rfl (metricTensor (S := S) c)
+        (metricTensor (S := S) (S.τ c)) =
+      permT (id : Fin 2 → Fin 2) (IsReindexing.unitTensor_pair (S.τ_τ_apply c))
+        (unitTensor (S := S) (S.τ c)) := by
+  rw [crossToEnd_two, contrT_metricTensor_metricTensor_eq_dual_unit, permT_permT]
+  exact permT_congr (by decide) rfl
+
+/-!
+
+## C. Dualising twice
+
+-/
+
+/-- Dualising the index `i` twice returns the original tensor, up to the reindexing of the
+  colors. -/
+lemma toDualMapAtIndex_toDualMapAtIndex {n : ℕ} {c : Fin n → C}
+    (i : Fin n) (t : S.Tensor c) :
+    toDualMapAtIndex (S := S) i (toDualMapAtIndex (S := S) i t) =
+      permT (id : Fin n → Fin n)
+        (IsReindexing.update_update_of_eq i (by simp [τ_τ_apply])) t := by
+  cases n with
+  | zero => exact i.elim0
+  | succ nA =>
+    -- Both metrics enter at literal colors, matched by `S.τ_τ_apply`, so neither is transported.
+    have key := crossToSlot_raise_lower_round_trip (S := S) i (he := rfl) (ha := rfl)
+      (hb := S.τ_τ_apply (c i)) (M := metricTensor (S := S) (S.τ (c i)))
+      (M' := metricTensor (S := S) (c i))
+      (hM := crossToEnd_dual_metricTensor_metricTensor) (t := t)
+    -- The second dualisation reads its metric at the composite color the first one left behind.
+    rw [toDualMapAtIndex, toDualMapAtIndex,
+      metricTensor_congr (by simp [Function.update_self, τ_τ_apply] :
+        S.τ (Function.update c i (S.τ (c i)) i) = c i)]
+    erw [crossToSlot_permT_right_id, key, permT_permT]
+    exact permT_congr (by funext j; simp) rfl
+
+/-!
+
+## D. The returning contraction
+
+-/
+
+/-- The linear map between `S.Tensor (Function.update c i (S.τ (c i)))` and `S.Tensor c`
+  formed by contracting the index `i` with the metric tensor. It is the inverse of
+  `toDualMapAtIndex`. -/
+noncomputable def fromDualMapAtIndex : {n : ℕ} → {c : Fin n → C} → (i : Fin n) →
+    S.Tensor (Function.update c i (S.τ (c i))) →ₗ[k] S.Tensor c
+  | 0, _, i => i.elim0
+  | _ + 1, c, i => crossToSlotInv i rfl (S.τ_τ_apply (c i)) (metricTensor (S := S) (c i))
+
 @[simp]
-lemma toDualMap_fromDualMap {c : C} (t : S.Tensor ![S.τ c]) :
-    toDualMap (fromDualMap t) = t := by
-  rw [toDualMap_apply, fromDualMap_apply, prodT_permT_right, prodT_contrT_snd,
-    contrT_permT, contrT_permT, contrT_comm, permT_permT, permT_permT]
-  conv_lhs =>
-    enter [2, 2]
-    change contrT 1 1 2 _ _
-    enter [2]
-    change contrT 3 1 2 _ _
-  rw [prodT_assoc', prodT_swap, contrT_permT, contrT_permT]
-  conv_lhs =>
-    enter [2, 2, 2, 2, 2]
-    rw [contrT_congr (n := 1 + 2) (Fin.natAdd (m := 4)  1 1) (Fin.natAdd (m := 4) 1 2) _
-      (by rfl) (by rfl)]
-    rw (transparency := .instances) [contrT_prodT_snd 1 2 (by change _ ∧ S.τ (S.τ c) = c; simp)]
-    rw [contrT_dual_metricTensor_metricTensor, prodT_permT_right, prodT_swap]
-    simp only [CompTriple.comp_eq, permT_permT, Fin.reduceNatAdd, Fin.cast_eq_self]
-  conv_lhs =>
-    enter [2, 2]
-    rw [permT_permT]
-    rw (transparency := .instances) [permT_permT, contrT_permT]
-  conv_lhs =>
-    enter [2, 2, 2]
-    rw [contrT_congr 1 2 _ (by rfl) (by rfl)]
-    enter [2]
-    rw [contrT_unitTensor_dual_single]
-  simp only [permT_permT, CompTriple.comp_eq]
-  rw (transparency := .instances) [permT_permT]
-  apply permT_congr_eq_id
-  ext i
-  fin_cases i
-  simp
-
-lemma fromDualMap_eq_permT_toDualMap {c : C} (t : S.Tensor ![S.τ c]) :
-    fromDualMap t = permT id (by simp) (toDualMap t) := by
-  rw [fromDualMap_apply, toDualMap_apply]
-  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, permT_permT, CompTriple.comp_eq]
-  rw [metricTensor_congr (by simp : c = S.τ (S.τ c))]
-  rw [prodT_permT_left, contrT_permT]
-  simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, permT_permT, CompTriple.comp_eq]
-  apply permT_congr
-  · ext i
-    fin_cases i
-    rfl
-  · rfl
-
-lemma toDualMap_eq_permT_fromDualMap {c : C} (t : S.Tensor ![c]) :
-    toDualMap t = (fromDualMap (permT id (by simp) t)) := by
-  rw [fromDualMap_eq_permT_toDualMap]
-  rw [toDualMap_apply, toDualMap_apply]
-  conv_rhs =>
-    enter [2, 2]
-    rw [prodT_permT_right]
-    rw [metricTensor_congr (by simp : S.τ (S.τ (S.τ c)) = S.τ c)]
-    rw [prodT_permT_left]
-    rw [contrT_permT, contrT_permT]
-  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, permT_permT, CompTriple.comp_eq,
-    τ_τ_apply, IsReindexing.on_id, Matrix.cons_val_fin_one, implies_true]
-  apply permT_congr
-  · ext i
-    fin_cases i
-    rfl
-  · rfl
+lemma fromDualMapAtIndex_toDualMapAtIndex {n : ℕ} {c : Fin n → C} (i : Fin n) (t : S.Tensor c) :
+    fromDualMapAtIndex (S := S) i (toDualMapAtIndex (S := S) i t) = t := by
+  cases n with
+  | zero => exact i.elim0
+  | succ nA =>
+    exact crossToSlotInv_crossToSlot i rfl rfl (S.τ_τ_apply (c i)) _ _
+      crossToEnd_dual_metricTensor_metricTensor t
 
 @[simp]
-lemma fromDualMap_toDualMap {c : C} (t : S.Tensor ![c]) :
-    fromDualMap (toDualMap t) = t := by
-  rw [fromDualMap_eq_permT_toDualMap]
-  conv_lhs =>
-    enter [2, 2]
-    rw [toDualMap_eq_permT_fromDualMap]
-  simp
-
-/-- The linear equivalence between `S.Tensor ![c]` and
-  `S.Tensor ![S.τ c]` formed by contracting with metric tensors. -/
-noncomputable def toDual {c : C} : S.Tensor ![c] ≃ₗ[k] S.Tensor ![S.τ c] :=
-  LinearEquiv.mk toDualMap fromDualMap.toFun
-    (fun x => by simp) (fun x => by simp)
-
-lemma toDual_equivariant {c : C} (g : G) (t : S.Tensor ![c]) :
-    toDual (g • t) = g • toDual t := by
-  simp [toDual, toDualMap]
-  conv_lhs => rw [← metricTensor_invariant g]
-  rw [prodT_equivariant, contrT_equivariant, permT_equivariant]
+lemma toDualMapAtIndex_fromDualMapAtIndex {n : ℕ} {c : Fin n → C} (i : Fin n)
+    (t : S.Tensor (Function.update c i (S.τ (c i)))) :
+    toDualMapAtIndex (S := S) i (fromDualMapAtIndex (S := S) i t) = t := by
+  cases n with
+  | zero => exact i.elim0
+  | succ nA =>
+    exact crossToSlot_crossToSlotInv i rfl rfl (S.τ_τ_apply (c i)) _ _
+      crossToEnd_dual_metricTensor_metricTensor crossToEnd_metricTensor_metricTensor_eq_dual_unit t
 
-/-- The linear map between `S.Tensor c` and `S.Tensor (Function.update c i (S.τ (c i)))`
-  formed by contracting with metric tensors at a specific index. -/
-noncomputable def toDualAtIndex {c : Fin n → C} (i : Fin n) :
-    S.Tensor c →ₗ[k] S.Tensor (Function.update c i (S.τ (c i))) where
-  toFun t := permT _ (IsReindexing.contr_two_rotate S i) <|
-    contrT (n) (Fin.natAdd n (0 : Fin 2)) (Fin.castAdd 2 i)
-      (by simp [Fin.ext_iff]; grind) <|
-    prodT t (metricTensor (S := S) (S.τ (c i)))
-  map_add' := by intros; simp
-  map_smul' := by intros; simp
+/-!
+
+## E. Equivariance
+
+-/
+
+/-- Dualising the index `i` commutes with the action of `G`. -/
+@[simp]
+lemma toDualMapAtIndex_equivariant {n : ℕ} {c : Fin n → C} (i : Fin n) (g : G) (t : S.Tensor c) :
+    toDualMapAtIndex (S := S) i (g • t) = g • toDualMapAtIndex (S := S) i t := by
+  cases n with
+  | zero => exact i.elim0
+  | succ nA =>
+    rw [toDualMapAtIndex]
+    conv_lhs => rw [← metricTensor_invariant (S := S) g]
+    exact crossToSlot_equivariant i (0 : Fin 2) _ g _ t
+
+/-!
+
+## F. Raising and lowering as an equivalence
+
+-/
+
+/-- The linear equivalence between `S.Tensor c` and `S.Tensor (Function.update c i (S.τ (c i)))`
+  formed by contracting the index `i` with the metric tensor. -/
+noncomputable def toDualAtIndex : {n : ℕ} → {c : Fin n → C} → (i : Fin n) →
+    S.Tensor c ≃ₗ[k] S.Tensor (Function.update c i (S.τ (c i)))
+  | 0, _, i => i.elim0
+  | _ + 1, c, i =>
+    crossToSlotEquiv i rfl rfl (S.τ_τ_apply (c i)) (metricTensor (S := S) (S.τ (c i)))
+      (metricTensor (S := S) (c i)) crossToEnd_dual_metricTensor_metricTensor
+      crossToEnd_metricTensor_metricTensor_eq_dual_unit
+
+@[simp]
+lemma toDualAtIndex_apply {n : ℕ} {c : Fin n → C} (i : Fin n) (t : S.Tensor c) :
+    toDualAtIndex (S := S) i t = toDualMapAtIndex (S := S) i t := by
+  cases n with
+  | zero => exact i.elim0
+  | succ nA => rfl
+
+@[simp]
+lemma toDualAtIndex_symm_apply {n : ℕ} {c : Fin n → C} (i : Fin n)
+    (t : S.Tensor (Function.update c i (S.τ (c i)))) :
+    (toDualAtIndex (S := S) i).symm t = fromDualMapAtIndex (S := S) i t := by
+  cases n with
+  | zero => exact i.elim0
+  | succ nA => rfl
 
 end Tensor
 
diff --git a/Physlib/Relativity/Tensors/Elab.lean b/Physlib/Relativity/Tensors/Elab.lean
index efecd4fd6..724434957 100644
--- a/Physlib/Relativity/Tensors/Elab.lean
+++ b/Physlib/Relativity/Tensors/Elab.lean
@@ -5,10 +5,8 @@ Authors: Joseph Tooby-Smith
 -/
 module
 
-public import Physlib.Relativity.Tensors.Contraction.Basic
-public import Physlib.Relativity.Tensors.Evaluation
-public import Physlib.Relativity.Tensors.Tensorial
 public import Physlib.Relativity.Tensors.Dual
+public import Physlib.Relativity.Tensors.Tensorial
 /-!
 
 # Elaboration of tensor expressions
@@ -401,7 +399,7 @@ def TensorExpressionOperator.create (stx : Syntax) :
   indices with `τ`-syntax. -/
 def TensorExpressionOperator.jiggle : TensorExpressionOperator := fun (ind, T) => do
   let pos ← getJigglePos ind
-  let T' := pos.foldl (fun T' x => Syntax.mkApp (mkIdent ``Tensor.toDualAtIndex)
+  let T' := pos.foldl (fun T' x => Syntax.mkApp (mkIdent ``Tensor.toDualMapAtIndex)
     #[Syntax.mkNumLit (toString x), T']) T
   let ind' := ind.map indexRemoveTau
   return (ind', T')
@@ -667,13 +665,13 @@ variable {k : Type} [RCLike k] {C : Type} [DecidableEq C]  {G : Type} [Group G]
     {w : S.Tensor ![c3]} {td : S.Tensor ![S.τ c1, S.τ c2]}
     {M : Type} [AddCommMonoid M] [Module k M] [Tensorial S c M] (m : M)
 
-/-- info: (toDualAtIndex 0) u :
+/-- info: (toDualMapAtIndex 0) u :
   S.Tensor (Function.update ![c1, c2] 0 (S.τ (![c1, c2] 0))) -/
 #guard_msgs (whitespace := lax) in
 #check {u | τ(α) β}ᵀ
 
 /-- info: (contrT 2 1 3 ⋯)
-  ((prodT u) ((toDualAtIndex 1) u)) :
+  ((prodT u) ((toDualMapAtIndex 1) u)) :
     S.Tensor (Fin.append ![c1, c2]
       (Function.update ![c1, c2] 1 (S.τ (![c1, c2] 1))) ∘ Fin.succSuccAbove 1 3) -/
 #guard_msgs (whitespace := lax) in
diff --git a/Physlib/Relativity/Tensors/Reindexing.lean b/Physlib/Relativity/Tensors/Reindexing.lean
index 8c81e7ce6..6bbb7e51d 100644
--- a/Physlib/Relativity/Tensors/Reindexing.lean
+++ b/Physlib/Relativity/Tensors/Reindexing.lean
@@ -32,6 +32,40 @@ We are interested in the interaction of reindexing with the following operations
 
 open Module
 
+namespace Fin
+
+/-!
+
+## Index maps
+
+The finite index maps out of which the reindexings below are built: `Fin.append` for products and
+`Fin.succAbove` for a deleted slot. The lemmas on `Fin.succSuccAbove`, for a deleted pair, are in
+`Physlib.Relativity.Tensors.Contraction.SuccSuccAbove`.
+
+-/
+
+/-- Splitting `Fin (m + n)` into its two blocks and reassembling them is the identity. -/
+lemma append_castAdd_natAdd_eq_id {m n : ℕ} :
+    Fin.append (Fin.castAdd n) (Fin.natAdd m) = (id : Fin (m + n) → Fin (m + n)) := by
+  simpa using Fin.append_castAdd_natAdd (f := (id : Fin (m + n) → Fin (m + n)))
+
+/-- Moving slot `i` to the end is the cycle `[i, last]`: the block map that lists the
+  `i.succAbove` survivors in order and then `i` is `Fin.cycleIcc i (Fin.last n)`. -/
+lemma append_succAbove_const_eq_cycleIcc {n : ℕ} (i : Fin (n + 1)) :
+    Fin.append i.succAbove (fun _ : Fin 1 => i) = ⇑(Fin.cycleIcc i (Fin.last n)) := by
+  funext y
+  refine Fin.addCases (fun a => ?_) (fun a => ?_) y
+  · rw [Fin.append_left]
+    have h := congrFun (Fin.cycleIcc_comp_succAbove i (Fin.last n) (Fin.le_last i)) a
+    rw [Fin.succAbove_last] at h
+    exact h.symm
+  · rw [Fin.append_right]
+    have : (Fin.natAdd n a : Fin (n + 1)) = Fin.last n := by
+      apply Fin.ext; simp [Fin.val_natAdd]
+    rw [this, Fin.cycleIcc_of_le_of_le (Fin.le_last _) (Fin.le_last _), if_pos rfl]
+
+end Fin
+
 namespace TensorSpecies
 
 variable {k : Type} [CommRing k] {C : Type} {G : Type} [Group G]
@@ -364,6 +398,23 @@ lemma succAbove {n n1 : ℕ} {c : Fin (n + 1) → C} {c1 : Fin (n1 + 1) → C}
   · simpa [hi] using IsReindexing.succAbove_of_eq_zero i h hi
   · simpa [hi] using IsReindexing.succAbove_of_neq_zero i h hi
 
+/-- The conclusion of `succAbove` from an explicit survivor relabelling: if `σ'` fills the square
+  `(σ i).succAbove ∘ σ' = σ ∘ i.succAbove`, carrying the complement of `i` to the complement of
+  `σ i`, then it is a reindexing of the two shortened colour lists. The square forces `σ'` to be
+  injective, hence bijective, so no bijectivity hypothesis is needed; this is why the statement is
+  restricted to equal lengths.
+
+  Where `succAbove` builds the relabelling from `σ` as a `dite` composite, the map here is the
+  caller's, which is what lets it stand in the statement of a lemma the caller instantiates. -/
+lemma succAbove_of_succAbove_eq {n : ℕ} {c c1 : Fin (n + 1) → C}
+    {σ : Fin (n + 1) → Fin (n + 1)} {σ' : Fin n → Fin n} (i : Fin (n + 1))
+    (h : IsReindexing c c1 σ) (hσ' : (σ i).succAbove ∘ σ' = σ ∘ i.succAbove) :
+    IsReindexing (c ∘ (σ i).succAbove) (c1 ∘ i.succAbove) σ' := by
+  have key : ∀ a, (σ i).succAbove (σ' a) = σ (i.succAbove a) := congrFun hσ'
+  refine ⟨Finite.injective_iff_bijective.mp (fun a b hab => ?_), fun a => ?_⟩
+  · exact Fin.succAbove_right_injective (h.injective (by rw [← key a, ← key b, hab]))
+  · simpa only [Function.comp_apply, key a] using h.2 (i.succAbove a)
+
 /-- Given a reindexing of `c` by `c1` via `σ` and two distinct indices `i ≠ j`, removing the
   `i`-th and `j`-th entries of `c1` and the `(σ i)`-th and `(σ j)`-th entries of `c` yields a
   reindexing of `c ∘ (σ i).succSuccAbove (σ j)` by `c1 ∘ i.succSuccAbove j`.
@@ -472,6 +523,30 @@ lemma append_succ_last {n : ℕ} (c : Fin (n + 1) → C) :
   · simp only [Fin.append_left, Function.comp_apply]; rfl
   · fin_cases i; simp only [Fin.append_right, Matrix.cons_val_fin_one]; rfl
 
+/-- Splitting a list of colours `c : Fin (n + 1) → C` at an arbitrary slot `i`, rather than at the
+  last one as in `append_succ_last`: the block map that lists the `i.succAbove` survivors and then
+  `i` itself matches `c` with the survivors of `i` followed by the surviving entry `c1 1` of a
+  rank-two list `c1` whose second entry is slot `i`'s colour. -/
+lemma move_last {n : ℕ} {c : Fin (n + 1) → C} {c1 : Fin 2 → C} (i : Fin (n + 1))
+    (hc : c i = c1 1) :
+    IsReindexing c
+      (Fin.append (c ∘ i.succAbove) (c1 ∘ (0 : Fin 2).succAbove))
+      (Fin.append i.succAbove (fun _ : Fin 1 => i)) :=
+  ⟨by
+      rw [Fin.append_succAbove_const_eq_cycleIcc i]
+      exact (Fin.cycleIcc i (Fin.last n)).bijective,
+    fun x => by
+      refine Fin.addCases (fun a => ?_) (fun a => ?_) x
+      · simp [Fin.append_left]
+      · fin_cases a
+        simp [Fin.append_right, hc]⟩
+
+/-- Updating slot `i` of `c` to `d` and then back to `e = c i` returns `c`, no other slot moving:
+  the colour cast a round trip of two contractions at slot `i` generates. -/
+lemma update_update_of_eq {n : ℕ} {c : Fin n → C} {d e : C} (i : Fin n) (he : c i = e) :
+    IsReindexing c (Function.update (Function.update c i d) i e) (id : Fin n → Fin n) :=
+  on_id.mpr (fun j => by by_cases h : j = i <;> simp [h, Function.update_of_ne, he])
+
 /-- Splitting a list of colours `c : Fin (n + 1) → C` into its first entry and its remaining
   `n` entries recovers `c`: the canonical reindexing `Fin (1 + n) ≃ Fin (n + 1)` matches
   `Fin.append ![c 0] (c ∘ Fin.succAbove 0)` with `c`. -/
@@ -492,52 +567,6 @@ lemma fin_cast_isReindexing (n n1 : ℕ) {c : Fin n → C} (h : n1 = n) :
   · intro i
     rfl
 
-/-- Contracting the `i`-th index of a tensor with the first index of an appended metric tensor
-  is, up to a cycle permutation, a reindexing to the color list where the `i`-th index is
-  replaced by its dual. -/
-lemma contr_two_rotate  {c : Fin n → C}  (i : Fin n) : IsReindexing
-    ((Fin.append c ![S.τ (c i), S.τ (c i)] ∘
-      (Fin.natAdd n (0 : Fin 2)).succSuccAbove (Fin.castAdd 2 i)))
-    (Function.update c i (S.τ (c i)))
-    (Fin.cycleIcc i ⟨n - 1, by have := i.prop; omega⟩).symm := by
-  haveI : NeZero n := ⟨by have := i.prop; omega⟩
-  set j : Fin n := ⟨n - 1, by have := i.prop; omega⟩ with hj
-  have key : ∀ y : Fin n, Fin.append c ![S.τ (c i), S.τ (c i)]
-      ((Fin.natAdd n (0 : Fin 2)).succSuccAbove (Fin.castAdd 2 i) y)
-      = Function.update c i (S.τ (c i)) (Fin.cycleIcc i j y) := by
-    intro y
-    have hval := Fin.succSuccAbove_val (Fin.natAdd n (0 : Fin 2)) (Fin.castAdd 2 i) y
-    simp only [Fin.val_natAdd, Fin.val_castAdd, Fin.val_zero, Nat.add_zero] at hval
-    rcases lt_or_ge y.val i.val with hy | hy
-    · -- y < i
-      rw [Fin.cycleIcc_of_lt (Fin.lt_def.mpr hy),
-        Function.update_of_ne (Fin.ne_of_val_ne (by omega)),
-        Fin.succSuccAbove_apply_lt_lt _ _ _ (by simp) (by simpa using hy),
-        show y.castSucc.castSucc = Fin.castAdd 2 y from by ext; simp, Fin.append_left]
-    · rcases eq_or_lt_of_le (show y.val ≤ n - 1 from by have := y.isLt; omega) with hyj | hyj
-      · -- y = j (the last index)
-        have hyj' : y = j := Fin.ext (by rw [hj]; exact hyj)
-        subst hyj'
-        have hval' : ((Fin.natAdd n (0 : Fin 2)).succSuccAbove (Fin.castAdd 2 i) j).val
-            = n + 1 := by rw [hval]; split_ifs <;> omega
-        rw [Fin.cycleIcc_of_last (Fin.le_def.mpr (by rw [hj]; omega)), Function.update_self,
-          show (Fin.natAdd n (0 : Fin 2)).succSuccAbove (Fin.castAdd 2 i) j =
-            Fin.natAdd n (1 : Fin 2)
-            from Fin.ext (by rw [hval']; simp [Fin.val_natAdd]), Fin.append_right]
-        simp
-      · -- i ≤ y < j
-        have hy1 : (y + 1).val = y.val + 1 := by
-          rw [Fin.val_add, Fin.val_one', Nat.mod_eq_of_lt (show 1 < n by omega),
-            Nat.mod_eq_of_lt (show y.val + 1 < n by omega)]
-        have hval' : ((Fin.natAdd n (0 : Fin 2)).succSuccAbove (Fin.castAdd 2 i) y).val
-            = y.val + 1 := by rw [hval]; split_ifs <;> omega
-        rw [Fin.cycleIcc_of_ge_of_lt (Fin.le_def.mpr hy) (Fin.lt_def.mpr hyj),
-          Function.update_of_ne (Fin.ne_of_val_ne (by omega)),
-          show (Fin.natAdd n (0 : Fin 2)).succSuccAbove (Fin.castAdd 2 i) y = Fin.castAdd 2 (y + 1)
-            from Fin.ext (by rw [hval', Fin.val_castAdd, hy1]), Fin.append_left]
-  refine ⟨(Equiv.symm _).bijective, fun x => ?_⟩
-  rw [Function.comp_apply, key, Equiv.apply_symm_apply]
-
 end IsReindexing
 
 end Tensor