diff --git a/Physlib/Relativity/Tensors/Basic.lean b/Physlib/Relativity/Tensors/Basic.lean
index db6de37ee..5be0b7896 100644
--- a/Physlib/Relativity/Tensors/Basic.lean
+++ b/Physlib/Relativity/Tensors/Basic.lean
@@ -8,6 +8,7 @@ module
 public import Physlib.Relativity.Tensors.TensorSpecies.Basic
 public import Mathlib.Topology.Algebra.Module.ModuleTopology
 public import Mathlib.Analysis.RCLike.Basic
+public import Mathlib.Tactic.Cases
 public import Physlib.Meta.TODO.Basic
 /-!
 
@@ -825,6 +826,31 @@ lemma permT_basis_repr_symm_apply {n m : ℕ} {c : Fin n → C} {c1 : Fin m →
   · intro t1 t2 h1 h2
     simp [h1, h2]
 
+lemma permT_basis {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
+    {σ : Fin m → Fin n} (h : PermCond c c1 σ)
+    (b : ComponentIdx c) :
+    (permT σ h) (basis (S := S) c b) = basis c1 (fun i =>
+      basisIdxCongr (by simp [h.2]) (b (σ i))) := by
+  apply (basis c1).repr.injective
+  ext b'
+  rw [permT_basis_repr_symm_apply]
+  simp [Finsupp.single_apply]
+  congr 1
+  simp only [eq_iff_iff]
+  constructor
+  · intro h
+    rw [h]
+    ext i
+    simp only [basisIdxCongr_apply_apply]
+    refine Eq.symm (ComponentIdx.congr_right b' i (PermCond.inv σ _ (σ i)) ?_)
+    simp [PermCond.apply_inv_apply]
+  · intro h
+    rw [← h]
+    ext i
+    simp only [basisIdxCongr_apply_apply]
+    apply ComponentIdx.congr_right
+    simp [PermCond.inv_apply_apply]
+
 lemma permT_eq_zero_iff {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
     {σ : Fin m → Fin n} (h : PermCond c c1 σ) (t : S.Tensor c) :
     permT σ h t = 0 ↔ t = 0 := by
@@ -865,6 +891,14 @@ lemma toField_pure {c : Fin 0 → C} (p : Pure S c) :
   ext i
   exact Fin.elim0 i
 
+lemma toField_permT {c c1 : Fin 0 → C} (σ : Fin 0 → Fin 0) (h : PermCond c c1 σ) (t : S.Tensor c) :
+    toField (permT σ h t) = toField t := by
+  induction' t using induction_on_basis with b r t ht t1 t2 h1 h2
+  · simp [toField_pure, basis_apply, permT_pure]
+  · simp
+  · simp [ht]
+  · simp [h1, h2]
+
 @[simp]
 lemma toField_basis_default {c : Fin 0 → C} :
     toField (basis c (@default (ComponentIdx (S := S) c) Unique.instInhabited)) = 1 := by
diff --git a/Physlib/Relativity/Tensors/Contraction/Basis.lean b/Physlib/Relativity/Tensors/Contraction/Basis.lean
index 9997838a3..786bd7a8e 100644
--- a/Physlib/Relativity/Tensors/Contraction/Basis.lean
+++ b/Physlib/Relativity/Tensors/Contraction/Basis.lean
@@ -226,6 +226,15 @@ lemma contrT_basis_repr_apply_eq_sum_fin {n : ℕ} {c : Fin (n + 1 + 1) → C} {
     Fintype.sum_prod_type]
   simp
 
+
+lemma contrT_basis {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)}
+    (h : i ≠ j ∧ S.τ (c i) = c j) (b : ComponentIdx (S := S) c):
+    contrT n i j h (basis c b) =
+    Pure.contrPCoeff i j h (Pure.basisVector c b) •
+      basis (c ∘ Pure.dropPairEmb i j) (b.dropPair i j) := by
+  simp [basis_apply, contrT_pure, Pure.contrP, Pure.dropPair_basisVector]
+  rfl
+
 end Tensor
 
 end TensorSpecies
diff --git a/Physlib/Relativity/Tensors/Contraction/Pure.lean b/Physlib/Relativity/Tensors/Contraction/Pure.lean
index fa552f258..8a64a97bf 100644
--- a/Physlib/Relativity/Tensors/Contraction/Pure.lean
+++ b/Physlib/Relativity/Tensors/Contraction/Pure.lean
@@ -79,6 +79,26 @@ lemma dropPairEmb_eq_succAbove_succAbove (i : Fin (n + 1 + 1)) (j : Fin (n + 1))
       simp_all
       try omega
 
+lemma dropPairEmb_eq_predAbove {i j : Fin (n + 1 + 1)} (hij : i ≠ j) :
+    dropPairEmb i j = fun x => (i.succAbove (((Fin.predAbove 0 i).predAbove j).succAbove x)) := by
+  rcases Fin.eq_self_or_eq_succAbove i j with rfl | ⟨j, rfl⟩
+  · ext x
+    grind
+  · ext x
+    simp [dropPairEmb_eq_succAbove_succAbove]
+    congr
+    refine Fin.eq_of_val_eq ?_
+    by_cases hi : i = 0
+    · subst hi
+      simp
+    simp [hi]
+    simp [Fin.predAbove, Fin.lt_def, Fin.succAbove, Fin.val_castSucc]
+    split_ifs
+    · grind
+    · simp
+    · simp
+    · grind
+
 lemma dropPairEmb_injective {n : ℕ}
     (i j : Fin (n + 1 + 1)) : Function.Injective (dropPairEmb i j) := by
   rcases Fin.eq_self_or_eq_succAbove i j with rfl | ⟨j, rfl⟩
diff --git a/Physlib/Relativity/Tensors/Evaluation.lean b/Physlib/Relativity/Tensors/Evaluation.lean
index 29567d5b7..3a97d8cd6 100644
--- a/Physlib/Relativity/Tensors/Evaluation.lean
+++ b/Physlib/Relativity/Tensors/Evaluation.lean
@@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
 module
 
 public import Physlib.Relativity.Tensors.Basic
+public import Physlib.Relativity.Tensors.Product
 /-!
 
 # Evaluation of tensor indices
@@ -57,6 +58,10 @@ lemma evalPCoeff_update_succAbove (i : Fin (n + 1)) [inst : DecidableEq (Fin (n
     evalPCoeff i b (p.update (i.succAbove j) x) = evalPCoeff i b p := by
   simp [evalPCoeff]
 
+lemma evalPCoeff_basisVector (i : Fin (n + 1)) (b : basisIdx (c i)) (b' : ComponentIdx (S := S) c) :
+    evalPCoeff i b (Pure.basisVector c b') = if b' i = b then (1 : k) else 0 := by
+  simp [evalPCoeff, basisVector, Finsupp.single_apply]
+
 /-!
 
 ## Evaluation for a pure tensor.
@@ -135,6 +140,14 @@ lemma evalT_pure {n : ℕ} {c : Fin (n + 1) → C} (i : Fin (n + 1))
   conv_rhs => rw [← PiTensorProduct.lift.tprod]
   rfl
 
+lemma evalT_basis {n : ℕ} {c : Fin (n + 1) → C} (i : Fin (n + 1))
+    (b : ComponentIdx c)
+    (x : basisIdx (c i)) :
+    evalT i x (basis (S := S) c b) = if b i = x then basis (c ∘ i.succAbove)
+      (fun j => b (i.succAbove j)) else 0 := by
+  simp [basis_apply, evalT_pure, Pure.evalP, Pure.evalPCoeff_basisVector]
+  rfl
+
 TODO "Add lemmas related to the interaction of evalT and permT, prodT and contrT."
 
 end Tensor
diff --git a/Physlib/Relativity/Tensors/RealTensor/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
index 24ad73aad..027bd1a13 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Basic.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
@@ -7,6 +7,8 @@ module
 
 public import Physlib.Relativity.Tensors.RealTensor.Metrics.Pre
 public import Physlib.Relativity.Tensors.Contraction.Basis
+public import Physlib.Relativity.Tensors.Elab
+meta import Mathlib.Tactic.Cases
 /-!
 
 ## Real Lorentz tensors
@@ -234,5 +236,73 @@ lemma contrT_basis_repr_apply_eq_fin {n d: ℕ} {c : Fin (n + 1 + 1) → realLor
       exact Ne.symm hy
   · simp
 
+/-!
+
+## Contractions and to Field
+
+-/
+
+attribute [-simp] Fintype.sum_sum_type
+
+lemma contrPCoeff_basis {d : ℕ} {c : Fin n → realLorentzTensor.Color} (i j : Fin n)
+    (hij : i ≠ j ∧ (realLorentzTensor d).τ (c i) = c j)
+    (b : ComponentIdx (S := realLorentzTensor d) c) :
+    Pure.contrPCoeff i j hij (Pure.basisVector c b) = if b i = b j then 1 else 0 := by
+  simp [Pure.contrPCoeff, Pure.basisVector]
+  generalize b i = b1 at *
+  generalize b j = b2 at *
+  suffices h : ∀ c, ∀ c1,  (hc : (realLorentzTensor d).τ c = c1) →
+    (realLorentzTensor d).castToField ((ConcreteCategory.hom
+    ((realLorentzTensor d).contr.app { as :=c }))
+    (((realLorentzTensor d).basis c) b1 ⊗ₜ[ℝ]
+      (ConcreteCategory.hom ((realLorentzTensor d).FD.map (eqToHom (by simp_all))))
+      (((realLorentzTensor d).basis c1) b2))) =
+    if b1 = b2 then 1 else 0 by
+    exact h (c i) (c j) hij.2
+  intro c c1 hc
+  subst hc
+  exact contr_basis _ _
+
+lemma contrT_eq_sum_evalT {n} {d} (c : Fin (n + 1 + 1) → Color) (i j : Fin (n + 1 + 1))
+    (h : i ≠ j ∧ (realLorentzTensor d).τ (c i) = c j) (t : ℝT(d, c)) :
+    contrT n i j h t =  ∑ (μ : Fin 1 ⊕ Fin d), permT id (by
+      simp [Pure.dropPairEmb_eq_predAbove h.1])
+     (evalT ((Fin.predAbove 0 i).predAbove j) μ (evalT i μ t)) := by
+  induction' t using Tensor.induction_on_basis with b r t h t1 t2 h1 h2
+  · rw [contrT_basis]
+    simp only [ contrPCoeff_basis, ite_smul, one_smul, zero_smul]
+    conv_rhs =>
+      enter [2, μ];
+      simp only [evalT_basis, Fin.zero_succAbove, apply_ite, Fin.succ_zero_eq_one, map_zero]
+    simp only [Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]
+    have h0 : i.succAbove ((Fin.predAbove 0 i).predAbove j) = j := by
+      rcases i.eq_zero_or_eq_succ with rfl | ⟨k, rfl⟩
+      · exact Fin.succAbove_predAbove (Ne.symm h.1)
+      · rw [Fin.predAbove_zero_succ]
+        exact Fin.succ_succAbove_predAbove (Ne.symm h.1)
+    rw [h0]
+    split_ifs
+    · rw [permT_basis]
+      congr
+      ext x
+      simp [ComponentIdx.dropPair]
+      rw [Pure.dropPairEmb_eq_predAbove h.1]
+    · simp_all
+    · simp_all
+    · rfl
+  · simp
+  · simp [Finset.smul_sum, h]
+  · simp [h1, h2, Finset.sum_add_distrib]
+
+lemma contrT_toField {d} (c : Fin 2 → Color)
+    (h : 0 ≠ 1 ∧ (realLorentzTensor d).τ (c 0) = c 1) (t : ℝT(d, c)) :
+    (contrT 0 0 1 h t).toField = ∑ (μ : Fin 1 ⊕ Fin d), {t | [μ] [μ]}ᵀ.toField := by
+  rw [contrT_eq_sum_evalT]
+  simp only [map_sum, Tensorial.self_toTensor_apply]
+  congr
+  ext μ
+  simp only [toField_permT]
+  rfl
+
 end realLorentzTensor
 end
diff --git a/Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean
index 4b68dd842..1cc7a02bf 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean
@@ -93,12 +93,12 @@ lemma contrMetric_eq_fromPairT {d : ℕ} :
 @[simp]
 lemma actionT_coMetric {d : ℕ} (g : LorentzGroup d) :
     g • η' d = η' d:= by
-  rw [TensorSpecies.metricTensor_invariant]
+  erw [TensorSpecies.metricTensor_invariant]
 
 /-- The tensor `contrMetric` is invariant under the action of `LorentzGroup d`. -/
 @[simp]
 lemma actionT_contrMetric {d} (g : LorentzGroup d) : g • η d = η d := by
-  rw [TensorSpecies.metricTensor_invariant]
+  erw [TensorSpecies.metricTensor_invariant]
 
 /-