diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Metric.lean b/HepLean/SpaceTime/LorentzVector/Complex/Metric.lean
index 342977a..58a587b 100644
--- a/HepLean/SpaceTime/LorentzVector/Complex/Metric.lean
+++ b/HepLean/SpaceTime/LorentzVector/Complex/Metric.lean
@@ -24,6 +24,23 @@ namespace Lorentz
 def contrMetricVal : (complexContr ⊗ complexContr).V :=
   contrContrToMatrix.symm ((@minkowskiMatrix 3).map ofReal)
 
+/-- The expansion of `contrMetricVal` into basis vectors. -/
+lemma contrMetricVal_expand_tmul : contrMetricVal =
+    complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)
+    - complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)
+    - complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)
+    - complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, contrMetricVal, Fin.isValue]
+  erw [contrContrToMatrix_symm_expand_tmul]
+  simp only [map_apply, ofReal_eq_coe, coe_smul, Fintype.sum_sum_type, Finset.univ_unique,
+    Fin.default_eq_zero, Fin.isValue, Finset.sum_singleton, Fin.sum_univ_three, ne_eq, reduceCtorEq,
+    not_false_eq_true, minkowskiMatrix.off_diag_zero, zero_smul, add_zero, zero_add, Sum.inr.injEq,
+    zero_ne_one, Fin.reduceEq, one_ne_zero]
+  rw [minkowskiMatrix.inl_0_inl_0, minkowskiMatrix.inr_i_inr_i,
+    minkowskiMatrix.inr_i_inr_i, minkowskiMatrix.inr_i_inr_i]
+  simp only [Fin.isValue, one_smul, neg_smul]
+  rfl
+
 /-- The metric `ηᵃᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexContr`,
   making its invariance under the action of `SL(2,ℂ)`. -/
 def contrMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexContr where
@@ -51,10 +68,16 @@ def contrMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexContr wh
     apply congrArg
     simp only [LorentzGroup.toComplex_mul_minkowskiMatrix_mul_transpose]
 
+lemma contrMetric_apply_one : contrMetric.hom (1 : ℂ) = contrMetricVal := by
+  change contrMetric.hom.toFun (1 : ℂ) = contrMetricVal
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    contrMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
+
 /-- The metric `ηᵢᵢ` as an element of `(complexCo ⊗ complexCo).V`. -/
 def coMetricVal : (complexCo ⊗ complexCo).V :=
   coCoToMatrix.symm ((@minkowskiMatrix 3).map ofReal)
 
+/-- The expansion of `coMetricVal` into basis vectors. -/
 lemma coMetricVal_expand_tmul : coMetricVal =
     complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)
     - complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)
@@ -102,7 +125,8 @@ def coMetric : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexCo where
 
 lemma coMetric_apply_one : coMetric.hom (1 : ℂ) = coMetricVal := by
   change coMetric.hom.toFun (1 : ℂ) = coMetricVal
-  simp [coMetric]
+  simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    coMetric, AddHom.toFun_eq_coe, AddHom.coe_mk, one_smul]
 
 end Lorentz
 end
diff --git a/HepLean/SpaceTime/LorentzVector/Complex/Two.lean b/HepLean/SpaceTime/LorentzVector/Complex/Two.lean
index a76f3d0..57388d4 100644
--- a/HepLean/SpaceTime/LorentzVector/Complex/Two.lean
+++ b/HepLean/SpaceTime/LorentzVector/Complex/Two.lean
@@ -27,6 +27,19 @@ def contrContrToMatrix : (complexContr ⊗ complexContr).V ≃ₗ[ℂ]
   Finsupp.linearEquivFunOnFinite ℂ ℂ ((Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3)
 
+/-- Expanding `contrContrToMatrix` in terms of the standard basis. -/
+lemma contrContrToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ) :
+    contrContrToMatrix.symm M =
+    ∑ i, ∑ j, M i j • (complexContrBasis i ⊗ₜ[ℂ] complexContrBasis j) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, contrContrToMatrix, LinearEquiv.trans_symm,
+    LinearEquiv.trans_apply, Basis.repr_symm_apply]
+  rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
+  · erw [Finset.sum_product]
+    refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
+    erw [Basis.tensorProduct_apply complexContrBasis complexContrBasis i j]
+    rfl
+  · simp
+
 /-- Equivalence of `complexCo ⊗ complexCo` to `4 x 4` complex matrices. -/
 def coCoToMatrix : (complexCo ⊗ complexCo).V ≃ₗ[ℂ]
     Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=
