From 85b30e9565dbcafd992c56b524e41c49211e02f4 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 6 May 2026 10:36:24 +0100
Subject: [PATCH 1/5] feat: Add contrT_toField

---
 .../Relativity/Tensors/Contraction/Basis.lean |  9 ++++
 Physlib/Relativity/Tensors/Evaluation.lean    | 12 +++++
 .../Relativity/Tensors/RealTensor/Basic.lean  | 50 +++++++++++++++++++
 .../Tensors/RealTensor/Metrics/Basic.lean     |  4 +-
 4 files changed, 73 insertions(+), 2 deletions(-)

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/Evaluation.lean b/Physlib/Relativity/Tensors/Evaluation.lean
index 29567d5b7..56056b6e7 100644
--- a/Physlib/Relativity/Tensors/Evaluation.lean
+++ b/Physlib/Relativity/Tensors/Evaluation.lean
@@ -57,6 +57,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 +139,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..c559ce166 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,53 @@ 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 _ _
+
+attribute [-simp] Nat.reduceAdd Fin.isValue Fin.succAbove_zero in
+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
+  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,
+       Tensorial.self_toTensor_apply]
+    conv_rhs =>
+      enter [2, μ];
+      simp only [evalT_basis, Fin.zero_succAbove, apply_ite, Fin.succ_zero_eq_one, map_zero]
+    simp
+    split_ifs
+    · rfl
+    · simp_all
+    · simp_all
+    · rfl
+  · simp [map_zero]
+  · simp [Finset.mul_sum, h]
+  · simp [h1, h2, Finset.sum_add_distrib]
+
 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]
 
 /-
 

From 0aee60ecf9cb127f7ab362e3783594873b70d93b Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 6 May 2026 13:14:04 +0100
Subject: [PATCH 2/5] refactor: lint

---
 Physlib/Relativity/Tensors/RealTensor/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Physlib/Relativity/Tensors/RealTensor/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
index c559ce166..73a4eae2d 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Basic.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
@@ -274,7 +274,7 @@ lemma contrT_toField {d} (c : Fin 2 → Color)
     conv_rhs =>
       enter [2, μ];
       simp only [evalT_basis, Fin.zero_succAbove, apply_ite, Fin.succ_zero_eq_one, map_zero]
-    simp
+    simp only [Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]
     split_ifs
     · rfl
     · simp_all

From 1b227f54596ed0a287a2bfd64605358926535382 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 6 May 2026 14:58:08 +0100
Subject: [PATCH 3/5] refactor: generalize proof

---
 Physlib/Relativity/Tensors/Basic.lean         | 34 +++++++++++++++++
 .../Relativity/Tensors/Contraction/Pure.lean  | 20 ++++++++++
 .../Relativity/Tensors/RealTensor/Basic.lean  | 38 ++++++++++++++-----
 3 files changed, 83 insertions(+), 9 deletions(-)