diff --git a/HepLean/SpaceTime/WeylFermion/Two.lean b/HepLean/SpaceTime/WeylFermion/Two.lean
index d46a514..fa1a046 100644
--- a/HepLean/SpaceTime/WeylFermion/Two.lean
+++ b/HepLean/SpaceTime/WeylFermion/Two.lean
@@ -33,60 +33,180 @@ def leftLeftToMatrix : (leftHanded ⊗ leftHanded).V ≃ₗ[ℂ] Matrix (Fin 2)
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
+/-- Expanding `leftLeftToMatrix` in terms of the standard basis. -/
+lemma leftLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
+    leftLeftToMatrix.symm M = ∑ i, ∑ j, M i j • (leftBasis i ⊗ₜ[ℂ] leftBasis j) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, leftLeftToMatrix,
+    LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
+  rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
+  · erw [Finset.sum_product]
+    refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
+    erw [Basis.tensorProduct_apply leftBasis leftBasis i j]
+    rfl
+  · simp
+
 /-- Equivalence of `altLeftHanded ⊗ altLeftHanded` to `2 x 2` complex matrices. -/
 def altLeftaltLeftToMatrix : (altLeftHanded ⊗ altLeftHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
   (Basis.tensorProduct altLeftBasis altLeftBasis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
+/-- Expanding `altLeftaltLeftToMatrix` in terms of the standard basis. -/
+lemma altLeftaltLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
+    altLeftaltLeftToMatrix.symm M = ∑ i, ∑ j, M i j • (altLeftBasis i ⊗ₜ[ℂ] altLeftBasis j) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, altLeftaltLeftToMatrix,
+    LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
+  rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
+  · erw [Finset.sum_product]
+    refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
+    erw [Basis.tensorProduct_apply altLeftBasis altLeftBasis i j]
+    rfl
+  · simp
+
 /-- Equivalence of `leftHanded ⊗ altLeftHanded` to `2 x 2` complex matrices. -/
 def leftAltLeftToMatrix : (leftHanded ⊗ altLeftHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
   (Basis.tensorProduct leftBasis altLeftBasis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
+/-- Expanding `leftAltLeftToMatrix` in terms of the standard basis. -/
+lemma leftAltLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
+    leftAltLeftToMatrix.symm M = ∑ i, ∑ j, M i j • (leftBasis i ⊗ₜ[ℂ] altLeftBasis j) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, leftAltLeftToMatrix,
+    LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
+  rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
+  · erw [Finset.sum_product]
+    refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
+    erw [Basis.tensorProduct_apply leftBasis altLeftBasis i j]
+    rfl
+  · simp
+
 /-- Equivalence of `altLeftHanded ⊗ leftHanded` to `2 x 2` complex matrices. -/
 def altLeftLeftToMatrix : (altLeftHanded ⊗ leftHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
   (Basis.tensorProduct altLeftBasis leftBasis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
+/-- Expanding `altLeftLeftToMatrix` in terms of the standard basis. -/
+lemma altLeftLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
+    altLeftLeftToMatrix.symm M = ∑ i, ∑ j, M i j • (altLeftBasis i ⊗ₜ[ℂ] leftBasis j) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, altLeftLeftToMatrix,
+    LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
+  rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
+  · erw [Finset.sum_product]
+    refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
+    erw [Basis.tensorProduct_apply altLeftBasis leftBasis i j]
+    rfl
+  · simp
+
 /-- Equivalence of `rightHanded ⊗ rightHanded` to `2 x 2` complex matrices. -/
 def rightRightToMatrix : (rightHanded ⊗ rightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
   (Basis.tensorProduct rightBasis rightBasis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
+/-- Expanding `rightRightToMatrix` in terms of the standard basis. -/
+lemma rightRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
+    rightRightToMatrix.symm M = ∑ i, ∑ j, M i j • (rightBasis i ⊗ₜ[ℂ] rightBasis j) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, rightRightToMatrix,
+    LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
+  rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
+  · erw [Finset.sum_product]
+    refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
+    erw [Basis.tensorProduct_apply rightBasis rightBasis i j]
+    rfl
+  · simp
+
 /-- Equivalence of `altRightHanded ⊗ altRightHanded` to `2 x 2` complex matrices. -/
 def altRightAltRightToMatrix : (altRightHanded ⊗ altRightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
   (Basis.tensorProduct altRightBasis altRightBasis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
+/-- Expanding `altRightAltRightToMatrix` in terms of the standard basis. -/
+lemma altRightAltRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
+    altRightAltRightToMatrix.symm M = ∑ i, ∑ j, M i j • (altRightBasis i ⊗ₜ[ℂ] altRightBasis j) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, altRightAltRightToMatrix,
+    LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
+  rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
+  · erw [Finset.sum_product]
+    refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
+    erw [Basis.tensorProduct_apply altRightBasis altRightBasis i j]
+    rfl
+  · simp
+
 /-- Equivalence of `rightHanded ⊗ altRightHanded` to `2 x 2` complex matrices. -/
 def rightAltRightToMatrix : (rightHanded ⊗ altRightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
   (Basis.tensorProduct rightBasis altRightBasis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
+/-- Expanding `rightAltRightToMatrix` in terms of the standard basis. -/
+lemma rightAltRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
+    rightAltRightToMatrix.symm M = ∑ i, ∑ j, M i j • (rightBasis i ⊗ₜ[ℂ] altRightBasis j) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, rightAltRightToMatrix, LinearEquiv.trans_symm,
+    LinearEquiv.trans_apply, Basis.repr_symm_apply]
+  rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
+  · erw [Finset.sum_product]
+    refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
+    erw [Basis.tensorProduct_apply rightBasis altRightBasis i j]
+    rfl
+  · simp
+
 /-- Equivalence of `altRightHanded ⊗ rightHanded` to `2 x 2` complex matrices. -/
 def altRightRightToMatrix : (altRightHanded ⊗ rightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
   (Basis.tensorProduct altRightBasis rightBasis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
+/-- Expanding `altRightRightToMatrix` in terms of the standard basis. -/
+lemma altRightRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
+    altRightRightToMatrix.symm M = ∑ i, ∑ j, M i j • (altRightBasis i ⊗ₜ[ℂ] rightBasis j) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, altRightRightToMatrix, LinearEquiv.trans_symm,
+    LinearEquiv.trans_apply, Basis.repr_symm_apply]
+  rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
+  · erw [Finset.sum_product]
+    refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
+    erw [Basis.tensorProduct_apply altRightBasis rightBasis i j]
+    rfl
+  · simp
+
 /-- Equivalence of `altLeftHanded ⊗ altRightHanded` to `2 x 2` complex matrices. -/
 def altLeftAltRightToMatrix : (altLeftHanded ⊗ altRightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
   (Basis.tensorProduct altLeftBasis altRightBasis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
+/-- Expanding `altLeftAltRightToMatrix` in terms of the standard basis. -/
+lemma altLeftAltRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
+    altLeftAltRightToMatrix.symm M = ∑ i, ∑ j, M i j • (altLeftBasis i ⊗ₜ[ℂ] altRightBasis j) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, altLeftAltRightToMatrix,
+    LinearEquiv.trans_symm, LinearEquiv.trans_apply, Basis.repr_symm_apply]
+  rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
+  · erw [Finset.sum_product]
+    refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
+    erw [Basis.tensorProduct_apply altLeftBasis altRightBasis i j]
+    rfl
+  · simp
+
 /-- Equivalence of `leftHanded ⊗ rightHanded` to `2 x 2` complex matrices. -/
 def leftRightToMatrix : (leftHanded ⊗ rightHanded).V ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
   (Basis.tensorProduct leftBasis rightBasis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
+/-- Expanding `leftRightToMatrix` in terms of the standard basis. -/
+lemma leftRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
+    leftRightToMatrix.symm M = ∑ i, ∑ j, M i j • (leftBasis i ⊗ₜ[ℂ] rightBasis j) := by
+  simp only [Action.instMonoidalCategory_tensorObj_V, leftRightToMatrix, LinearEquiv.trans_symm,
+    LinearEquiv.trans_apply, Basis.repr_symm_apply]
+  rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
+  · erw [Finset.sum_product]
+    refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
+    erw [Basis.tensorProduct_apply leftBasis rightBasis i j]
+    rfl
+  · simp
+
 /-!
 
 ## Group actions
diff --git a/HepLean/Tensors/ComplexLorentz/Basis.lean b/HepLean/Tensors/ComplexLorentz/Basis.lean
index 6833eb4..3057f4f 100644
--- a/HepLean/Tensors/ComplexLorentz/Basis.lean
+++ b/HepLean/Tensors/ComplexLorentz/Basis.lean
@@ -42,8 +42,14 @@ def basisVector {n : ℕ} (c : Fin n → complexLorentzTensor.C)
     complexLorentzTensor.F.obj (OverColor.mk c) :=
   PiTensorProduct.tprod ℂ (fun i => complexLorentzTensor.basis (c i) (b i))
 
+/-!
+
+## Useful expansions.
+
+-/
+
 /-- The expansion of the Lorentz covariant metric in terms of basis vectors. -/
-lemma coMetric_expand : {Lorentz.coMetric | μ ν}ᵀ.tensor =
+lemma coMetric_basis_expand : {Lorentz.coMetric | μ ν}ᵀ.tensor =
     basisVector ![Color.down, Color.down] (fun _ => 0)
     - basisVector ![Color.down, Color.down] (fun _ => 1)
     - basisVector ![Color.down, Color.down] (fun _ => 2)
@@ -68,6 +74,32 @@ lemma coMetric_expand : {Lorentz.coMetric | μ ν}ᵀ.tensor =
       simp only [Fin.isValue, Lorentz.complexCoBasisFin4, Basis.coe_reindex, Function.comp_apply]
       rfl
 
+/-- The expansion of the Lorentz contrvariant metric in terms of basis vectors. -/
+lemma contrMatrix_basis_expand : {Lorentz.contrMetric | μ ν}ᵀ.tensor =
+    basisVector ![Color.up, Color.up] (fun _ => 0)
+    - basisVector ![Color.up, Color.up] (fun _ => 1)
+    - basisVector ![Color.up, Color.up] (fun _ => 2)
+    - basisVector ![Color.up, Color.up] (fun _ => 3) := by
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, constTwoNode_tensor,
+    Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
+    Functor.id_obj, Fin.isValue]
+  erw [Lorentz.contrMetric_apply_one, Lorentz.contrMetricVal_expand_tmul]
+  simp only [Fin.isValue, map_sub]
+  congr 1
+  congr 1
+  congr 1
+  all_goals
+    erw [pairIsoSep_tmul, basisVector]
+    apply congrArg
+    funext i
+    fin_cases i
+    all_goals
+      simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, OverColor.mk_hom,
+        cons_val_zero, Fin.cases_zero]
+      change _ = Lorentz.complexContrBasisFin4 _
+      simp only [Fin.isValue, Lorentz.complexContrBasisFin4, Basis.coe_reindex, Function.comp_apply]
+      rfl
+
 end complexLorentzTensor
 end Fermion
 end
diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean
index 561ded5..a8da69f 100644
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.lean
@@ -203,6 +203,11 @@ def specialTypes : List (String × (Term → Term)) := [
       mkIdent ``Fermion.complexLorentzTensor,
       mkIdent ``Fermion.Color.down,
       mkIdent ``Fermion.Color.down, T]),
+  ("𝟙_ (Rep ℂ SL(2, ℂ)) ⟶ Lorentz.complexContr ⊗ Lorentz.complexContr", fun T =>
+    Syntax.mkApp (mkIdent ``TensorTree.constTwoNodeE) #[
+      mkIdent ``Fermion.complexLorentzTensor,
+      mkIdent ``Fermion.Color.up,
+      mkIdent ``Fermion.Color.up, T]),
   ("𝟙_ (Rep ℂ SL(2, ℂ)) ⟶ Lorentz.complexContr ⊗ Fermion.leftHanded ⊗ Fermion.rightHanded", fun T =>
     Syntax.mkApp (mkIdent ``TensorTree.constThreeNodeE) #[
       mkIdent ``Fermion.complexLorentzTensor, mkIdent ``Fermion.Color.up,