diff --git a/Physlib/Relativity/Tensors/Basic.lean b/Physlib/Relativity/Tensors/Basic.lean
index db6de37ee..5bf47d92e 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
+  constructor
+  · intro h
+    rw [h]
+    ext i
+    simp
+    refine Eq.symm (ComponentIdx.congr_right b' i (PermCond.inv σ _ (σ i)) ?_)
+    simp [PermCond.apply_inv_apply]
+  · intro h
+    rw [← h]
+    ext i
+    simp
+    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/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/RealTensor/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
index 73a4eae2d..027bd1a13 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Basic.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
@@ -263,26 +263,46 @@ lemma contrPCoeff_basis {d : ℕ} {c : Fin n → realLorentzTensor.Color} (i j :
   subst hc
   exact contr_basis _ _
 
-attribute [-simp] Nat.reduceAdd Fin.isValue Fin.succAbove_zero in
-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
+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,
-       Tensorial.self_toTensor_apply]
+    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
-    · rfl
+    · rw [permT_basis]
+      congr
+      ext x
+      simp [ComponentIdx.dropPair]
+      rw [Pure.dropPairEmb_eq_predAbove h.1]
     · simp_all
     · simp_all
     · rfl
-  · simp [map_zero]
-  · simp [Finset.mul_sum, h]
+  · 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

From be5cb4772a07f5286bc1d2884ef178815d42726c Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 7 May 2026 05:24:16 +0100
Subject: [PATCH 4/5] refactor: Lint

---
 Physlib/Relativity/Tensors/Basic.lean      | 6 +++---
 Physlib/Relativity/Tensors/Evaluation.lean | 1 +
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/Physlib/Relativity/Tensors/Basic.lean b/Physlib/Relativity/Tensors/Basic.lean
index 5bf47d92e..5be0b7896 100644
--- a/Physlib/Relativity/Tensors/Basic.lean
+++ b/Physlib/Relativity/Tensors/Basic.lean
@@ -836,18 +836,18 @@ lemma permT_basis {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
   rw [permT_basis_repr_symm_apply]
   simp [Finsupp.single_apply]
   congr 1
-  simp
+  simp only [eq_iff_iff]
   constructor
   · intro h
     rw [h]
     ext i
-    simp
+    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
+    simp only [basisIdxCongr_apply_apply]
     apply ComponentIdx.congr_right
     simp [PermCond.inv_apply_apply]
 
diff --git a/Physlib/Relativity/Tensors/Evaluation.lean b/Physlib/Relativity/Tensors/Evaluation.lean
index 56056b6e7..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

From 49d4ff2eecc9431835558c5547864205f8369077 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 12 May 2026 05:54:45 +0100
Subject: [PATCH 5/5] Apply suggestions from code review

Co-authored-by: Daniel Morrison <39346894+morrison-daniel@users.noreply.github.com>
---
 Physlib/Relativity/Tensors/Basic.lean         |  5 ++--
 .../Relativity/Tensors/Contraction/Basis.lean |  2 +-
 .../Relativity/Tensors/Contraction/Pure.lean  | 26 +++++++++----------
 Physlib/Relativity/Tensors/Evaluation.lean    |  6 ++---
 .../Relativity/Tensors/RealTensor/Basic.lean  | 20 +++++++-------
 5 files changed, 28 insertions(+), 31 deletions(-)

diff --git a/Physlib/Relativity/Tensors/Basic.lean b/Physlib/Relativity/Tensors/Basic.lean
index 5be0b7896..899848cb5 100644
--- a/Physlib/Relativity/Tensors/Basic.lean
+++ b/Physlib/Relativity/Tensors/Basic.lean
@@ -834,7 +834,7 @@ lemma permT_basis {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
   apply (basis c1).repr.injective
   ext b'
   rw [permT_basis_repr_symm_apply]
-  simp [Finsupp.single_apply]
+  simp only [Basis.repr_self, Finsupp.single_apply]
   congr 1
   simp only [eq_iff_iff]
   constructor
@@ -844,8 +844,7 @@ lemma permT_basis {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
     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]
+  · rintro rfl
     ext i
     simp only [basisIdxCongr_apply_apply]
     apply ComponentIdx.congr_right
diff --git a/Physlib/Relativity/Tensors/Contraction/Basis.lean b/Physlib/Relativity/Tensors/Contraction/Basis.lean
index 786bd7a8e..90340568f 100644
--- a/Physlib/Relativity/Tensors/Contraction/Basis.lean
+++ b/Physlib/Relativity/Tensors/Contraction/Basis.lean
@@ -232,7 +232,7 @@ lemma contrT_basis {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)}
     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]
+  simp only [basis_apply, contrT_pure, Pure.contrP, Pure.dropPair_basisVector]
   rfl
 
 end Tensor
diff --git a/Physlib/Relativity/Tensors/Contraction/Pure.lean b/Physlib/Relativity/Tensors/Contraction/Pure.lean
index 8a64a97bf..9e63adb61 100644
--- a/Physlib/Relativity/Tensors/Contraction/Pure.lean
+++ b/Physlib/Relativity/Tensors/Contraction/Pure.lean
@@ -82,22 +82,20 @@ lemma dropPairEmb_eq_succAbove_succAbove (i : Fin (n + 1 + 1)) (j : Fin (n + 1))
 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⟩
+  · contradiction
   · ext x
-    grind
-  · ext x
-    simp [dropPairEmb_eq_succAbove_succAbove]
+    rw [dropPairEmb_eq_succAbove_succAbove, Function.comp_apply]
     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
+    rcases eq_or_ne i 0 with rfl | hi
+    · rfl
+    · rw [Fin.predAbove_zero_of_ne_zero hi]
+      rcases lt_or_ge (i.pred hi).castSucc (i.succAbove j) with h | h
+      · rw [Fin.predAbove_of_castSucc_lt _ _ h, Fin.pred_succAbove]
+        rw [← Fin.lt_succAbove_iff_le_castSucc]
+        exact lt_of_le_of_ne ((Fin.castSucc_pred_lt_iff hi).mp h) hij
+      · rw [Fin.predAbove_of_le_castSucc _ _ h, Fin.castPred_succAbove]
+        rw [Fin.castSucc_lt_iff_succ_le, ← Fin.succAbove_lt_iff_succ_le]
+        exact (Fin.le_castSucc_pred_iff hi).mp h
 
 lemma dropPairEmb_injective {n : ℕ}
     (i j : Fin (n + 1 + 1)) : Function.Injective (dropPairEmb i j) := by
diff --git a/Physlib/Relativity/Tensors/Evaluation.lean b/Physlib/Relativity/Tensors/Evaluation.lean
index 3a97d8cd6..d5476b087 100644
--- a/Physlib/Relativity/Tensors/Evaluation.lean
+++ b/Physlib/Relativity/Tensors/Evaluation.lean
@@ -141,11 +141,11 @@ lemma evalT_pure {n : ℕ} {c : Fin (n + 1) → C} (i : Fin (n + 1))
   rfl
 
 lemma evalT_basis {n : ℕ} {c : Fin (n + 1) → C} (i : Fin (n + 1))
-    (b : ComponentIdx c)
-    (x : basisIdx (c i)) :
+    (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]
+  simp only [basis_apply, evalT_pure, Pure.evalP, Pure.evalPCoeff_basisVector, ite_smul, one_smul,
+    zero_smul]
   rfl
 
 TODO "Add lemmas related to the interaction of evalT and permT, prodT and contrT."
diff --git a/Physlib/Relativity/Tensors/RealTensor/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
index 027bd1a13..7e274b55b 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Basic.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
@@ -244,11 +244,12 @@ lemma contrT_basis_repr_apply_eq_fin {n d: ℕ} {c : Fin (n + 1 + 1) → realLor
 
 attribute [-simp] Fintype.sum_sum_type
 
-lemma contrPCoeff_basis {d : ℕ} {c : Fin n → realLorentzTensor.Color} (i j : Fin n)
+lemma contrPCoeff_basis {d n : ℕ} {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]
+  simp only [Pure.contrPCoeff, Monoidal.tensorUnit_obj, Rep.tensorUnit_V, Rep.tensorUnit_ρ,
+    Functor.comp_obj, Discrete.functor_obj_eq_as, Function.comp_apply, Pure.basisVector]
   generalize b i = b1 at *
   generalize b j = b2 at *
   suffices h : ∀ c, ∀ c1,  (hc : (realLorentzTensor d).τ c = c1) →
@@ -259,8 +260,7 @@ lemma contrPCoeff_basis {d : ℕ} {c : Fin n → realLorentzTensor.Color} (i j :
       (((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
+  rintro c c1 rfl
   exact contr_basis _ _
 
 lemma contrT_eq_sum_evalT {n} {d} (c : Fin (n + 1 + 1) → Color) (i j : Fin (n + 1 + 1))
@@ -281,14 +281,15 @@ lemma contrT_eq_sum_evalT {n} {d} (c : Fin (n + 1 + 1) → Color) (i j : Fin (n
       · rw [Fin.predAbove_zero_succ]
         exact Fin.succ_succAbove_predAbove (Ne.symm h.1)
     rw [h0]
-    split_ifs
+    split_ifs with h₁ _ h₂
     · rw [permT_basis]
       congr
       ext x
-      simp [ComponentIdx.dropPair]
+      simp only [Function.comp_apply, ComponentIdx.dropPair, id_eq, basisIdxCongr_eq_refl,
+        Equiv.refl_apply]
       rw [Pure.dropPairEmb_eq_predAbove h.1]
-    · simp_all
-    · simp_all
+    · symm at h₁; contradiction
+    · symm at h₂; contradiction
     · rfl
   · simp
   · simp [Finset.smul_sum, h]
@@ -297,8 +298,7 @@ lemma contrT_eq_sum_evalT {n} {d} (c : Fin (n + 1 + 1) → Color) (i j : Fin (n
 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]
+  rw [contrT_eq_sum_evalT, map_sum, Tensorial.self_toTensor_apply]
   congr
   ext μ
   simp only [toField_permT]