diff --git a/Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean b/Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean
index 0885e9f98..3363a4380 100644
--- a/Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean
+++ b/Physlib/Particles/StandardModel/Fermions/QuarkDoublet.lean
@@ -89,7 +89,7 @@ open Representation in
 noncomputable def repLorentzGroup : Representation ℂ (SL(2,ℂ)) QuarkDoublet where
   toFun Λ :=  valLinEquiv.symm ∘ₗ
       TensorProduct.map
-      (TensorProduct.map (Fermion.leftHandedRep Λ)
+      (TensorProduct.map (Fermion.LeftHandedWeyl.rep Λ)
         (trivial ℂ (SL(2,ℂ)) (EuclideanSpace ℂ (Fin 3)) Λ))
         (trivial ℂ (SL(2,ℂ)) (EuclideanSpace ℂ (Fin 2)) Λ)
       ∘ₗ valLinEquiv
diff --git a/Physlib/Relativity/PauliMatrices/AsTensor.lean b/Physlib/Relativity/PauliMatrices/AsTensor.lean
index d1fcdbb6f..9c29bc6d8 100644
--- a/Physlib/Relativity/PauliMatrices/AsTensor.lean
+++ b/Physlib/Relativity/PauliMatrices/AsTensor.lean
@@ -47,39 +47,43 @@ lemma asTensor_expand_complexContrBasis : asTensor =
 
 /-- The expansion of the pauli matrix `σ₀` in terms of a basis of tensor product vectors. -/
 lemma leftRightToMatrix_σSA_inl_0_expand : leftRightToMatrix.symm (pauliBasis (Sum.inl 0)) =
-    leftBasis 0 ⊗ₜ rightBasis 0 + leftBasis 1 ⊗ₜ rightBasis 1 := by
+    LeftHandedWeyl.basis 0 ⊗ₜ RightHandedWeyl.basis 0 +
+      LeftHandedWeyl.basis 1 ⊗ₜ RightHandedWeyl.basis 1 := by
   rw [leftRightToMatrix_symm_expand_tmul]
   simp [pauliBasis, pauliSelfAdjoint, pauliMatrix]
 
 /-- The expansion of the pauli matrix `σ₁` in terms of a basis of tensor product vectors. -/
 lemma leftRightToMatrix_σSA_inr_0_expand : leftRightToMatrix.symm (pauliBasis (Sum.inr 0)) =
-    leftBasis 0 ⊗ₜ rightBasis 1 + leftBasis 1 ⊗ₜ rightBasis 0:= by
+    LeftHandedWeyl.basis 0 ⊗ₜ RightHandedWeyl.basis 1 +
+      LeftHandedWeyl.basis 1 ⊗ₜ RightHandedWeyl.basis 0:= by
   rw [leftRightToMatrix_symm_expand_tmul]
   simp [pauliBasis, pauliSelfAdjoint, pauliMatrix]
 
 /-- The expansion of the pauli matrix `σ₂` in terms of a basis of tensor product vectors. -/
 lemma leftRightToMatrix_σSA_inr_1_expand : leftRightToMatrix.symm (pauliBasis (Sum.inr 1)) =
-    -(I • leftBasis 0 ⊗ₜ[ℂ] rightBasis 1) + I • leftBasis 1 ⊗ₜ[ℂ] rightBasis 0 := by
+    -(I • LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1) +
+      I • LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 := by
   simp [leftRightToMatrix_symm_expand_tmul, pauliBasis, pauliSelfAdjoint, pauliMatrix]
   module
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The expansion of the pauli matrix `σ₃` in terms of a basis of tensor product vectors. -/
 lemma leftRightToMatrix_σSA_inr_2_expand : leftRightToMatrix.symm (pauliBasis (Sum.inr 2)) =
-    leftBasis 0 ⊗ₜ rightBasis 0 - leftBasis 1 ⊗ₜ rightBasis 1 := by
+    LeftHandedWeyl.basis 0 ⊗ₜ RightHandedWeyl.basis 0 -
+      LeftHandedWeyl.basis 1 ⊗ₜ RightHandedWeyl.basis 1 := by
   simp [leftRightToMatrix_symm_expand_tmul, pauliBasis, pauliSelfAdjoint, pauliMatrix]
   module
 
 /-- The expansion of `asTensor` into complexContrBasis basis of tensor product vectors. -/
 lemma asTensor_expand : asTensor =
-    complexContrBasis (Sum.inl 0) ⊗ₜ (leftBasis 0 ⊗ₜ rightBasis 0)
-    + complexContrBasis (Sum.inl 0) ⊗ₜ (leftBasis 1 ⊗ₜ rightBasis 1)
-    + complexContrBasis (Sum.inr 0) ⊗ₜ (leftBasis 0 ⊗ₜ rightBasis 1)
-    + complexContrBasis (Sum.inr 0) ⊗ₜ (leftBasis 1 ⊗ₜ rightBasis 0)
-    - I • complexContrBasis (Sum.inr 1) ⊗ₜ (leftBasis 0 ⊗ₜ rightBasis 1)
-    + I • complexContrBasis (Sum.inr 1) ⊗ₜ (leftBasis 1 ⊗ₜ rightBasis 0)
-    + complexContrBasis (Sum.inr 2) ⊗ₜ (leftBasis 0 ⊗ₜ rightBasis 0)
-    - complexContrBasis (Sum.inr 2) ⊗ₜ (leftBasis 1 ⊗ₜ rightBasis 1) := by
+    complexContrBasis (Sum.inl 0) ⊗ₜ (LeftHandedWeyl.basis 0 ⊗ₜ RightHandedWeyl.basis 0)
+    + complexContrBasis (Sum.inl 0) ⊗ₜ (LeftHandedWeyl.basis 1 ⊗ₜ RightHandedWeyl.basis 1)
+    + complexContrBasis (Sum.inr 0) ⊗ₜ (LeftHandedWeyl.basis 0 ⊗ₜ RightHandedWeyl.basis 1)
+    + complexContrBasis (Sum.inr 0) ⊗ₜ (LeftHandedWeyl.basis 1 ⊗ₜ RightHandedWeyl.basis 0)
+    - I • complexContrBasis (Sum.inr 1) ⊗ₜ (LeftHandedWeyl.basis 0 ⊗ₜ RightHandedWeyl.basis 1)
+    + I • complexContrBasis (Sum.inr 1) ⊗ₜ (LeftHandedWeyl.basis 1 ⊗ₜ RightHandedWeyl.basis 0)
+    + complexContrBasis (Sum.inr 2) ⊗ₜ (LeftHandedWeyl.basis 0 ⊗ₜ RightHandedWeyl.basis 0)
+    - complexContrBasis (Sum.inr 2) ⊗ₜ (LeftHandedWeyl.basis 1 ⊗ₜ RightHandedWeyl.basis 1) := by
   rw [asTensor_expand_complexContrBasis]
   rw [leftRightToMatrix_σSA_inl_0_expand, leftRightToMatrix_σSA_inr_0_expand,
     leftRightToMatrix_σSA_inr_1_expand, leftRightToMatrix_σSA_inr_2_expand]
@@ -92,7 +96,7 @@ set_option backward.isDefEq.respectTransparency false in
   the invariance under the `SL(2,ℂ)` action. -/
 def asConsTensor :
     (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
-    (ContrℂModule.SL2CRep.tprod (leftHandedRep.tprod rightHandedRep)) where
+    (ContrℂModule.SL2CRep.tprod (LeftHandedWeyl.rep.tprod RightHandedWeyl.rep)) where
 
     toFun := fun a =>
       let a' : ℂ := a
@@ -106,7 +110,7 @@ def asConsTensor :
       refine LinearMap.ext fun x : ℂ => ?_
       change x • asTensor =
         (TensorProduct.map (ContrℂModule.SL2CRep M)
-          (TensorProduct.map (leftHandedRep M) (rightHandedRep M))) (x • asTensor)
+          (TensorProduct.map (LeftHandedWeyl.rep M) (RightHandedWeyl.rep M))) (x • asTensor)
       simp only [map_smul]
       apply congrArg
       nth_rewrite 2 [asTensor]
diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Basic.lean b/Physlib/Relativity/Tensors/ComplexTensor/Basic.lean
index df59945b5..472983f5f 100644
--- a/Physlib/Relativity/Tensors/ComplexTensor/Basic.lean
+++ b/Physlib/Relativity/Tensors/ComplexTensor/Basic.lean
@@ -130,17 +130,17 @@ def complexLorentzTensor : TensorSpecies ℂ complexLorentzTensor.Color SL(2, 
       | Color.down => Lorentz.CoℂModule)
     (fun c => Fin (repDim c))
     (fun c => match c with
-      | Color.upL => Fermion.leftHandedRep
-      | Color.downL => Fermion.dualLeftHandedRep
-      | Color.upR => Fermion.rightHandedRep
-      | Color.downR => Fermion.dualRightHandedRep
+      | Color.upL => Fermion.LeftHandedWeyl.rep
+      | Color.downL => Fermion.DualLeftHandedWeyl.rep
+      | Color.upR => Fermion.RightHandedWeyl.rep
+      | Color.downR => Fermion.DualRightHandedWeyl.rep
       | Color.up => Lorentz.ContrℂModule.SL2CRep
       | Color.down => Lorentz.CoℂModule.SL2CRep)
     (fun c => match c with
-    | Color.upL => Fermion.leftBasis
-    | Color.downL => Fermion.dualLeftBasis
-    | Color.upR => Fermion.rightBasis
-    | Color.downR => Fermion.dualRightBasis
+    | Color.upL => Fermion.LeftHandedWeyl.basis
+    | Color.downL => Fermion.DualLeftHandedWeyl.basis
+    | Color.upR => Fermion.RightHandedWeyl.basis
+    | Color.downR => Fermion.DualRightHandedWeyl.basis
     | Color.up => Lorentz.complexContrBasisFin4
     | Color.down => Lorentz.complexCoBasisFin4) where
 
@@ -231,20 +231,20 @@ syntax (name := complexLorentzTensorSyntax) "ℂT[" term,* "]" : term
 /-- The basis associated with each of the different types of complex Lorentz vector space. -/
 abbrev basis (c : Color) : Module.Basis (Fin (repDim c)) ℂ (modules c) :=
   match c with
-  | Color.upL => Fermion.leftBasis
-  | Color.downL => Fermion.dualLeftBasis
-  | Color.upR => Fermion.rightBasis
-  | Color.downR => Fermion.dualRightBasis
+  | Color.upL => Fermion.LeftHandedWeyl.basis
+  | Color.downL => Fermion.DualLeftHandedWeyl.basis
+  | Color.upR => Fermion.RightHandedWeyl.basis
+  | Color.downR => Fermion.DualRightHandedWeyl.basis
   | Color.up => Lorentz.complexContrBasisFin4
   | Color.down => Lorentz.complexCoBasisFin4
 
 /-- The reps associated with each of the different types of complex Lorentz vector space. -/
 abbrev rep (c : Color) : Representation ℂ SL(2, ℂ) (modules c) :=
   match c with
-  | Color.upL => Fermion.leftHandedRep
-  | Color.downL => Fermion.dualLeftHandedRep
-  | Color.upR => Fermion.rightHandedRep
-  | Color.downR => Fermion.dualRightHandedRep
+  | Color.upL => Fermion.LeftHandedWeyl.rep
+  | Color.downL => Fermion.DualLeftHandedWeyl.rep
+  | Color.upR => Fermion.RightHandedWeyl.rep
+  | Color.downR => Fermion.DualRightHandedWeyl.rep
   | Color.up => Lorentz.ContrℂModule.SL2CRep
   | Color.down => Lorentz.CoℂModule.SL2CRep
 
diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Metrics/Basic.lean b/Physlib/Relativity/Tensors/ComplexTensor/Metrics/Basic.lean
index d9f832f19..6d1977dba 100644
--- a/Physlib/Relativity/Tensors/ComplexTensor/Metrics/Basic.lean
+++ b/Physlib/Relativity/Tensors/ComplexTensor/Metrics/Basic.lean
@@ -183,30 +183,30 @@ lemma contrMetric_eq_complexContrBasisFin4 : η =
   rfl
 
 open Fermion in
-lemma leftMetric_eq_leftBasis : εL =
-    - fromPairT (leftBasis 0 ⊗ₜ[ℂ] leftBasis 1)
-    + fromPairT (leftBasis 1 ⊗ₜ[ℂ] leftBasis 0) := by
+lemma leftMetric_eq_leftHandedWeyl_basis : εL =
+    - fromPairT (LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1)
+    + fromPairT (LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] LeftHandedWeyl.basis 0) := by
   rw [leftMetric_eq_fromPairT, leftMetricVal_expand_tmul]
   simp
 
 open Fermion in
-lemma dualLeftMetric_eq_dualLeftBasis : εL' =
-    fromPairT (dualLeftBasis 0 ⊗ₜ[ℂ] dualLeftBasis 1)
-    - fromPairT (dualLeftBasis 1 ⊗ₜ[ℂ] dualLeftBasis 0) := by
+lemma dualLeftMetric_eq_dualLeftHandedWeyl_basis : εL' =
+    fromPairT (DualLeftHandedWeyl.basis 0 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 1)
+    - fromPairT (DualLeftHandedWeyl.basis 1 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 0) := by
   rw [dualLeftMetric_eq_fromPairT, dualLeftMetricVal_expand_tmul]
   simp
 
 open Fermion in
-lemma rightMetric_eq_rightBasis : εR =
-    - fromPairT (rightBasis 0 ⊗ₜ[ℂ] rightBasis 1)
-    + fromPairT (rightBasis 1 ⊗ₜ[ℂ] rightBasis 0) := by
+lemma rightMetric_eq_rightHandedWeyl_basis : εR =
+    - fromPairT (RightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1)
+    + fromPairT (RightHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0) := by
   rw [rightMetric_eq_fromPairT, rightMetricVal_expand_tmul]
   simp
 
 open Fermion in
-lemma dualRightMetric_eq_dualRightBasis : εR' =
-    fromPairT (dualRightBasis 0 ⊗ₜ[ℂ] dualRightBasis 1)
-    - fromPairT (dualRightBasis 1 ⊗ₜ[ℂ] dualRightBasis 0) := by
+lemma dualRightMetric_eq_dualRightHandedWeyl_basis : εR' =
+    fromPairT (DualRightHandedWeyl.basis 0 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 1)
+    - fromPairT (DualRightHandedWeyl.basis 1 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 0) := by
   rw [dualRightMetric_eq_fromPairT, dualRightMetricVal_expand_tmul]
   simp
 
@@ -272,7 +272,7 @@ lemma leftMetric_eq_basis : εL =
       (fun | 0 => (0 : Fin 2) | 1 => (1 : Fin 2)))
     + (Tensor.basis (S := complexLorentzTensor)
       ![Color.upL, Color.upL] (fun | 0 => (1 : Fin 2) | 1 => (0 : Fin 2))) := by
-  rw [leftMetric_eq_leftBasis]
+  rw [leftMetric_eq_leftHandedWeyl_basis]
   conv_lhs =>
     enter [2]
     erw [fromPairT_apply_basis_repr]
@@ -287,7 +287,7 @@ lemma dualLeftMetric_eq_basis : εL' =
       (fun | 0 => (0 : Fin 2) | 1 => (1 : Fin 2)))
     - (Tensor.basis (S := complexLorentzTensor)
       ![Color.downL, Color.downL] (fun | 0 => (1 : Fin 2) | 1 => (0 : Fin 2))) := by
-  rw [dualLeftMetric_eq_dualLeftBasis]
+  rw [dualLeftMetric_eq_dualLeftHandedWeyl_basis]
   conv_lhs =>
     enter [2]
     erw [fromPairT_apply_basis_repr]
@@ -302,7 +302,7 @@ lemma rightMetric_eq_basis : εR =
       (fun | 0 => (0 : Fin 2) | 1 => (1 : Fin 2)))
     + (Tensor.basis (S := complexLorentzTensor)
       ![Color.upR, Color.upR] (fun | 0 => (1 : Fin 2) | 1 => (0 : Fin 2))) := by
-  rw [rightMetric_eq_rightBasis]
+  rw [rightMetric_eq_rightHandedWeyl_basis]
   conv_lhs =>
     enter [2]
     erw [fromPairT_apply_basis_repr]
@@ -317,7 +317,7 @@ lemma dualRightMetric_eq_basis : εR' =
       ![Color.downR, Color.downR] (fun | 0 => (0 : Fin 2) | 1 => (1 : Fin 2)))
     - (Tensor.basis (S := complexLorentzTensor)
       ![Color.downR, Color.downR] (fun | 0 => (1 : Fin 2) | 1 => (0 : Fin 2))) := by
-  rw [dualRightMetric_eq_dualRightBasis]
+  rw [dualRightMetric_eq_dualRightHandedWeyl_basis]
   conv_lhs =>
     enter [2]
     erw [fromPairT_apply_basis_repr]
diff --git a/Physlib/Relativity/Tensors/ComplexTensor/OfRat.lean b/Physlib/Relativity/Tensors/ComplexTensor/OfRat.lean
index 5490f8761..b9c9c9ef0 100644
--- a/Physlib/Relativity/Tensors/ComplexTensor/OfRat.lean
+++ b/Physlib/Relativity/Tensors/ComplexTensor/OfRat.lean
@@ -76,19 +76,23 @@ lemma contr_basis_ratComplexNum {c : complexLorentzTensor.Color}
       = toComplexNum (if i.val = j.val then 1 else 0) := by
   match c with
   | Color.upL =>
-    change Fermion.leftDualContraction (Fermion.leftBasis i ⊗ₜ Fermion.dualLeftBasis j) = _
+    change Fermion.leftDualContraction
+      (Fermion.LeftHandedWeyl.basis i ⊗ₜ Fermion.DualLeftHandedWeyl.basis j) = _
     rw [Fermion.leftDualContraction_basis]
     simp
   | Color.downL =>
-    change Fermion.dualLeftContraction (Fermion.dualLeftBasis i ⊗ₜ Fermion.leftBasis j) = _
+    change Fermion.dualLeftContraction
+      (Fermion.DualLeftHandedWeyl.basis i ⊗ₜ Fermion.LeftHandedWeyl.basis j) = _
     rw [Fermion.dualLeftContraction_basis]
     simp
   | Color.upR =>
-    change Fermion.rightDualContraction (Fermion.rightBasis i ⊗ₜ Fermion.dualRightBasis j) = _
+    change Fermion.rightDualContraction
+      (Fermion.RightHandedWeyl.basis i ⊗ₜ Fermion.DualRightHandedWeyl.basis j) = _
     rw [Fermion.rightDualContraction_basis]
     simp
   | Color.downR =>
-    change Fermion.rightDualContraction (Fermion.rightBasis i ⊗ₜ Fermion.dualRightBasis j) = _
+    change Fermion.rightDualContraction
+      (Fermion.RightHandedWeyl.basis i ⊗ₜ Fermion.DualRightHandedWeyl.basis j) = _
     rw [Fermion.rightDualContraction_basis]
     simp
   | Color.up =>
diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Units/Basic.lean b/Physlib/Relativity/Tensors/ComplexTensor/Units/Basic.lean
index 947062b86..e24c59d2a 100644
--- a/Physlib/Relativity/Tensors/ComplexTensor/Units/Basic.lean
+++ b/Physlib/Relativity/Tensors/ComplexTensor/Units/Basic.lean
@@ -177,26 +177,26 @@ lemma contrCoUnit_eq_complexContrBasisFin4_complexCoBasisFin4 : δ =
   simp [complexContrBasisFin4, complexCoBasisFin4]
 
 open Fermion in
-lemma dualLeftLeftUnit_eq_dualLeftBasis_leftBasis : δL' =
-    ∑ i, fromPairT (dualLeftBasis i ⊗ₜ[ℂ] leftBasis i) := by
+lemma dualLeftLeftUnit_eq_basis : δL' =
+    ∑ i, fromPairT (DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] LeftHandedWeyl.basis i) := by
   rw [dualLeftLeftUnit_eq_fromPairT, dualLeftLeftUnitVal_expand_tmul]
   rfl
 
 open Fermion in
-lemma leftDualLeftUnit_eq_leftBasis_dualLeftBasis : δL =
-    ∑ i, fromPairT (leftBasis i ⊗ₜ[ℂ] dualLeftBasis i) := by
+lemma leftDualLeftUnit_eq_basis : δL =
+    ∑ i, fromPairT (LeftHandedWeyl.basis i ⊗ₜ[ℂ] DualLeftHandedWeyl.basis i) := by
   rw [leftDualLeftUnit_eq_fromPairT, leftDualLeftUnitVal_expand_tmul]
   rfl
 
 open Fermion in
-lemma dualRightRightUnit_eq_dualRightBasis_rightBasis : δR' =
-    ∑ i, fromPairT (dualRightBasis i ⊗ₜ[ℂ] rightBasis i) := by
+lemma dualRightRightUnit_eq_basis : δR' =
+    ∑ i, fromPairT (DualRightHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis i) := by
   rw [dualRightRightUnit_eq_fromPairT, dualRightRightUnitVal_expand_tmul]
   rfl
 
 open Fermion in
-lemma rightDualRightUnit_eq_rightBasis_dualRightBasis : δR =
-    ∑ i, fromPairT (rightBasis i ⊗ₜ[ℂ] dualRightBasis i) := by
+lemma rightDualRightUnit_eq_basis : δR =
+    ∑ i, fromPairT (RightHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis i) := by
   rw [rightDualRightUnit_eq_fromPairT, rightDualRightUnitVal_expand_tmul]
   rfl
 
@@ -228,10 +228,10 @@ lemma contrCoUnit_eq_basis : δ =
     rw [fromPairT_apply_basis_repr]
   rfl
 
-lemma dualLeftLeftUnit_eq_basis : δL' =
+lemma dualLeftLeftUnit_eq_tensor_basis : δL' =
     ∑ i, Tensor.basis (S := complexLorentzTensor)
       ![Color.downL, Color.upL] (fun | 0 => i | 1 => i) := by
-  rw [dualLeftLeftUnit_eq_dualLeftBasis_leftBasis]
+  rw [dualLeftLeftUnit_eq_basis]
   conv_lhs =>
     enter [2, x]
     change fromPairT ((complexLorentzTensor.basis .downL x) ⊗ₜ[ℂ]
@@ -239,10 +239,10 @@ lemma dualLeftLeftUnit_eq_basis : δL' =
     rw [fromPairT_apply_basis_repr]
   rfl
 
-lemma leftDualLeftUnit_eq_basis : δL =
+lemma leftDualLeftUnit_eq_tensor_basis : δL =
     ∑ i, Tensor.basis (S := complexLorentzTensor)
       ![Color.upL, Color.downL] (fun | 0 => i | 1 => i) := by
-  rw [leftDualLeftUnit_eq_leftBasis_dualLeftBasis]
+  rw [leftDualLeftUnit_eq_basis]
   conv_lhs =>
     enter [2, x]
     change fromPairT ((complexLorentzTensor.basis .upL x) ⊗ₜ[ℂ]
@@ -250,10 +250,10 @@ lemma leftDualLeftUnit_eq_basis : δL =
     rw [fromPairT_apply_basis_repr]
   rfl
 
-lemma dualRightRightUnit_eq_basis : δR' =
+lemma dualRightRightUnit_eq_tensor_basis : δR' =
     ∑ i, Tensor.basis (S := complexLorentzTensor)
       ![Color.downR, Color.upR] (fun | 0 => i | 1 => i) := by
-  rw [dualRightRightUnit_eq_dualRightBasis_rightBasis]
+  rw [dualRightRightUnit_eq_basis]
   conv_lhs =>
     enter [2, x]
     change fromPairT ((complexLorentzTensor.basis .downR x) ⊗ₜ[ℂ]
@@ -261,10 +261,10 @@ lemma dualRightRightUnit_eq_basis : δR' =
     rw [fromPairT_apply_basis_repr]
   rfl
 
-lemma rightDualRightUnit_eq_basis : δR =
+lemma rightDualRightUnit_eq_tensor_basis : δR =
     ∑ i, Tensor.basis (S := complexLorentzTensor)
       ![Color.upR, Color.downR] (fun | 0 => i | 1 => i) := by
-  rw [rightDualRightUnit_eq_rightBasis_dualRightBasis]
+  rw [rightDualRightUnit_eq_basis]
   conv_lhs =>
     enter [2, x]
     change fromPairT ((complexLorentzTensor.basis .upR x) ⊗ₜ[ℂ]
@@ -300,7 +300,7 @@ lemma contrCoUnit_eq_ofRat : δ = ofRat fun f =>
 
 lemma dualLeftLeftUnit_eq_ofRat : δL' = ofRat fun f =>
     if f 0 = f 1 then 1 else 0 := by
-  rw [dualLeftLeftUnit_eq_basis]
+  rw [dualLeftLeftUnit_eq_tensor_basis]
   conv_lhs =>
     enter [2, x]
     rw [basis_eq_ofRat]
@@ -310,7 +310,7 @@ lemma dualLeftLeftUnit_eq_ofRat : δL' = ofRat fun f =>
 
 lemma leftDualLeftUnit_eq_ofRat : δL = ofRat fun f =>
     if f 0 = f 1 then 1 else 0 := by
-  rw [leftDualLeftUnit_eq_basis]
+  rw [leftDualLeftUnit_eq_tensor_basis]
   conv_lhs =>
     enter [2, x]
     rw [basis_eq_ofRat]
@@ -320,7 +320,7 @@ lemma leftDualLeftUnit_eq_ofRat : δL = ofRat fun f =>
 
 lemma dualRightRightUnit_eq_ofRat : δR' = ofRat fun f =>
     if f 0 = f 1 then 1 else 0 := by
-  rw [dualRightRightUnit_eq_basis]
+  rw [dualRightRightUnit_eq_tensor_basis]
   conv_lhs =>
     enter [2, x]
     rw [basis_eq_ofRat]
@@ -330,7 +330,7 @@ lemma dualRightRightUnit_eq_ofRat : δR' = ofRat fun f =>
 
 lemma rightDualRightUnit_eq_ofRat : δR = ofRat fun f =>
     if f 0 = f 1 then 1 else 0 := by
-  rw [rightDualRightUnit_eq_basis]
+  rw [rightDualRightUnit_eq_tensor_basis]
   conv_lhs =>
     enter [2, x]
     rw [basis_eq_ofRat]
diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Basic.lean b/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Basic.lean
index 0a3c356a8..c8f4007b6 100644
--- a/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Basic.lean
+++ b/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Basic.lean
@@ -28,15 +28,37 @@ open MatrixGroups
 open Complex
 open TensorProduct
 
-TODO "Rename the Weyl fermion representations `leftHandedRep`, `dualLeftHandedRep`,
-  `rightHandedRep` and `dualRightHandedRep` to `LeftHandedWeyl.rep`,
-  `DualLeftHandedWeyl.rep`, `RightHandedWeyl.rep` and `DualRightHandedWeyl.rep`
-  respectively, so that each representation lives in the namespace of the module it
-  acts on, and update all references accordingly."
+/-!
+
+## Left-handed Weyl fermions
+
+-/
+
+namespace LeftHandedWeyl
+
+/-- The standard basis on left-handed Weyl fermions. -/
+def basis : Basis (Fin 2) ℂ LeftHandedWeyl := Basis.ofEquivFun
+  (Equiv.linearEquiv ℂ LeftHandedWeyl.toFin2ℂFun)
+
+lemma basis_apply (i j : Fin 2) : (basis i).1 j = if j = i then 1 else 0 := by
+  simp only [basis, Equiv.linearEquiv, AddEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe,
+    EquivLike.coe_coe, Equiv.invFun_as_coe, AddEquiv.coe_toEquiv_symm, Basis.coe_ofEquivFun,
+    LinearEquiv.symm_mk, LinearMap.coe_mk, AddHom.coe_mk, LinearEquiv.coe_mk,
+    Equiv.addEquiv_symm_apply]
+  change Pi.single i 1 j = _
+  simp [Pi.single_apply]
+
+lemma eq_sum_basis (ψ : LeftHandedWeyl) : ψ = ∑ i, ψ.1 i • basis i := by
+  conv_lhs => rw [← basis.sum_repr ψ]
+  rfl
+
+lemma basis_val (i : Fin 2) : (basis i).val = Pi.single i 1 := by
+  ext j
+  simp [basis_apply, Pi.single_apply]
 
 /-- The vector space ℂ^2 carrying the fundamental representation of SL(2,C).
   In index notation corresponds to a Weyl fermion with indices ψ^a. -/
-def leftHandedRep : Representation ℂ SL(2,ℂ) LeftHandedWeyl where
+def rep : Representation ℂ SL(2,ℂ) LeftHandedWeyl where
   toFun := fun M => {
     toFun := fun (ψ : LeftHandedWeyl) =>
       LeftHandedWeyl.toFin2ℂEquiv.symm (M.1 *ᵥ ψ.toFin2ℂ),
@@ -55,26 +77,65 @@ def leftHandedRep : Representation ℂ SL(2,ℂ) LeftHandedWeyl where
     simp only [LinearMap.coe_mk, AddHom.coe_mk, Module.End.mul_apply, LinearEquiv.apply_symm_apply,
       mulVec_mulVec]
 
-/-- The standard basis on left-handed Weyl fermions. -/
-def leftBasis : Basis (Fin 2) ℂ LeftHandedWeyl := Basis.ofEquivFun
-  (Equiv.linearEquiv ℂ LeftHandedWeyl.toFin2ℂFun)
+lemma rep_apply (M : SL(2,ℂ)) (ψ : LeftHandedWeyl) : rep M ψ = ⟨M.1 *ᵥ ψ.1⟩ := rfl
 
-@[simp]
-lemma leftBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
-    (LinearMap.toMatrix leftBasis leftBasis) (leftHandedRep M) i j = M.1 i j := by
+lemma rep_apply_eq_sum_basis (M : SL(2,ℂ)) (ψ : LeftHandedWeyl) :
+    rep M ψ = ∑ i, (∑ j, M.1 i j * ψ.1 j) • basis i := by
+  rw [eq_sum_basis (rep M ψ)]
+  rfl
+
+lemma rep_apply_basis (M : SL(2,ℂ)) (i : Fin 2) :
+    rep M (basis i) = ∑ j, M.1 j i • basis j := by
+  rw [rep_apply_eq_sum_basis]
+  congr
+  funext j
+  simp [basis_apply]
+
+lemma rep_toMatrix (M : SL(2,ℂ)) : (LinearMap.toMatrix basis basis) (rep M) = M.1 := by
+  ext i j
   rw [LinearMap.toMatrix_apply]
-  simp only [leftBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply]
+  simp only [basis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply]
   change (M.1 *ᵥ (Pi.single j 1)) i = _
   simp
 
-@[simp]
-lemma leftBasis_toFin2ℂ (i : Fin 2) : (leftBasis i).toFin2ℂ = Pi.single i 1 := by
-  simp only [leftBasis, Basis.coe_ofEquivFun]
+lemma rep_apply_basis_repr (M : SL(2,ℂ)) (i j : Fin 2) :
+    basis.repr (rep M (basis i)) j = M.1 j i := by
+  fin_cases j <;> simp [rep_apply_basis]
+
+end LeftHandedWeyl
+
+
+/-!
+
+## Dual Left-handed Weyl fermions
+
+-/
+
+namespace DualLeftHandedWeyl
+
+/-- The standard basis on dual-left-handed Weyl fermions. -/
+def basis : Basis (Fin 2) ℂ DualLeftHandedWeyl := Basis.ofEquivFun
+  (Equiv.linearEquiv ℂ DualLeftHandedWeyl.toFin2ℂFun)
+
+lemma basis_apply (i j : Fin 2) : (basis i).1 j = if j = i then 1 else 0 := by
+  simp only [basis, Equiv.linearEquiv, AddEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe,
+    EquivLike.coe_coe, Equiv.invFun_as_coe, AddEquiv.coe_toEquiv_symm, Basis.coe_ofEquivFun,
+    LinearEquiv.symm_mk, LinearMap.coe_mk, AddHom.coe_mk, LinearEquiv.coe_mk,
+    Equiv.addEquiv_symm_apply]
+  change Pi.single i 1 j = _
+  simp [Pi.single_apply]
+
+lemma eq_sum_basis (ψ : DualLeftHandedWeyl) : ψ = ∑ i, ψ.1 i • basis i := by
+  conv_lhs => rw [← basis.sum_repr ψ]
   rfl
 
+lemma basis_val (i : Fin 2) : (basis i).val = Pi.single i 1 := by
+  ext j
+  simp [basis_apply, Pi.single_apply]
+
 /-- The vector space ℂ^2 carrying the representation of SL(2,C) given by
-    M → (M⁻¹)ᵀ. In index notation corresponds to a Weyl fermion with indices ψ_a. -/
-def dualLeftHandedRep : Representation ℂ SL(2,ℂ) DualLeftHandedWeyl where
+    M → (M⁻¹)ᵀ. In index notation corresponds to a left-handed Weyl fermion with indices ψ_a. -/
+def rep : Representation ℂ SL(2,ℂ) DualLeftHandedWeyl where
   toFun := fun M => {
     toFun := fun (ψ : DualLeftHandedWeyl) =>
       DualLeftHandedWeyl.toFin2ℂEquiv.symm ((M.1⁻¹)ᵀ *ᵥ ψ.toFin2ℂ),
@@ -95,26 +156,62 @@ def dualLeftHandedRep : Representation ℂ SL(2,ℂ) DualLeftHandedWeyl where
     rw [Matrix.mul_inv_rev]
     exact transpose_mul _ _
 
-/-- The standard basis on dual-left-handed Weyl fermions. -/
-def dualLeftBasis : Basis (Fin 2) ℂ DualLeftHandedWeyl := Basis.ofEquivFun
-  (Equiv.linearEquiv ℂ DualLeftHandedWeyl.toFin2ℂFun)
-
-@[simp]
-lemma dualLeftBasis_toFin2ℂ (i : Fin 2) : (dualLeftBasis i).toFin2ℂ = Pi.single i 1 := by
-  simp only [dualLeftBasis, Basis.coe_ofEquivFun]
+lemma rep_apply_eq_sum_basis (M : SL(2,ℂ)) (ψ : DualLeftHandedWeyl) :
+    rep M ψ = ∑ i, (∑ j, M.1⁻¹ j i * ψ.1 j) • basis i := by
+  rw [eq_sum_basis (rep M ψ)]
   rfl
 
-@[simp]
-lemma dualLeftBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
-    (LinearMap.toMatrix dualLeftBasis dualLeftBasis) (dualLeftHandedRep M) i j = (M.1⁻¹)ᵀ i j := by
+lemma rep_apply_basis (M : SL(2,ℂ)) (i : Fin 2) :
+    rep M (basis i) = ∑ j, M.1⁻¹ i j • basis j := by
+  rw [rep_apply_eq_sum_basis]
+  congr
+  funext j
+  simp [basis_apply]
+
+lemma rep_toMatrix (M : SL(2,ℂ)) : (LinearMap.toMatrix basis basis) (rep M) = (M.1⁻¹)ᵀ := by
+  ext i j
   rw [LinearMap.toMatrix_apply]
-  simp only [dualLeftBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply, transpose_apply]
+  simp only [basis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply]
   change ((M.1⁻¹)ᵀ *ᵥ (Pi.single j 1)) i = _
   simp
 
+lemma rep_apply_basis_repr (M : SL(2,ℂ)) (i j : Fin 2) :
+    basis.repr (rep M (basis i)) j = M.1⁻¹ i j := by
+  fin_cases j <;> simp [rep_apply_basis]
+
+end DualLeftHandedWeyl
+
+/-!
+
+## Right-handed Weyl fermions
+
+-/
+
+namespace RightHandedWeyl
+
+/-- The standard basis on right-handed Weyl fermions. -/
+def basis : Basis (Fin 2) ℂ RightHandedWeyl := Basis.ofEquivFun
+  (Equiv.linearEquiv ℂ RightHandedWeyl.toFin2ℂFun)
+
+lemma basis_apply (i j : Fin 2) : (basis i).1 j = if j = i then 1 else 0 := by
+  simp only [basis, Equiv.linearEquiv, AddEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe,
+    EquivLike.coe_coe, Equiv.invFun_as_coe, AddEquiv.coe_toEquiv_symm, Basis.coe_ofEquivFun,
+    LinearEquiv.symm_mk, LinearMap.coe_mk, AddHom.coe_mk, LinearEquiv.coe_mk,
+    Equiv.addEquiv_symm_apply]
+  change Pi.single i 1 j = _
+  simp [Pi.single_apply]
+
+lemma eq_sum_basis (ψ : RightHandedWeyl) : ψ = ∑ i, ψ.1 i • basis i := by
+  conv_lhs => rw [← basis.sum_repr ψ]
+  rfl
+
+lemma basis_val (i : Fin 2) : (basis i).val = Pi.single i 1 := by
+  ext j
+  simp [basis_apply, Pi.single_apply]
+
 /-- The vector space ℂ^2 carrying the conjugate representation of SL(2,C).
   In index notation corresponds to a Weyl fermion with indices ψ^{dot a}. -/
-def rightHandedRep : Representation ℂ SL(2,ℂ) RightHandedWeyl where
+def rep : Representation ℂ SL(2,ℂ) RightHandedWeyl where
   toFun := fun M => {
     toFun := fun (ψ : RightHandedWeyl) =>
       RightHandedWeyl.toFin2ℂEquiv.symm (M.1.map star *ᵥ ψ.toFin2ℂ),
@@ -132,27 +229,65 @@ def rightHandedRep : Representation ℂ SL(2,ℂ) RightHandedWeyl where
     simp only [SpecialLinearGroup.coe_mul, RCLike.star_def, Matrix.map_mul, LinearMap.coe_mk,
       AddHom.coe_mk, Module.End.mul_apply, LinearEquiv.apply_symm_apply, mulVec_mulVec]
 
-/-- The standard basis on right-handed Weyl fermions. -/
-def rightBasis : Basis (Fin 2) ℂ RightHandedWeyl := Basis.ofEquivFun
-  (Equiv.linearEquiv ℂ RightHandedWeyl.toFin2ℂFun)
+lemma rep_apply (M : SL(2,ℂ)) (ψ : RightHandedWeyl) : rep M ψ = ⟨M.1.map star *ᵥ ψ.1⟩ := rfl
 
-@[simp]
-lemma rightBasis_toFin2ℂ (i : Fin 2) : (rightBasis i).toFin2ℂ = Pi.single i 1 := by
-  simp only [rightBasis, Basis.coe_ofEquivFun]
+lemma rep_apply_eq_sum_basis (M : SL(2,ℂ)) (ψ : RightHandedWeyl) :
+    rep M ψ = ∑ i, (∑ j, M.1.map star i j * ψ.1 j) • basis i := by
+  rw [eq_sum_basis (rep M ψ)]
   rfl
 
-@[simp]
-lemma rightBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
-    (LinearMap.toMatrix rightBasis rightBasis) (rightHandedRep M) i j = (M.1.map star) i j := by
+lemma rep_apply_basis (M : SL(2,ℂ)) (i : Fin 2) :
+    rep M (basis i) = ∑ j, M.1.map star j i • basis j := by
+  rw [rep_apply_eq_sum_basis]
+  congr
+  funext j
+  simp [basis_apply]
+
+lemma rep_toMatrix (M : SL(2,ℂ)) : (LinearMap.toMatrix basis basis) (rep M) = M.1.map star := by
+  ext i j
   rw [LinearMap.toMatrix_apply]
-  simp only [rightBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply]
+  simp only [basis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply]
   change (M.1.map star *ᵥ (Pi.single j 1)) i = _
-  simp [mulVec_single]
+  simp
+
+lemma rep_apply_basis_repr (M : SL(2,ℂ)) (i j : Fin 2) :
+    basis.repr (rep M (basis i)) j = star (M.1 j i) := by
+  fin_cases j <;> simp [rep_apply_basis]
+
+end RightHandedWeyl
+
+/-!
+
+## Dual Right-handed Weyl fermions
+
+-/
+
+namespace DualRightHandedWeyl
+
+/-- The standard basis on dual-right-handed Weyl fermions. -/
+def basis : Basis (Fin 2) ℂ DualRightHandedWeyl := Basis.ofEquivFun
+  (Equiv.linearEquiv ℂ DualRightHandedWeyl.toFin2ℂFun)
+
+
+lemma basis_apply (i j : Fin 2) : (basis i).1 j = if j = i then 1 else 0 := by
+  simp only [basis, Equiv.linearEquiv, AddEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe,
+    EquivLike.coe_coe, Equiv.invFun_as_coe, AddEquiv.coe_toEquiv_symm, Basis.coe_ofEquivFun,
+    LinearEquiv.symm_mk, LinearMap.coe_mk, AddHom.coe_mk, LinearEquiv.coe_mk,
+    Equiv.addEquiv_symm_apply]
+  change Pi.single i 1 j = _
+  simp [Pi.single_apply]
 
+lemma eq_sum_basis (ψ : DualRightHandedWeyl) : ψ = ∑ i, ψ.1 i • basis i := by
+  conv_lhs => rw [← basis.sum_repr ψ]
+  rfl
+
+lemma basis_val (i : Fin 2) : (basis i).val = Pi.single i 1 := by
+  ext j
+  simp [basis_apply, Pi.single_apply]
 /-- The vector space ℂ^2 carrying the representation of SL(2,C) given by
     M → (M⁻¹)^†.
     In index notation this corresponds to a Weyl fermion with index `ψ_{dot a}`. -/
-def dualRightHandedRep : Representation ℂ SL(2,ℂ) DualRightHandedWeyl where
+def rep : Representation ℂ SL(2,ℂ) DualRightHandedWeyl where
   toFun := fun M => {
     toFun := fun (ψ : DualRightHandedWeyl) =>
       DualRightHandedWeyl.toFin2ℂEquiv.symm ((M.1⁻¹).conjTranspose *ᵥ ψ.toFin2ℂ),
@@ -173,34 +308,48 @@ def dualRightHandedRep : Representation ℂ SL(2,ℂ) DualRightHandedWeyl where
     rw [Matrix.mul_inv_rev]
     exact conjTranspose_mul _ _
 
-/-- The standard basis on dual-right-handed Weyl fermions. -/
-def dualRightBasis : Basis (Fin 2) ℂ DualRightHandedWeyl := Basis.ofEquivFun
-  (Equiv.linearEquiv ℂ DualRightHandedWeyl.toFin2ℂFun)
+lemma rep_apply (M : SL(2,ℂ)) (ψ : DualRightHandedWeyl) :
+    rep M ψ = ⟨(M.1⁻¹).conjTranspose *ᵥ ψ.1⟩ := rfl
 
-@[simp]
-lemma dualRightBasis_toFin2ℂ (i : Fin 2) : (dualRightBasis i).toFin2ℂ = Pi.single i 1 := by
-  simp only [dualRightBasis, Basis.coe_ofEquivFun]
+lemma rep_apply_eq_sum_basis (M : SL(2,ℂ)) (ψ : DualRightHandedWeyl) :
+    rep M ψ = ∑ i, (∑ j, (M.1⁻¹).conjTranspose i j * ψ.1 j) • basis i := by
+  rw [eq_sum_basis (rep M ψ)]
   rfl
 
-@[simp]
-lemma dualRightBasis_ρ_apply (M : SL(2,ℂ)) (i j : Fin 2) :
-    (LinearMap.toMatrix dualRightBasis dualRightBasis) (dualRightHandedRep M) i j =
-    ((M.1⁻¹).conjTranspose) i j := by
+lemma rep_apply_basis (M : SL(2,ℂ)) (i : Fin 2) :
+    rep M (basis i) = ∑ j, (M.1⁻¹).conjTranspose j i • basis j := by
+  rw [rep_apply_eq_sum_basis]
+  congr
+  funext j
+  simp [basis_apply]
+
+lemma rep_toMatrix (M : SL(2,ℂ)) :
+    (LinearMap.toMatrix basis basis) (rep M) = (M.1⁻¹).conjTranspose := by
+  ext i j
   rw [LinearMap.toMatrix_apply]
-  simp only [dualRightBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply]
+  simp only [basis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply]
   change ((M.1⁻¹).conjTranspose *ᵥ (Pi.single j 1)) i = _
-  simp [mulVec_single]
+  simp
+
+lemma rep_apply_basis_repr (M : SL(2,ℂ)) (i j : Fin 2) :
+    basis.repr (rep M (basis i)) j = star (M.1⁻¹ i j) := by
+  fin_cases j <;> simp [rep_apply_basis]
+
+end DualRightHandedWeyl
 
 /-!
 
-## Equivalences between Weyl fermion vector spaces.
+## Duals of Weyl fermions
+
+The dual of `LeftHandedWeyl` is `DualLeftHandedWeyl`, and the dual of `RightHandedWeyl` is
+`DualRightHandedWeyl`.
 
 -/
 
 /-- The morphism between the representation `leftHanded` and the representation
   `dualLeftHanded` defined by multiplying an element of
   `leftHanded` by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`. -/
-def leftHandedToDual : leftHandedRep.IntertwiningMap dualLeftHandedRep where
+def LeftHandedWeyl.dual : LeftHandedWeyl.rep.IntertwiningMap DualLeftHandedWeyl.rep where
   toFun := fun ψ => DualLeftHandedWeyl.toFin2ℂEquiv.symm (!![0, 1; -1, 0] *ᵥ ψ.toFin2ℂ)
   map_add' := by
     intro ψ ψ'
@@ -221,14 +370,14 @@ def leftHandedToDual : leftHandedRep.IntertwiningMap dualLeftHandedRep where
       Matrix.mul_fin_two, eta_fin_two !![M.1 1 1, -M.1 0 1; -M.1 1 0, M.1 0 0]ᵀ]
     simp
 
-lemma leftHandedToDual_hom_apply (ψ : LeftHandedWeyl) :
-    leftHandedToDual ψ =
+lemma LeftHandedWeyl.dual_hom_apply (ψ : LeftHandedWeyl) :
+    LeftHandedWeyl.dual ψ =
     DualLeftHandedWeyl.toFin2ℂEquiv.symm (!![0, 1; -1, 0] *ᵥ ψ.toFin2ℂ) := rfl
 
 /-- The morphism from `dualLeftHanded` to
   `leftHanded` defined by multiplying an element of
   DualLeftHandedWeyl by the matrix `εₐ₁ₐ₂ = !![0, -1; 1, 0]`. -/
-def leftHandedDualTo : dualLeftHandedRep.IntertwiningMap leftHandedRep where
+def DualLeftHandedWeyl.dual : DualLeftHandedWeyl.rep.IntertwiningMap LeftHandedWeyl.rep where
   toFun := fun ψ =>
       LeftHandedWeyl.toFin2ℂEquiv.symm (!![0, -1; 1, 0] *ᵥ ψ.toFin2ℂ)
   map_add' := by
@@ -252,19 +401,19 @@ def leftHandedDualTo : dualLeftHandedRep.IntertwiningMap leftHandedRep where
       Matrix.mul_fin_two, eta_fin_two !![M.1 1 1, -M.1 0 1; -M.1 1 0, M.1 0 0]ᵀ]
     simp
 
-lemma leftHandedDualTo_hom_apply (ψ : DualLeftHandedWeyl) :
-    leftHandedDualTo ψ =
+lemma DualLeftHandedWeyl.dual_hom_apply (ψ : DualLeftHandedWeyl) :
+    DualLeftHandedWeyl.dual ψ =
     LeftHandedWeyl.toFin2ℂEquiv.symm (!![0, -1; 1, 0] *ᵥ ψ.toFin2ℂ) := rfl
 
 /-- The equivalence between the representation `leftHanded` and the representation
   `dualLeftHanded` defined by multiplying an element of
   `leftHanded` by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`. -/
-def leftHandedDualEquiv : leftHandedRep.Equiv dualLeftHandedRep := by
-  refine Representation.Equiv.mk' leftHandedToDual leftHandedDualTo ?_ ?_
+def LeftHandedWeyl.dualEquiv : LeftHandedWeyl.rep.Equiv DualLeftHandedWeyl.rep := by
+  refine Representation.Equiv.mk'  LeftHandedWeyl.dual DualLeftHandedWeyl.dual ?_ ?_
   · intro x
     simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
       Representation.IntertwiningMap.coe_toLinearMap]
-    rw [leftHandedDualTo_hom_apply, leftHandedToDual_hom_apply]
+    rw [DualLeftHandedWeyl.dual_hom_apply, LeftHandedWeyl.dual_hom_apply]
     rw [DualLeftHandedWeyl.toFin2ℂ, LinearEquiv.apply_symm_apply, mulVec_mulVec]
     rw [show (!![0, -1; (1 : ℂ), 0] * !![0, 1; -1, 0]) = 1 by simpa using Eq.symm one_fin_two]
     rw [one_mulVec]
@@ -272,7 +421,7 @@ def leftHandedDualEquiv : leftHandedRep.Equiv dualLeftHandedRep := by
   · intro ψ
     simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
       Representation.IntertwiningMap.coe_toLinearMap]
-    rw [leftHandedDualTo_hom_apply, leftHandedToDual_hom_apply, LeftHandedWeyl.toFin2ℂ,
+    rw [DualLeftHandedWeyl.dual_hom_apply, LeftHandedWeyl.dual_hom_apply, LeftHandedWeyl.toFin2ℂ,
       LinearEquiv.apply_symm_apply, mulVec_mulVec]
     rw [show (!![0, (1 : ℂ); -1, 0] * !![0, -1; 1, 0]) = 1 by simpa using Eq.symm one_fin_two]
     rw [one_mulVec]
@@ -280,28 +429,28 @@ def leftHandedDualEquiv : leftHandedRep.Equiv dualLeftHandedRep := by
 
 /-- `leftHandedDualEquiv` acting on an element `ψ : leftHanded` corresponds
   to multiplying `ψ` by the matrix `!![0, 1; -1, 0]`. -/
-lemma leftHandedDualEquiv_hom_hom_apply (ψ : LeftHandedWeyl) :
-    leftHandedDualEquiv ψ =
+lemma LeftHandedWeyl.dualEquiv_hom_hom_apply (ψ : LeftHandedWeyl) :
+    LeftHandedWeyl.dualEquiv ψ =
     DualLeftHandedWeyl.toFin2ℂEquiv.symm (!![0, 1; -1, 0] *ᵥ ψ.toFin2ℂ) := rfl
 
 /-- The inverse of `leftHandedDualEquiv` acting on an element`ψ : dualLeftHanded` corresponds
   to multiplying `ψ` by the matrix `!![0, -1; 1, 0]`. -/
-lemma leftHandedDualEquiv_inv_hom_apply (ψ : DualLeftHandedWeyl) :
-    leftHandedDualEquiv.symm ψ =
+lemma LeftHandedWeyl.dualEquiv_inv_hom_apply (ψ : DualLeftHandedWeyl) :
+    LeftHandedWeyl.dualEquiv.symm ψ =
     LeftHandedWeyl.toFin2ℂEquiv.symm (!![0, -1; 1, 0] *ᵥ ψ.toFin2ℂ) := rfl
 
 /-- The linear equivalence between `rightHandedWeyl` and `DualRightHandedWeyl` given by multiplying
 an element of `rightHandedWeyl` by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`.
 -/
-informal_definition rightHandedWeylDualEquiv where
-  deps := [``rightHandedRep, ``dualRightHandedRep]
+informal_definition RightHandedWeyl.dualEquiv where
+  deps := [``RightHandedWeyl, ``DualRightHandedWeyl]
   tag := "6VZR4"
 
 /-- The linear equivalence `rightHandedWeylDualEquiv` is equivariant with respect to the action of
 `SL(2,C)` on `rightHandedWeyl` and `DualRightHandedWeyl`.
 -/
-informal_lemma rightHandedWeylDualEquiv_equivariant where
-  deps := [``rightHandedWeylDualEquiv]
+informal_lemma RightHandedWeyl.dualEquiv_equivariant where
+  deps := [``RightHandedWeyl.dualEquiv]
   tag := "6VZSG"
 
 end
diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Contraction.lean b/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Contraction.lean
index 4748e2992..e1b9cc659 100644
--- a/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Contraction.lean
+++ b/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Contraction.lean
@@ -130,7 +130,7 @@ def dualRightBi : DualRightHandedWeyl →ₗ[ℂ] RightHandedWeyl →ₗ[ℂ] 
     standard basis (i.e. the dot product).
     Physically, the contraction of a left-handed Weyl fermion with a dual-left-handed Weyl fermion.
     In index notation this is ψ^a φ_a. -/
-def leftDualContraction : (leftHandedRep.tprod dualLeftHandedRep).IntertwiningMap
+def leftDualContraction : (LeftHandedWeyl.rep.tprod DualLeftHandedWeyl.rep).IntertwiningMap
     (Representation.trivial ℂ SL(2,ℂ) ℂ) where
   toLinearMap := TensorProduct.lift leftDualBi
   isIntertwining' M := TensorProduct.ext' fun ψ φ => by
@@ -144,9 +144,11 @@ lemma leftDualContraction_hom_tmul (ψ : LeftHandedWeyl)
   rfl
 
 lemma leftDualContraction_basis (i j : Fin 2) :
-    leftDualContraction (leftBasis i ⊗ₜ dualLeftBasis j) = if i.1 = j.1 then (1 : ℂ) else 0 := by
+    leftDualContraction (LeftHandedWeyl.basis i ⊗ₜ DualLeftHandedWeyl.basis j) =
+      if i.1 = j.1 then (1 : ℂ) else 0 := by
   rw [leftDualContraction_hom_tmul]
-  simp only [leftBasis_toFin2ℂ, dualLeftBasis_toFin2ℂ, dotProduct_single, mul_one]
+  simp only [LeftHandedWeyl.toFin2ℂ_eq_val, LeftHandedWeyl.basis_val,
+    DualLeftHandedWeyl.toFin2ℂ_eq_val, DualLeftHandedWeyl.basis_val, dotProduct_single, mul_one]
   rw [Pi.single_apply]
   simp only [Fin.ext_iff]
   refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
@@ -157,7 +159,7 @@ lemma leftDualContraction_basis (i j : Fin 2) :
     standard basis (i.e. the dot product).
     Physically, the contraction of a dual-left-handed Weyl fermion with a left-handed Weyl fermion.
     In index notation this is φ_a ψ^a. -/
-def dualLeftContraction : (dualLeftHandedRep.tprod leftHandedRep).IntertwiningMap
+def dualLeftContraction : (DualLeftHandedWeyl.rep.tprod LeftHandedWeyl.rep).IntertwiningMap
     (Representation.trivial ℂ SL(2,ℂ) ℂ) where
   toLinearMap := TensorProduct.lift dualLeftBi
   isIntertwining' M := TensorProduct.ext' fun φ ψ => by
@@ -170,9 +172,11 @@ lemma dualLeftContraction_hom_tmul (φ : DualLeftHandedWeyl) (ψ : LeftHandedWey
   rfl
 
 lemma dualLeftContraction_basis (i j : Fin 2) :
-    dualLeftContraction (dualLeftBasis i ⊗ₜ leftBasis j) = if i.1 = j.1 then (1 : ℂ) else 0 := by
+    dualLeftContraction (DualLeftHandedWeyl.basis i ⊗ₜ LeftHandedWeyl.basis j) =
+      if i.1 = j.1 then (1 : ℂ) else 0 := by
   rw [dualLeftContraction_hom_tmul]
-  simp only [dualLeftBasis_toFin2ℂ, leftBasis_toFin2ℂ, dotProduct_single, mul_one]
+  simp only [DualLeftHandedWeyl.toFin2ℂ_eq_val, DualLeftHandedWeyl.basis_val,
+    LeftHandedWeyl.toFin2ℂ_eq_val, LeftHandedWeyl.basis_val, dotProduct_single, mul_one]
   rw [Pi.single_apply]
   simp only [Fin.ext_iff]
   refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
@@ -185,7 +189,7 @@ The linear map from `rightHandedWeyl ⊗ DualRightHandedWeyl` to `ℂ` given by
   The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
   In index notation this is `ψ^{dot a} φ_{dot a}`.
 -/
-def rightDualContraction : (rightHandedRep.tprod dualRightHandedRep).IntertwiningMap
+def rightDualContraction : (RightHandedWeyl.rep.tprod DualRightHandedWeyl.rep).IntertwiningMap
     (Representation.trivial ℂ SL(2,ℂ) ℂ) where
   toLinearMap := TensorProduct.lift rightDualBi
   isIntertwining' M := TensorProduct.ext' fun ψ φ => by
@@ -210,10 +214,11 @@ lemma rightDualContraction_hom_tmul (ψ : RightHandedWeyl)
   rfl
 
 lemma rightDualContraction_basis (i j : Fin 2) :
-    rightDualContraction (rightBasis i ⊗ₜ dualRightBasis j) =
+    rightDualContraction (RightHandedWeyl.basis i ⊗ₜ DualRightHandedWeyl.basis j) =
     if i.1 = j.1 then (1 : ℂ) else 0 := by
   rw [rightDualContraction_hom_tmul]
-  simp only [rightBasis_toFin2ℂ, dualRightBasis_toFin2ℂ, dotProduct_single, mul_one]
+  simp only [RightHandedWeyl.toFin2ℂ_eq_val, RightHandedWeyl.basis_val,
+    DualRightHandedWeyl.toFin2ℂ_eq_val, DualRightHandedWeyl.basis_val, dotProduct_single, mul_one]
   rw [Pi.single_apply]
   simp only [Fin.ext_iff]
   refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
@@ -226,7 +231,7 @@ lemma rightDualContraction_basis (i j : Fin 2) :
   The contraction of a right-handed Weyl fermion with a left-handed Weyl fermion.
     In index notation this is φ_{dot a} ψ^{dot a}.
 -/
-def dualRightContraction : (dualRightHandedRep.tprod rightHandedRep).IntertwiningMap
+def dualRightContraction : (DualRightHandedWeyl.rep.tprod RightHandedWeyl.rep).IntertwiningMap
     (Representation.trivial ℂ SL(2,ℂ) ℂ) where
   toLinearMap := TensorProduct.lift dualRightBi
   isIntertwining' M := TensorProduct.ext' fun φ ψ => by
@@ -251,10 +256,11 @@ lemma dualRightContraction_hom_tmul (φ : DualRightHandedWeyl)
   rfl
 
 lemma dualRightContraction_basis (i j : Fin 2) :
-    dualRightContraction (dualRightBasis i ⊗ₜ rightBasis j) =
+    dualRightContraction (DualRightHandedWeyl.basis i ⊗ₜ RightHandedWeyl.basis j) =
     if i.1 = j.1 then (1 : ℂ) else 0 := by
   rw [dualRightContraction_hom_tmul]
-  simp only [dualRightBasis_toFin2ℂ, rightBasis_toFin2ℂ, dotProduct_single, mul_one]
+  simp only [DualRightHandedWeyl.toFin2ℂ_eq_val, DualRightHandedWeyl.basis_val,
+    RightHandedWeyl.toFin2ℂ_eq_val, RightHandedWeyl.basis_val, dotProduct_single, mul_one]
   rw [Pi.single_apply]
   simp only [Fin.ext_iff]
   refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Metric.lean b/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Metric.lean
index 60f8174b6..ea042b91e 100644
--- a/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Metric.lean
+++ b/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Metric.lean
@@ -76,7 +76,8 @@ def leftMetricVal : LeftHandedWeyl ⊗[ℂ] LeftHandedWeyl :=
 set_option backward.isDefEq.respectTransparency false in
 /-- Expansion of `leftMetricVal` into the left basis. -/
 lemma leftMetricVal_expand_tmul : leftMetricVal =
-    - leftBasis 0 ⊗ₜ[ℂ] leftBasis 1 + leftBasis 1 ⊗ₜ[ℂ] leftBasis 0 := by
+    - LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1 +
+      LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] LeftHandedWeyl.basis 0 := by
   simp only [leftMetricVal, Fin.isValue]
   rw [leftLeftToMatrix_symm_expand_tmul]
   simp only [metricRaw, Matrix.neg_apply, of_apply, cons_val', empty_val', cons_val_fin_one,
@@ -84,13 +85,14 @@ lemma leftMetricVal_expand_tmul : leftMetricVal =
     neg_neg, one_smul, add_zero, add_left_inj]
   module
 
-lemma leftMetricVal_expand_tmul' : leftMetricVal = leftBasis 1 ⊗ₜ[ℂ] leftBasis 0
-    - leftBasis 0 ⊗ₜ[ℂ] leftBasis 1 := by rw [leftMetricVal_expand_tmul]; abel
+lemma leftMetricVal_expand_tmul' : leftMetricVal =
+    LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] LeftHandedWeyl.basis 0
+    - LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1 := by rw [leftMetricVal_expand_tmul]; abel
 
 /-- The metric `εᵃᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ leftHanded`,
   making manifest its invariance under the action of `SL(2,ℂ)`. -/
 def leftMetric : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
-    (leftHandedRep.tprod leftHandedRep) where
+    (LeftHandedWeyl.rep.tprod LeftHandedWeyl.rep) where
   toFun := fun a =>
     let a' : ℂ := a
     a' • leftMetricVal
@@ -102,7 +104,7 @@ def leftMetric : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
   isIntertwining' M := by
     refine LinearMap.ext fun x : ℂ => ?_
     change x • leftMetricVal =
-      (TensorProduct.map (leftHandedRep M) (leftHandedRep M)) (x • leftMetricVal)
+      (TensorProduct.map (LeftHandedWeyl.rep M) (LeftHandedWeyl.rep M)) (x • leftMetricVal)
     simp only [map_smul]
     apply congrArg
     simp only [leftMetricVal, map_neg, neg_inj]
@@ -123,7 +125,8 @@ def dualLeftMetricVal : (DualLeftHandedWeyl ⊗[ℂ] DualLeftHandedWeyl) :=
 set_option backward.isDefEq.respectTransparency false in
 /-- Expansion of `dualLeftMetricVal` into the left basis. -/
 lemma dualLeftMetricVal_expand_tmul : dualLeftMetricVal =
-    dualLeftBasis 0 ⊗ₜ[ℂ] dualLeftBasis 1 - dualLeftBasis 1 ⊗ₜ[ℂ] dualLeftBasis 0 := by
+    DualLeftHandedWeyl.basis 0 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 1 -
+      DualLeftHandedWeyl.basis 1 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 0 := by
   simp only [dualLeftMetricVal, Fin.isValue]
   rw [dualLeftdualLeftToMatrix_symm_expand_tmul]
   simp only [metricRaw, of_apply, cons_val', empty_val', cons_val_fin_one, Fin.sum_univ_two,
@@ -133,7 +136,7 @@ lemma dualLeftMetricVal_expand_tmul : dualLeftMetricVal =
 /-- The metric `εₐₐ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ dualLeftHanded ⊗ dualLeftHanded`,
   making manifest its invariance under the action of `SL(2,ℂ)`. -/
 def dualLeftMetric : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
-    (dualLeftHandedRep.tprod dualLeftHandedRep) where
+    (DualLeftHandedWeyl.rep.tprod DualLeftHandedWeyl.rep) where
     toFun := fun a =>
       let a' : ℂ := a
       a' • dualLeftMetricVal
@@ -145,7 +148,8 @@ def dualLeftMetric : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
     isIntertwining' M := by
       refine LinearMap.ext fun x : ℂ => ?_
       change x • dualLeftMetricVal =
-        (TensorProduct.map (dualLeftHandedRep M) (dualLeftHandedRep M)) (x • dualLeftMetricVal)
+        (TensorProduct.map (DualLeftHandedWeyl.rep M) (DualLeftHandedWeyl.rep M))
+          (x • dualLeftMetricVal)
       simp only [map_smul]
       apply congrArg
       simp only [dualLeftMetricVal]
@@ -166,7 +170,8 @@ def rightMetricVal : (RightHandedWeyl ⊗[ℂ] RightHandedWeyl) :=
 set_option backward.isDefEq.respectTransparency false in
 /-- Expansion of `rightMetricVal` into the left basis. -/
 lemma rightMetricVal_expand_tmul : rightMetricVal =
-    - rightBasis 0 ⊗ₜ[ℂ] rightBasis 1 + rightBasis 1 ⊗ₜ[ℂ] rightBasis 0 := by
+    - RightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 +
+      RightHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 := by
   simp only [rightMetricVal, Fin.isValue]
   rw [rightRightToMatrix_symm_expand_tmul]
   simp only [metricRaw, Matrix.neg_apply, of_apply, cons_val', empty_val', cons_val_fin_one,
@@ -174,13 +179,16 @@ lemma rightMetricVal_expand_tmul : rightMetricVal =
     neg_neg, one_smul, add_zero, add_left_inj]
   module
 
-lemma rightMetricVal_expand_tmul' : rightMetricVal = rightBasis 1 ⊗ₜ[ℂ] rightBasis 0
-    - rightBasis 0 ⊗ₜ[ℂ] rightBasis 1 := by rw [rightMetricVal_expand_tmul]; abel
+lemma rightMetricVal_expand_tmul' : rightMetricVal =
+    RightHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 0
+    - RightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 := by
+  rw [rightMetricVal_expand_tmul]
+  abel
 
 /-- The metric `ε^{dot a}^{dot a}` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ rightHanded`,
   making manifest its invariance under the action of `SL(2,ℂ)`. -/
 def rightMetric : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
-    (rightHandedRep.tprod rightHandedRep) where
+    (RightHandedWeyl.rep.tprod RightHandedWeyl.rep) where
   toFun := fun a =>
     let a' : ℂ := a
     a' • rightMetricVal
@@ -192,7 +200,7 @@ def rightMetric : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
   isIntertwining' M := by
     refine LinearMap.ext fun x : ℂ => ?_
     change x • rightMetricVal =
-      (TensorProduct.map (rightHandedRep M) (rightHandedRep M)) (x • rightMetricVal)
+      (TensorProduct.map (RightHandedWeyl.rep M) (RightHandedWeyl.rep M)) (x • rightMetricVal)
     simp only [map_smul]
     apply congrArg
     simp only [rightMetricVal, map_neg, neg_inj]
@@ -220,7 +228,8 @@ def dualRightMetricVal : DualRightHandedWeyl ⊗[ℂ] DualRightHandedWeyl :=
 set_option backward.isDefEq.respectTransparency false in
 /-- Expansion of `rightMetricVal` into the left basis. -/
 lemma dualRightMetricVal_expand_tmul : dualRightMetricVal =
-    dualRightBasis 0 ⊗ₜ[ℂ] dualRightBasis 1 - dualRightBasis 1 ⊗ₜ[ℂ] dualRightBasis 0 := by
+    DualRightHandedWeyl.basis 0 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 1 -
+      DualRightHandedWeyl.basis 1 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 0 := by
   simp only [dualRightMetricVal, Fin.isValue]
   rw [dualRightDualRightToMatrix_symm_expand_tmul]
   simp only [metricRaw, of_apply, cons_val', empty_val', cons_val_fin_one, Fin.sum_univ_two,
@@ -231,7 +240,7 @@ lemma dualRightMetricVal_expand_tmul : dualRightMetricVal =
   `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ dualRightHanded ⊗ dualRightHanded`,
   making manifest its invariance under the action of `SL(2,ℂ)`. -/
 def dualRightMetric : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
-    (dualRightHandedRep.tprod dualRightHandedRep) where
+    (DualRightHandedWeyl.rep.tprod DualRightHandedWeyl.rep) where
   toFun := fun a =>
       let a' : ℂ := a
       a' • dualRightMetricVal
@@ -243,7 +252,8 @@ def dualRightMetric : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
   isIntertwining' M := by
     refine LinearMap.ext fun x : ℂ => ?_
     change x • dualRightMetricVal =
-      (TensorProduct.map (dualRightHandedRep M) (dualRightHandedRep M)) (x • dualRightMetricVal)
+      (TensorProduct.map (DualRightHandedWeyl.rep M) (DualRightHandedWeyl.rep M))
+        (x • dualRightMetricVal)
     simp only [map_smul]
     apply congrArg
     trans dualRightDualRightToMatrix.symm
diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Modules.lean b/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Modules.lean
index ff5e6506c..3ff1a9408 100644
--- a/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Modules.lean
+++ b/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Modules.lean
@@ -72,6 +72,8 @@ def toFin2ℂEquiv : LeftHandedWeyl ≃ₗ[ℂ] (Fin 2 → ℂ) where
   through the linear equivalence `toFin2ℂEquiv`. -/
 abbrev toFin2ℂ (ψ : LeftHandedWeyl) := toFin2ℂEquiv ψ
 
+lemma toFin2ℂ_eq_val (ψ : LeftHandedWeyl) : ψ.toFin2ℂ = ψ.val := rfl
+
 end LeftHandedWeyl
 
 end LeftHanded
@@ -116,6 +118,8 @@ def toFin2ℂEquiv : DualLeftHandedWeyl ≃ₗ[ℂ] (Fin 2 → ℂ) where
   through the linear equivalence `toFin2ℂEquiv`. -/
 abbrev toFin2ℂ (ψ : DualLeftHandedWeyl) := toFin2ℂEquiv ψ
 
+lemma toFin2ℂ_eq_val (ψ : DualLeftHandedWeyl) : ψ.toFin2ℂ = ψ.val := rfl
+
 end DualLeftHandedWeyl
 
 
@@ -161,6 +165,8 @@ def toFin2ℂEquiv : RightHandedWeyl ≃ₗ[ℂ] (Fin 2 → ℂ) where
   through the linear equivalence `toFin2ℂEquiv`. -/
 abbrev toFin2ℂ (ψ : RightHandedWeyl) := toFin2ℂEquiv ψ
 
+lemma toFin2ℂ_eq_val (ψ : RightHandedWeyl) : ψ.toFin2ℂ = ψ.val := rfl
+
 end RightHandedWeyl
 
 end RightHanded
@@ -207,6 +213,8 @@ def toFin2ℂEquiv : DualRightHandedWeyl ≃ₗ[ℂ] (Fin 2 → ℂ) where
   through the linear equivalence `toFin2ℂEquiv`. -/
 abbrev toFin2ℂ (ψ : DualRightHandedWeyl) := toFin2ℂEquiv ψ
 
+lemma toFin2ℂ_eq_val (ψ : DualRightHandedWeyl) : ψ.toFin2ℂ = ψ.val := rfl
+
 end DualRightHandedWeyl
 
 end DualRightHanded
diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Two.lean b/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Two.lean
index 3f638348d..1d0d5a982 100644
--- a/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Two.lean
+++ b/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Two.lean
@@ -31,183 +31,193 @@ open CategoryTheory.MonoidalCategory
 
 /-- Equivalence of `leftHanded ⊗ leftHanded` to `2 x 2` complex matrices. -/
 def leftLeftToMatrix : (LeftHandedWeyl ⊗[ℂ] LeftHandedWeyl) ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
-  (Basis.tensorProduct leftBasis leftBasis).repr ≪≫ₗ
+  (Basis.tensorProduct LeftHandedWeyl.basis LeftHandedWeyl.basis).repr ≪≫ₗ
   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
+    leftLeftToMatrix.symm M = ∑ i, ∑ j, M i j •
+      (LeftHandedWeyl.basis i ⊗ₜ[ℂ] LeftHandedWeyl.basis j) := by
   simp only [leftLeftToMatrix, LinearEquiv.trans_symm, LinearEquiv.trans_apply,
     Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
   · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
-    exact congrArg _ (Basis.tensorProduct_apply leftBasis leftBasis i j)
+    exact congrArg _ (Basis.tensorProduct_apply LeftHandedWeyl.basis LeftHandedWeyl.basis i j)
   · simp
 
 /-- Equivalence of `dualLeftHanded ⊗ dualLeftHanded` to `2 x 2` complex matrices. -/
 def dualLeftdualLeftToMatrix : (DualLeftHandedWeyl ⊗[ℂ] DualLeftHandedWeyl) ≃ₗ[ℂ]
     Matrix (Fin 2) (Fin 2) ℂ :=
-  (Basis.tensorProduct dualLeftBasis dualLeftBasis).repr ≪≫ₗ
+  (Basis.tensorProduct DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
 /-- Expanding `dualLeftdualLeftToMatrix` in terms of the standard basis. -/
 lemma dualLeftdualLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
     dualLeftdualLeftToMatrix.symm M = ∑ i, ∑ j, M i j •
-      (dualLeftBasis i ⊗ₜ[ℂ] dualLeftBasis j) := by
+      (DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] DualLeftHandedWeyl.basis j) := by
   simp only [dualLeftdualLeftToMatrix, LinearEquiv.trans_symm, LinearEquiv.trans_apply,
     Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
   · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
-    exact congrArg _ (Basis.tensorProduct_apply dualLeftBasis dualLeftBasis i j)
+    exact congrArg _ (Basis.tensorProduct_apply
+      DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis i j)
   · simp
 
 /-- Equivalence of `leftHanded ⊗ dualLeftHanded` to `2 x 2` complex matrices. -/
 def leftDualLeftToMatrix : (LeftHandedWeyl ⊗[ℂ] DualLeftHandedWeyl) ≃ₗ[ℂ]
     Matrix (Fin 2) (Fin 2) ℂ :=
-  (Basis.tensorProduct leftBasis dualLeftBasis).repr ≪≫ₗ
+  (Basis.tensorProduct LeftHandedWeyl.basis DualLeftHandedWeyl.basis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
 /-- Expanding `leftDualLeftToMatrix` in terms of the standard basis. -/
 lemma leftDualLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
-    leftDualLeftToMatrix.symm M = ∑ i, ∑ j, M i j • (leftBasis i ⊗ₜ[ℂ] dualLeftBasis j) := by
+    leftDualLeftToMatrix.symm M = ∑ i, ∑ j, M i j •
+      (LeftHandedWeyl.basis i ⊗ₜ[ℂ] DualLeftHandedWeyl.basis j) := by
   simp only [leftDualLeftToMatrix, LinearEquiv.trans_symm, LinearEquiv.trans_apply,
     Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
   · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
-    exact congrArg _ (Basis.tensorProduct_apply leftBasis dualLeftBasis i j)
+    exact congrArg _ (Basis.tensorProduct_apply LeftHandedWeyl.basis DualLeftHandedWeyl.basis i j)
   · simp
 
 /-- Equivalence of `dualLeftHanded ⊗ leftHanded` to `2 x 2` complex matrices. -/
 def dualLeftLeftToMatrix : (DualLeftHandedWeyl ⊗[ℂ] LeftHandedWeyl) ≃ₗ[ℂ]
     Matrix (Fin 2) (Fin 2) ℂ :=
-  (Basis.tensorProduct dualLeftBasis leftBasis).repr ≪≫ₗ
+  (Basis.tensorProduct DualLeftHandedWeyl.basis LeftHandedWeyl.basis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
 /-- Expanding `dualLeftLeftToMatrix` in terms of the standard basis. -/
 lemma dualLeftLeftToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
-    dualLeftLeftToMatrix.symm M = ∑ i, ∑ j, M i j • (dualLeftBasis i ⊗ₜ[ℂ] leftBasis j) := by
+    dualLeftLeftToMatrix.symm M = ∑ i, ∑ j, M i j •
+      (DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] LeftHandedWeyl.basis j) := by
   simp only [dualLeftLeftToMatrix, LinearEquiv.trans_symm, LinearEquiv.trans_apply,
     Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
   · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
-    exact congrArg _ (Basis.tensorProduct_apply dualLeftBasis leftBasis i j)
+    exact congrArg _ (Basis.tensorProduct_apply DualLeftHandedWeyl.basis LeftHandedWeyl.basis i j)
   · simp
 
 /-- Equivalence of `rightHanded ⊗ rightHanded` to `2 x 2` complex matrices. -/
 def rightRightToMatrix : (RightHandedWeyl ⊗[ℂ] RightHandedWeyl) ≃ₗ[ℂ]
     Matrix (Fin 2) (Fin 2) ℂ :=
-  (Basis.tensorProduct rightBasis rightBasis).repr ≪≫ₗ
+  (Basis.tensorProduct RightHandedWeyl.basis RightHandedWeyl.basis).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
+    rightRightToMatrix.symm M = ∑ i, ∑ j, M i j •
+      (RightHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis j) := by
   simp only [rightRightToMatrix, LinearEquiv.trans_symm, LinearEquiv.trans_apply,
     Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
   · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
-    exact congrArg _ (Basis.tensorProduct_apply rightBasis rightBasis i j)
+    exact congrArg _ (Basis.tensorProduct_apply RightHandedWeyl.basis RightHandedWeyl.basis i j)
   · simp
 
 /-- Equivalence of `dualRightHanded ⊗ dualRightHanded` to `2 x 2` complex matrices. -/
 def dualRightDualRightToMatrix : (DualRightHandedWeyl ⊗[ℂ] DualRightHandedWeyl) ≃ₗ[ℂ]
     Matrix (Fin 2) (Fin 2) ℂ :=
-  (Basis.tensorProduct dualRightBasis dualRightBasis).repr ≪≫ₗ
+  (Basis.tensorProduct DualRightHandedWeyl.basis DualRightHandedWeyl.basis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
 /-- Expanding `dualRightDualRightToMatrix` in terms of the standard basis. -/
 lemma dualRightDualRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
     dualRightDualRightToMatrix.symm M =
-    ∑ i, ∑ j, M i j • (dualRightBasis i ⊗ₜ[ℂ] dualRightBasis j) := by
+    ∑ i, ∑ j, M i j • (DualRightHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis j) := by
   simp only [dualRightDualRightToMatrix, LinearEquiv.trans_symm, LinearEquiv.trans_apply,
     Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
   · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
-    exact congrArg _ (Basis.tensorProduct_apply dualRightBasis dualRightBasis i j)
+    exact congrArg _
+      (Basis.tensorProduct_apply DualRightHandedWeyl.basis DualRightHandedWeyl.basis i j)
   · simp
 
 /-- Equivalence of `rightHanded ⊗ dualRightHanded` to `2 x 2` complex matrices. -/
 def rightDualRightToMatrix : (RightHandedWeyl ⊗[ℂ] DualRightHandedWeyl) ≃ₗ[ℂ]
     Matrix (Fin 2) (Fin 2) ℂ :=
-  (Basis.tensorProduct rightBasis dualRightBasis).repr ≪≫ₗ
+  (Basis.tensorProduct RightHandedWeyl.basis DualRightHandedWeyl.basis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
 /-- Expanding `rightDualRightToMatrix` in terms of the standard basis. -/
 lemma rightDualRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
-    rightDualRightToMatrix.symm M = ∑ i, ∑ j, M i j • (rightBasis i ⊗ₜ[ℂ] dualRightBasis j) := by
+    rightDualRightToMatrix.symm M = ∑ i, ∑ j, M i j •
+      (RightHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis j) := by
   simp only [rightDualRightToMatrix, LinearEquiv.trans_symm, LinearEquiv.trans_apply,
     Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
   · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
-    exact congrArg _ (Basis.tensorProduct_apply rightBasis dualRightBasis i j)
+    exact congrArg _ (Basis.tensorProduct_apply RightHandedWeyl.basis DualRightHandedWeyl.basis i j)
   · simp
 
 /-- Equivalence of `dualRightHanded ⊗ rightHanded` to `2 x 2` complex matrices. -/
 def dualRightRightToMatrix : (DualRightHandedWeyl ⊗[ℂ] RightHandedWeyl) ≃ₗ[ℂ]
     Matrix (Fin 2) (Fin 2) ℂ :=
-  (Basis.tensorProduct dualRightBasis rightBasis).repr ≪≫ₗ
+  (Basis.tensorProduct DualRightHandedWeyl.basis RightHandedWeyl.basis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
 /-- Expanding `dualRightRightToMatrix` in terms of the standard basis. -/
 lemma dualRightRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
-    dualRightRightToMatrix.symm M = ∑ i, ∑ j, M i j • (dualRightBasis i ⊗ₜ[ℂ] rightBasis j) := by
+    dualRightRightToMatrix.symm M = ∑ i, ∑ j, M i j •
+      (DualRightHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis j) := by
   simp only [dualRightRightToMatrix, LinearEquiv.trans_symm, LinearEquiv.trans_apply,
     Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
   · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
-    exact congrArg _ (Basis.tensorProduct_apply dualRightBasis rightBasis i j)
+    exact congrArg _ (Basis.tensorProduct_apply DualRightHandedWeyl.basis RightHandedWeyl.basis i j)
   · simp
 
 /-- Equivalence of `dualLeftHanded ⊗ dualRightHanded` to `2 x 2` complex matrices. -/
 def dualLeftDualRightToMatrix : (DualLeftHandedWeyl ⊗[ℂ] DualRightHandedWeyl) ≃ₗ[ℂ]
     Matrix (Fin 2) (Fin 2) ℂ :=
-  (Basis.tensorProduct dualLeftBasis dualRightBasis).repr ≪≫ₗ
+  (Basis.tensorProduct DualLeftHandedWeyl.basis DualRightHandedWeyl.basis).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2) ≪≫ₗ
   LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)
 
 /-- Expanding `dualLeftDualRightToMatrix` in terms of the standard basis. -/
 lemma dualLeftDualRightToMatrix_symm_expand_tmul (M : Matrix (Fin 2) (Fin 2) ℂ) :
     dualLeftDualRightToMatrix.symm M = ∑ i, ∑ j, M i j •
-      (dualLeftBasis i ⊗ₜ[ℂ] dualRightBasis j) := by
+      (DualLeftHandedWeyl.basis i ⊗ₜ[ℂ] DualRightHandedWeyl.basis j) := by
   simp only [dualLeftDualRightToMatrix, LinearEquiv.trans_symm, LinearEquiv.trans_apply,
     Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
   · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
-    exact congrArg _ (Basis.tensorProduct_apply dualLeftBasis dualRightBasis i j)
+    exact congrArg _
+      (Basis.tensorProduct_apply DualLeftHandedWeyl.basis DualRightHandedWeyl.basis i j)
   · simp
 
 /-- Equivalence of `leftHanded ⊗ rightHanded` to `2 x 2` complex matrices. -/
 def leftRightToMatrix : (LeftHandedWeyl ⊗[ℂ] RightHandedWeyl) ≃ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ :=
-  (Basis.tensorProduct leftBasis rightBasis).repr ≪≫ₗ
+  (Basis.tensorProduct LeftHandedWeyl.basis RightHandedWeyl.basis).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
+    leftRightToMatrix.symm M = ∑ i, ∑ j, M i j •
+      (LeftHandedWeyl.basis i ⊗ₜ[ℂ] RightHandedWeyl.basis j) := by
   simp only [leftRightToMatrix, LinearEquiv.trans_symm, LinearEquiv.trans_apply,
     Basis.repr_symm_apply]
   rw [Finsupp.linearCombination_apply_of_mem_supported ℂ (s := Finset.univ)]
   · rw [Fintype.sum_prod_type]
     refine Finset.sum_congr rfl (fun i _ => Finset.sum_congr rfl (fun j _ => ?_))
-    exact congrArg _ (Basis.tensorProduct_apply leftBasis rightBasis i j)
+    exact congrArg _ (Basis.tensorProduct_apply LeftHandedWeyl.basis RightHandedWeyl.basis i j)
   · simp
 
 /-- The coercion of `Finsupp.linearEquivFunOnFinite` to a function is the underlying
@@ -225,25 +235,29 @@ set_option backward.isDefEq.respectTransparency false in
 /-- The group action of `SL(2,ℂ)` on `leftHanded ⊗ leftHanded` is equivalent to
   `M.1 * leftLeftToMatrix v * (M.1)ᵀ`. -/
 lemma leftLeftToMatrix_ρ (v : (LeftHandedWeyl ⊗[ℂ] LeftHandedWeyl)) (M : SL(2,ℂ)) :
-    leftLeftToMatrix (TensorProduct.map (leftHandedRep M) (leftHandedRep M) v) =
+    leftLeftToMatrix (TensorProduct.map (LeftHandedWeyl.rep M) (LeftHandedWeyl.rep M) v) =
     M.1 * leftLeftToMatrix v * (M.1)ᵀ := by
   nth_rewrite 1 [leftLeftToMatrix]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
-      (leftBasis.tensorProduct leftBasis) (leftBasis.tensorProduct leftBasis)
-      (TensorProduct.map (leftHandedRep M) (leftHandedRep M)))
+      (LeftHandedWeyl.basis.tensorProduct LeftHandedWeyl.basis)
+        (LeftHandedWeyl.basis.tensorProduct LeftHandedWeyl.basis)
+      (TensorProduct.map (LeftHandedWeyl.rep M) (LeftHandedWeyl.rep M)))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
-      ((leftBasis.tensorProduct leftBasis).repr (v))))
+      ((LeftHandedWeyl.basis.tensorProduct LeftHandedWeyl.basis).repr (v))))
   · apply congrArg
-    have h1 := (LinearMap.toMatrix_mulVec_repr (leftBasis.tensorProduct leftBasis)
-      (leftBasis.tensorProduct leftBasis) (TensorProduct.map (leftHandedRep M) (leftHandedRep M)) v)
+    have h1 := (LinearMap.toMatrix_mulVec_repr (LeftHandedWeyl.basis.tensorProduct
+      LeftHandedWeyl.basis)
+      (LeftHandedWeyl.basis.tensorProduct LeftHandedWeyl.basis)
+        (TensorProduct.map (LeftHandedWeyl.rep M) (LeftHandedWeyl.rep M)) v)
     simp only [coe_linearEquivFunOnFinite]
     rw [h1]
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix leftBasis leftBasis) (leftHandedRep M))
-        ((LinearMap.toMatrix leftBasis leftBasis) (leftHandedRep M)) (i, j) k)
+        ((LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis) (LeftHandedWeyl.rep M))
+        ((LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis)
+          (LeftHandedWeyl.rep M)) (i, j) k)
         * leftLeftToMatrix v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
@@ -258,7 +272,7 @@ lemma leftLeftToMatrix_ρ (v : (LeftHandedWeyl ⊗[ℂ] LeftHandedWeyl)) (M : SL
   funext x
   congr
   funext x1
-  simp only [leftBasis_ρ_apply]
+  simp only [LeftHandedWeyl.rep_toMatrix]
   rw [mul_assoc]
   nth_rewrite 2 [mul_comm]
   rw [← mul_assoc]
@@ -267,26 +281,31 @@ set_option backward.isDefEq.respectTransparency false in
 /-- The group action of `SL(2,ℂ)` on `dualLeftHanded ⊗ dualLeftHanded` is equivalent to
   `(M.1⁻¹)ᵀ * leftLeftToMatrix v * (M.1⁻¹)`. -/
 lemma dualLeftdualLeftToMatrix_ρ (v : (DualLeftHandedWeyl ⊗[ℂ] DualLeftHandedWeyl)) (M : SL(2,ℂ)) :
-    dualLeftdualLeftToMatrix (TensorProduct.map (dualLeftHandedRep M) (dualLeftHandedRep M) v) =
+    dualLeftdualLeftToMatrix (TensorProduct.map (DualLeftHandedWeyl.rep M)
+      (DualLeftHandedWeyl.rep M) v) =
     (M.1⁻¹)ᵀ * dualLeftdualLeftToMatrix v * (M.1⁻¹) := by
   nth_rewrite 1 [dualLeftdualLeftToMatrix]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
-      (dualLeftBasis.tensorProduct dualLeftBasis) (dualLeftBasis.tensorProduct dualLeftBasis)
-      (TensorProduct.map (dualLeftHandedRep M) (dualLeftHandedRep M)))
+      (DualLeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis)
+        (DualLeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis)
+      (TensorProduct.map (DualLeftHandedWeyl.rep M) (DualLeftHandedWeyl.rep M)))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
-      ((dualLeftBasis.tensorProduct dualLeftBasis).repr v)))
+      ((DualLeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis).repr v)))
   · apply congrArg
-    have h1 := (LinearMap.toMatrix_mulVec_repr (dualLeftBasis.tensorProduct dualLeftBasis)
-      (dualLeftBasis.tensorProduct dualLeftBasis)
-      (TensorProduct.map (dualLeftHandedRep M) (dualLeftHandedRep M)) v)
+    have h1 := (LinearMap.toMatrix_mulVec_repr (DualLeftHandedWeyl.basis.tensorProduct
+      DualLeftHandedWeyl.basis)
+      (DualLeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis)
+      (TensorProduct.map (DualLeftHandedWeyl.rep M) (DualLeftHandedWeyl.rep M)) v)
     simp only [coe_linearEquivFunOnFinite]
     rw [h1]
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix dualLeftBasis dualLeftBasis) (dualLeftHandedRep M))
-        ((LinearMap.toMatrix dualLeftBasis dualLeftBasis) (dualLeftHandedRep M)) (i, j) k)
+        ((LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis)
+          (DualLeftHandedWeyl.rep M))
+        ((LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis)
+          (DualLeftHandedWeyl.rep M)) (i, j) k)
         * dualLeftdualLeftToMatrix v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
@@ -303,33 +322,36 @@ lemma dualLeftdualLeftToMatrix_ρ (v : (DualLeftHandedWeyl ⊗[ℂ] DualLeftHand
   funext x
   congr
   funext x1
-  simp only [dualLeftBasis_ρ_apply, transpose_apply]
+  simp only [DualLeftHandedWeyl.rep_toMatrix, transpose_apply]
   ring
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The group action of `SL(2,ℂ)` on `leftHanded ⊗ dualLeftHanded` is equivalent to
   `M.1 * leftDualLeftToMatrix v * (M.1⁻¹)`. -/
 lemma leftDualLeftToMatrix_ρ (v : (LeftHandedWeyl ⊗[ℂ] DualLeftHandedWeyl)) (M : SL(2,ℂ)) :
-    leftDualLeftToMatrix (TensorProduct.map (leftHandedRep M) (dualLeftHandedRep M) v) =
+    leftDualLeftToMatrix (TensorProduct.map (LeftHandedWeyl.rep M) (DualLeftHandedWeyl.rep M) v) =
     M.1 * leftDualLeftToMatrix v * (M.1⁻¹) := by
   nth_rewrite 1 [leftDualLeftToMatrix]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
-      (leftBasis.tensorProduct dualLeftBasis) (leftBasis.tensorProduct dualLeftBasis)
-      (TensorProduct.map (leftHandedRep M) (dualLeftHandedRep M)))
+      (LeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis)
+        (LeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis)
+      (TensorProduct.map (LeftHandedWeyl.rep M) (DualLeftHandedWeyl.rep M)))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
-      ((leftBasis.tensorProduct dualLeftBasis).repr (v))))
+      ((LeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis).repr (v))))
   · apply congrArg
-    have h1 := (LinearMap.toMatrix_mulVec_repr (leftBasis.tensorProduct dualLeftBasis)
-      (leftBasis.tensorProduct dualLeftBasis)
-      (TensorProduct.map (leftHandedRep M) (dualLeftHandedRep M)) v)
+    have h1 := (LinearMap.toMatrix_mulVec_repr (LeftHandedWeyl.basis.tensorProduct
+        DualLeftHandedWeyl.basis)
+      (LeftHandedWeyl.basis.tensorProduct DualLeftHandedWeyl.basis)
+      (TensorProduct.map (LeftHandedWeyl.rep M) (DualLeftHandedWeyl.rep M)) v)
     simp only [coe_linearEquivFunOnFinite]
     rw [h1]
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix leftBasis leftBasis) (leftHandedRep M))
-        ((LinearMap.toMatrix dualLeftBasis dualLeftBasis) (dualLeftHandedRep M)) (i, j) k)
+        ((LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis) (LeftHandedWeyl.rep M))
+        ((LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis)
+          (DualLeftHandedWeyl.rep M)) (i, j) k)
         * leftDualLeftToMatrix v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply]
@@ -344,33 +366,37 @@ lemma leftDualLeftToMatrix_ρ (v : (LeftHandedWeyl ⊗[ℂ] DualLeftHandedWeyl))
   funext x
   congr
   funext x1
-  simp only [leftBasis_ρ_apply, dualLeftBasis_ρ_apply, transpose_apply]
+  simp only [LeftHandedWeyl.rep_toMatrix, DualLeftHandedWeyl.rep_toMatrix, transpose_apply]
   ring
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The group action of `SL(2,ℂ)` on `dualLeftHanded ⊗ leftHanded` is equivalent to
   `(M.1⁻¹)ᵀ * leftDualLeftToMatrix v * (M.1)ᵀ`. -/
 lemma dualLeftLeftToMatrix_ρ (v : (DualLeftHandedWeyl ⊗[ℂ] LeftHandedWeyl)) (M : SL(2,ℂ)) :
-    dualLeftLeftToMatrix (TensorProduct.map (dualLeftHandedRep M) (leftHandedRep M) v) =
+    dualLeftLeftToMatrix (TensorProduct.map (DualLeftHandedWeyl.rep M) (LeftHandedWeyl.rep M) v) =
     (M.1⁻¹)ᵀ * dualLeftLeftToMatrix v * (M.1)ᵀ := by
   nth_rewrite 1 [dualLeftLeftToMatrix]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
-      (dualLeftBasis.tensorProduct leftBasis) (dualLeftBasis.tensorProduct leftBasis)
-      (TensorProduct.map (dualLeftHandedRep M) (leftHandedRep M)))
+      (DualLeftHandedWeyl.basis.tensorProduct LeftHandedWeyl.basis)
+        (DualLeftHandedWeyl.basis.tensorProduct LeftHandedWeyl.basis)
+      (TensorProduct.map (DualLeftHandedWeyl.rep M) (LeftHandedWeyl.rep M)))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
-      ((dualLeftBasis.tensorProduct leftBasis).repr (v))))
+      ((DualLeftHandedWeyl.basis.tensorProduct LeftHandedWeyl.basis).repr (v))))
   · apply congrArg
-    have h1 := (LinearMap.toMatrix_mulVec_repr (dualLeftBasis.tensorProduct leftBasis)
-      (dualLeftBasis.tensorProduct leftBasis)
-      (TensorProduct.map (dualLeftHandedRep M) (leftHandedRep M)) v)
+    have h1 := (LinearMap.toMatrix_mulVec_repr (DualLeftHandedWeyl.basis.tensorProduct
+        LeftHandedWeyl.basis)
+      (DualLeftHandedWeyl.basis.tensorProduct LeftHandedWeyl.basis)
+      (TensorProduct.map (DualLeftHandedWeyl.rep M) (LeftHandedWeyl.rep M)) v)
     simp only [coe_linearEquivFunOnFinite]
     rw [h1]
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix dualLeftBasis dualLeftBasis) (dualLeftHandedRep M))
-        ((LinearMap.toMatrix leftBasis leftBasis) (leftHandedRep M)) (i, j) k)
+        ((LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis)
+          (DualLeftHandedWeyl.rep M))
+        ((LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis)
+          (LeftHandedWeyl.rep M)) (i, j) k)
         * dualLeftLeftToMatrix v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
@@ -385,33 +411,36 @@ lemma dualLeftLeftToMatrix_ρ (v : (DualLeftHandedWeyl ⊗[ℂ] LeftHandedWeyl))
   funext x
   congr
   funext x1
-  simp only [dualLeftBasis_ρ_apply, transpose_apply, leftBasis_ρ_apply]
+  simp only [DualLeftHandedWeyl.rep_toMatrix, transpose_apply, LeftHandedWeyl.rep_toMatrix]
   ring
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The group action of `SL(2,ℂ)` on `rightHanded ⊗ rightHanded` is equivalent to
   `(M.1.map star) * rightRightToMatrix v * ((M.1.map star))ᵀ`. -/
 lemma rightRightToMatrix_ρ (v : (RightHandedWeyl ⊗[ℂ] RightHandedWeyl)) (M : SL(2,ℂ)) :
-    rightRightToMatrix (TensorProduct.map (rightHandedRep M) (rightHandedRep M) v) =
+    rightRightToMatrix (TensorProduct.map (RightHandedWeyl.rep M) (RightHandedWeyl.rep M) v) =
     (M.1.map star) * rightRightToMatrix v * ((M.1.map star))ᵀ := by
   nth_rewrite 1 [rightRightToMatrix]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
-      (rightBasis.tensorProduct rightBasis) (rightBasis.tensorProduct rightBasis)
-      (TensorProduct.map (rightHandedRep M) (rightHandedRep M)))
+      (RightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis)
+        (RightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis)
+      (TensorProduct.map (RightHandedWeyl.rep M) (RightHandedWeyl.rep M)))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
-      ((rightBasis.tensorProduct rightBasis).repr (v))))
+      ((RightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis).repr (v))))
   · apply congrArg
-    have h1 := (LinearMap.toMatrix_mulVec_repr (rightBasis.tensorProduct rightBasis)
-      (rightBasis.tensorProduct rightBasis)
-      (TensorProduct.map (rightHandedRep M) (rightHandedRep M)) v)
+    have h1 := (LinearMap.toMatrix_mulVec_repr (RightHandedWeyl.basis.tensorProduct
+        RightHandedWeyl.basis)
+      (RightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis)
+      (TensorProduct.map (RightHandedWeyl.rep M) (RightHandedWeyl.rep M)) v)
     simp only [coe_linearEquivFunOnFinite]
     rw [h1]
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix rightBasis rightBasis) (rightHandedRep M))
-        ((LinearMap.toMatrix rightBasis rightBasis) (rightHandedRep M)) (i, j) k)
+        ((LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis) (RightHandedWeyl.rep M))
+        ((LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis)
+          (RightHandedWeyl.rep M)) (i, j) k)
         * rightRightToMatrix v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
@@ -427,7 +456,7 @@ lemma rightRightToMatrix_ρ (v : (RightHandedWeyl ⊗[ℂ] RightHandedWeyl)) (M
   funext x
   congr
   funext x1
-  simp only [rightBasis_ρ_apply]
+  simp only [RightHandedWeyl.rep_toMatrix]
   ring
 
 set_option backward.isDefEq.respectTransparency false in
@@ -435,26 +464,31 @@ set_option backward.isDefEq.respectTransparency false in
   `((M.1⁻¹).conjTranspose * rightRightToMatrix v * (((M.1⁻¹).conjTranspose)ᵀ`. -/
 lemma dualRightDualRightToMatrix_ρ (v : (DualRightHandedWeyl ⊗[ℂ] DualRightHandedWeyl))
     (M : SL(2,ℂ)) :
-    dualRightDualRightToMatrix (TensorProduct.map (dualRightHandedRep M) (dualRightHandedRep M) v) =
+    dualRightDualRightToMatrix (TensorProduct.map (DualRightHandedWeyl.rep M)
+      (DualRightHandedWeyl.rep M) v) =
     ((M.1⁻¹).conjTranspose) * dualRightDualRightToMatrix v * (((M.1⁻¹).conjTranspose)ᵀ) := by
   nth_rewrite 1 [dualRightDualRightToMatrix]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
-      (dualRightBasis.tensorProduct dualRightBasis) (dualRightBasis.tensorProduct dualRightBasis)
-      (TensorProduct.map (dualRightHandedRep M) (dualRightHandedRep M)))
+      (DualRightHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis)
+        (DualRightHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis)
+      (TensorProduct.map (DualRightHandedWeyl.rep M) (DualRightHandedWeyl.rep M)))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
-      ((dualRightBasis.tensorProduct dualRightBasis).repr (v))))
+      ((DualRightHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis).repr (v))))
   · apply congrArg
-    have h1 := (LinearMap.toMatrix_mulVec_repr (dualRightBasis.tensorProduct dualRightBasis)
-      (dualRightBasis.tensorProduct dualRightBasis)
-      (TensorProduct.map (dualRightHandedRep M) (dualRightHandedRep M)) v)
+    have h1 := (LinearMap.toMatrix_mulVec_repr (DualRightHandedWeyl.basis.tensorProduct
+        DualRightHandedWeyl.basis)
+      (DualRightHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis)
+      (TensorProduct.map (DualRightHandedWeyl.rep M) (DualRightHandedWeyl.rep M)) v)
     simp only [coe_linearEquivFunOnFinite]
     rw [h1]
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix dualRightBasis dualRightBasis) (dualRightHandedRep M))
-        ((LinearMap.toMatrix dualRightBasis dualRightBasis) (dualRightHandedRep M)) (i, j) k)
+        ((LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis)
+          (DualRightHandedWeyl.rep M))
+        ((LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis)
+          (DualRightHandedWeyl.rep M)) (i, j) k)
         * dualRightDualRightToMatrix v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
@@ -470,33 +504,38 @@ lemma dualRightDualRightToMatrix_ρ (v : (DualRightHandedWeyl ⊗[ℂ] DualRight
   funext x
   congr
   funext x1
-  simp only [dualRightBasis_ρ_apply]
+  simp only [DualRightHandedWeyl.rep_toMatrix]
   ring
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The group action of `SL(2,ℂ)` on `rightHanded ⊗ dualRightHanded` is equivalent to
   `(M.1.map star) * rightDualRightToMatrix v * (((M.1⁻¹).conjTranspose)ᵀ`. -/
 lemma rightDualRightToMatrix_ρ (v : (RightHandedWeyl ⊗[ℂ] DualRightHandedWeyl)) (M : SL(2,ℂ)) :
-    rightDualRightToMatrix (TensorProduct.map (rightHandedRep M) (dualRightHandedRep M) v) =
+    rightDualRightToMatrix (TensorProduct.map (RightHandedWeyl.rep M)
+      (DualRightHandedWeyl.rep M) v) =
     (M.1.map star) * rightDualRightToMatrix v * (((M.1⁻¹).conjTranspose)ᵀ) := by
   nth_rewrite 1 [rightDualRightToMatrix]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
-      (rightBasis.tensorProduct dualRightBasis) (rightBasis.tensorProduct dualRightBasis)
-      (TensorProduct.map (rightHandedRep M) (dualRightHandedRep M)))
+      (RightHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis)
+        (RightHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis)
+      (TensorProduct.map (RightHandedWeyl.rep M) (DualRightHandedWeyl.rep M)))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
-      ((rightBasis.tensorProduct dualRightBasis).repr (v))))
+      ((RightHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis).repr (v))))
   · apply congrArg
-    have h1 := (LinearMap.toMatrix_mulVec_repr (rightBasis.tensorProduct dualRightBasis)
-    (rightBasis.tensorProduct dualRightBasis)
-    (TensorProduct.map (rightHandedRep M) (dualRightHandedRep M)) v)
+    have h1 := (LinearMap.toMatrix_mulVec_repr (RightHandedWeyl.basis.tensorProduct
+      DualRightHandedWeyl.basis)
+    (RightHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis)
+    (TensorProduct.map (RightHandedWeyl.rep M) (DualRightHandedWeyl.rep M)) v)
     simp only [coe_linearEquivFunOnFinite]
     rw [h1]
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix rightBasis rightBasis) (rightHandedRep M))
-        ((LinearMap.toMatrix dualRightBasis dualRightBasis) (dualRightHandedRep M)) (i, j) k)
+        ((LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis)
+          (RightHandedWeyl.rep M))
+        ((LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis)
+          (DualRightHandedWeyl.rep M)) (i, j) k)
         * rightDualRightToMatrix v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
@@ -512,33 +551,38 @@ lemma rightDualRightToMatrix_ρ (v : (RightHandedWeyl ⊗[ℂ] DualRightHandedWe
   funext x
   congr
   funext x1
-  simp only [rightBasis_ρ_apply, dualRightBasis_ρ_apply]
+  simp only [RightHandedWeyl.rep_toMatrix, DualRightHandedWeyl.rep_toMatrix]
   ring
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The group action of `SL(2,ℂ)` on `dualRightHanded ⊗ rightHanded` is equivalent to
   `((M.1⁻¹).conjTranspose * rightDualRightToMatrix v * ((M.1.map star)).ᵀ`. -/
 lemma dualRightRightToMatrix_ρ (v : (DualRightHandedWeyl ⊗[ℂ] RightHandedWeyl)) (M : SL(2,ℂ)) :
-    dualRightRightToMatrix (TensorProduct.map (dualRightHandedRep M) (rightHandedRep M) v) =
+    dualRightRightToMatrix (TensorProduct.map (DualRightHandedWeyl.rep M)
+      (RightHandedWeyl.rep M) v) =
     ((M.1⁻¹).conjTranspose) * dualRightRightToMatrix v * (M.1.map star)ᵀ := by
   nth_rewrite 1 [dualRightRightToMatrix]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
-      (dualRightBasis.tensorProduct rightBasis) (dualRightBasis.tensorProduct rightBasis)
-      (TensorProduct.map (dualRightHandedRep M) (rightHandedRep M)))
+      (DualRightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis)
+        (DualRightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis)
+      (TensorProduct.map (DualRightHandedWeyl.rep M) (RightHandedWeyl.rep M)))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
-      ((dualRightBasis.tensorProduct rightBasis).repr (v))))
+      ((DualRightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis).repr (v))))
   · apply congrArg
-    have h1 := (LinearMap.toMatrix_mulVec_repr (dualRightBasis.tensorProduct rightBasis)
-      (dualRightBasis.tensorProduct rightBasis)
-      (TensorProduct.map (dualRightHandedRep M) (rightHandedRep M)) v)
+    have h1 := (LinearMap.toMatrix_mulVec_repr
+      (DualRightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis)
+      (DualRightHandedWeyl.basis.tensorProduct RightHandedWeyl.basis)
+      (TensorProduct.map (DualRightHandedWeyl.rep M) (RightHandedWeyl.rep M)) v)
     simp only [coe_linearEquivFunOnFinite]
     rw [h1]
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix dualRightBasis dualRightBasis) (dualRightHandedRep M))
-        ((LinearMap.toMatrix rightBasis rightBasis) (rightHandedRep M)) (i, j) k)
+        ((LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis)
+          (DualRightHandedWeyl.rep M))
+        ((LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis)
+          (RightHandedWeyl.rep M)) (i, j) k)
         * dualRightRightToMatrix v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
@@ -555,32 +599,37 @@ lemma dualRightRightToMatrix_ρ (v : (DualRightHandedWeyl ⊗[ℂ] RightHandedWe
   funext x
   congr
   funext x1
-  simp only [dualRightBasis_ρ_apply, rightBasis_ρ_apply]
+  simp only [DualRightHandedWeyl.rep_toMatrix, RightHandedWeyl.rep_toMatrix]
   ring
 
 set_option backward.isDefEq.respectTransparency false in
 lemma dualLeftDualRightToMatrix_ρ (v : (DualLeftHandedWeyl ⊗[ℂ] DualRightHandedWeyl))
     (M : SL(2,ℂ)) :
-    dualLeftDualRightToMatrix (TensorProduct.map (dualLeftHandedRep M) (dualRightHandedRep M) v) =
+    dualLeftDualRightToMatrix (TensorProduct.map (DualLeftHandedWeyl.rep M)
+      (DualRightHandedWeyl.rep M) v) =
     (M.1⁻¹)ᵀ * dualLeftDualRightToMatrix v * ((M.1⁻¹).conjTranspose)ᵀ := by
   nth_rewrite 1 [dualLeftDualRightToMatrix]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
-      (dualLeftBasis.tensorProduct dualRightBasis) (dualLeftBasis.tensorProduct dualRightBasis)
-      (TensorProduct.map (dualLeftHandedRep M) (dualRightHandedRep M)))
+      (DualLeftHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis)
+        (DualLeftHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis)
+      (TensorProduct.map (DualLeftHandedWeyl.rep M) (DualRightHandedWeyl.rep M)))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
-      ((dualLeftBasis.tensorProduct dualRightBasis).repr (v))))
+      ((DualLeftHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis).repr (v))))
   · apply congrArg
-    have h1 := (LinearMap.toMatrix_mulVec_repr (dualLeftBasis.tensorProduct dualRightBasis)
-      (dualLeftBasis.tensorProduct dualRightBasis)
-      (TensorProduct.map (dualLeftHandedRep M) (dualRightHandedRep M)) v)
+    have h1 := (LinearMap.toMatrix_mulVec_repr (DualLeftHandedWeyl.basis.tensorProduct
+      DualRightHandedWeyl.basis)
+      (DualLeftHandedWeyl.basis.tensorProduct DualRightHandedWeyl.basis)
+      (TensorProduct.map (DualLeftHandedWeyl.rep M) (DualRightHandedWeyl.rep M)) v)
     simp only [coe_linearEquivFunOnFinite]
     rw [h1]
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix dualLeftBasis dualLeftBasis) (dualLeftHandedRep M))
-        ((LinearMap.toMatrix dualRightBasis dualRightBasis) (dualRightHandedRep M)) (i, j) k)
+        ((LinearMap.toMatrix DualLeftHandedWeyl.basis DualLeftHandedWeyl.basis)
+          (DualLeftHandedWeyl.rep M))
+        ((LinearMap.toMatrix DualRightHandedWeyl.basis DualRightHandedWeyl.basis)
+          (DualRightHandedWeyl.rep M)) (i, j) k)
         * dualLeftDualRightToMatrix v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
@@ -596,31 +645,34 @@ lemma dualLeftDualRightToMatrix_ρ (v : (DualLeftHandedWeyl ⊗[ℂ] DualRightHa
   funext x
   congr
   funext x1
-  simp only [dualLeftBasis_ρ_apply, transpose_apply, dualRightBasis_ρ_apply]
+  simp only [DualLeftHandedWeyl.rep_toMatrix, transpose_apply, DualRightHandedWeyl.rep_toMatrix]
   ring
 
 set_option backward.isDefEq.respectTransparency false in
 lemma leftRightToMatrix_ρ (v : (LeftHandedWeyl ⊗[ℂ] RightHandedWeyl)) (M : SL(2,ℂ)) :
-    leftRightToMatrix (TensorProduct.map (leftHandedRep M) (rightHandedRep M) v) =
+    leftRightToMatrix (TensorProduct.map (LeftHandedWeyl.rep M) (RightHandedWeyl.rep M) v) =
     M.1 * leftRightToMatrix v * (M.1)ᴴ := by
   nth_rewrite 1 [leftRightToMatrix]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℂ ℂ (Fin 2) (Fin 2)) ((LinearMap.toMatrix
-      (leftBasis.tensorProduct rightBasis) (leftBasis.tensorProduct rightBasis)
-      (TensorProduct.map (leftHandedRep M) (rightHandedRep M)))
+      (LeftHandedWeyl.basis.tensorProduct RightHandedWeyl.basis) (LeftHandedWeyl.basis.tensorProduct
+        RightHandedWeyl.basis)
+      (TensorProduct.map (LeftHandedWeyl.rep M) (RightHandedWeyl.rep M)))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℂ ℂ (Fin 2 × Fin 2))
-      ((leftBasis.tensorProduct rightBasis).repr (v))))
+      ((LeftHandedWeyl.basis.tensorProduct RightHandedWeyl.basis).repr (v))))
   · apply congrArg
-    have h1 := (LinearMap.toMatrix_mulVec_repr (leftBasis.tensorProduct rightBasis)
-      (leftBasis.tensorProduct rightBasis)
-      (TensorProduct.map (leftHandedRep M) (rightHandedRep M)) v)
+    have h1 := (LinearMap.toMatrix_mulVec_repr (LeftHandedWeyl.basis.tensorProduct
+      RightHandedWeyl.basis)
+      (LeftHandedWeyl.basis.tensorProduct RightHandedWeyl.basis)
+      (TensorProduct.map (LeftHandedWeyl.rep M) (RightHandedWeyl.rep M)) v)
     simp only [coe_linearEquivFunOnFinite]
     rw [h1]
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix leftBasis leftBasis) (leftHandedRep M))
-        ((LinearMap.toMatrix rightBasis rightBasis) (rightHandedRep M)) (i, j) k)
+        ((LinearMap.toMatrix LeftHandedWeyl.basis LeftHandedWeyl.basis) (LeftHandedWeyl.rep M))
+        ((LinearMap.toMatrix RightHandedWeyl.basis RightHandedWeyl.basis)
+          (RightHandedWeyl.rep M)) (i, j) k)
         * leftRightToMatrix v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply]
@@ -635,7 +687,7 @@ lemma leftRightToMatrix_ρ (v : (LeftHandedWeyl ⊗[ℂ] RightHandedWeyl)) (M :
   funext x
   congr
   funext x1
-  simp only [leftBasis_ρ_apply, rightBasis_ρ_apply]
+  simp only [LeftHandedWeyl.rep_toMatrix, RightHandedWeyl.rep_toMatrix]
   rw [Matrix.conjTranspose]
   simp only [RCLike.star_def, map_apply, transpose_apply]
   ring
@@ -647,14 +699,14 @@ lemma leftRightToMatrix_ρ (v : (LeftHandedWeyl ⊗[ℂ] RightHandedWeyl)) (M :
 -/
 
 lemma leftLeftToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
-    TensorProduct.map (leftHandedRep M) (leftHandedRep M) (leftLeftToMatrix.symm v) =
+    TensorProduct.map (LeftHandedWeyl.rep M) (LeftHandedWeyl.rep M) (leftLeftToMatrix.symm v) =
     leftLeftToMatrix.symm (M.1 * v * (M.1)ᵀ) := by
   have h1 := leftLeftToMatrix_ρ (leftLeftToMatrix.symm v) M
   simp only [LinearEquiv.apply_symm_apply] at h1
   rw [← h1, LinearEquiv.symm_apply_apply]
 
 lemma dualLeftdualLeftToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
-    TensorProduct.map (dualLeftHandedRep M) (dualLeftHandedRep M)
+    TensorProduct.map (DualLeftHandedWeyl.rep M) (DualLeftHandedWeyl.rep M)
       (dualLeftdualLeftToMatrix.symm v) =
     dualLeftdualLeftToMatrix.symm ((M.1⁻¹)ᵀ * v * (M.1⁻¹)) := by
   have h1 := dualLeftdualLeftToMatrix_ρ (dualLeftdualLeftToMatrix.symm v) M
@@ -662,28 +714,30 @@ lemma dualLeftdualLeftToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(
   rw [← h1, LinearEquiv.symm_apply_apply]
 
 lemma leftDualLeftToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
-    TensorProduct.map (leftHandedRep M) (dualLeftHandedRep M) (leftDualLeftToMatrix.symm v) =
+    TensorProduct.map (LeftHandedWeyl.rep M) (DualLeftHandedWeyl.rep M)
+      (leftDualLeftToMatrix.symm v) =
     leftDualLeftToMatrix.symm (M.1 * v * (M.1⁻¹)) := by
   have h1 := leftDualLeftToMatrix_ρ (leftDualLeftToMatrix.symm v) M
   simp only [LinearEquiv.apply_symm_apply] at h1
   rw [← h1, LinearEquiv.symm_apply_apply]
 
 lemma dualLeftLeftToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
-    TensorProduct.map (dualLeftHandedRep M) (leftHandedRep M) (dualLeftLeftToMatrix.symm v) =
+    TensorProduct.map (DualLeftHandedWeyl.rep M) (LeftHandedWeyl.rep M)
+      (dualLeftLeftToMatrix.symm v) =
     dualLeftLeftToMatrix.symm ((M.1⁻¹)ᵀ * v * (M.1)ᵀ) := by
   have h1 := dualLeftLeftToMatrix_ρ (dualLeftLeftToMatrix.symm v) M
   simp only [LinearEquiv.apply_symm_apply] at h1
   rw [← h1, LinearEquiv.symm_apply_apply]
 
 lemma rightRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
-    TensorProduct.map (rightHandedRep M) (rightHandedRep M) (rightRightToMatrix.symm v) =
+    TensorProduct.map (RightHandedWeyl.rep M) (RightHandedWeyl.rep M) (rightRightToMatrix.symm v) =
     rightRightToMatrix.symm ((M.1.map star) * v * ((M.1.map star))ᵀ) := by
   have h1 := rightRightToMatrix_ρ (rightRightToMatrix.symm v) M
   simp only [LinearEquiv.apply_symm_apply] at h1
   rw [← h1, LinearEquiv.symm_apply_apply]
 
 lemma dualRightDualRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
-    TensorProduct.map (dualRightHandedRep M) (dualRightHandedRep M)
+    TensorProduct.map (DualRightHandedWeyl.rep M) (DualRightHandedWeyl.rep M)
       (dualRightDualRightToMatrix.symm v) =
     dualRightDualRightToMatrix.symm (((M.1⁻¹).conjTranspose) * v * ((M.1⁻¹).conjTranspose)ᵀ) := by
   have h1 := dualRightDualRightToMatrix_ρ (dualRightDualRightToMatrix.symm v) M
@@ -691,21 +745,23 @@ lemma dualRightDualRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : S
   rw [← h1, LinearEquiv.symm_apply_apply]
 
 lemma rightDualRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
-    TensorProduct.map (rightHandedRep M) (dualRightHandedRep M) (rightDualRightToMatrix.symm v) =
+    TensorProduct.map (RightHandedWeyl.rep M) (DualRightHandedWeyl.rep M)
+      (rightDualRightToMatrix.symm v) =
     rightDualRightToMatrix.symm ((M.1.map star) * v * (((M.1⁻¹).conjTranspose)ᵀ)) := by
   have h1 := rightDualRightToMatrix_ρ (rightDualRightToMatrix.symm v) M
   simp only [LinearEquiv.apply_symm_apply] at h1
   rw [← h1, LinearEquiv.symm_apply_apply]
 
 lemma dualRightRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
-    TensorProduct.map (dualRightHandedRep M) (rightHandedRep M) (dualRightRightToMatrix.symm v) =
+    TensorProduct.map (DualRightHandedWeyl.rep M) (RightHandedWeyl.rep M)
+      (dualRightRightToMatrix.symm v) =
     dualRightRightToMatrix.symm (((M.1⁻¹).conjTranspose) * v * (M.1.map star)ᵀ) := by
   have h1 := dualRightRightToMatrix_ρ (dualRightRightToMatrix.symm v) M
   simp only [LinearEquiv.apply_symm_apply] at h1
   rw [← h1, LinearEquiv.symm_apply_apply]
 
 lemma dualLeftDualRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
-    TensorProduct.map (dualLeftHandedRep M) (dualRightHandedRep M)
+    TensorProduct.map (DualLeftHandedWeyl.rep M) (DualRightHandedWeyl.rep M)
       (dualLeftDualRightToMatrix.symm v) =
     dualLeftDualRightToMatrix.symm ((M.1⁻¹)ᵀ * v * ((M.1⁻¹).conjTranspose)ᵀ) := by
   have h1 := dualLeftDualRightToMatrix_ρ (dualLeftDualRightToMatrix.symm v) M
@@ -713,7 +769,7 @@ lemma dualLeftDualRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL
   rw [← h1, LinearEquiv.symm_apply_apply]
 
 lemma leftRightToMatrix_ρ_symm (v : Matrix (Fin 2) (Fin 2) ℂ) (M : SL(2,ℂ)) :
-    TensorProduct.map (leftHandedRep M) (rightHandedRep M) (leftRightToMatrix.symm v) =
+    TensorProduct.map (LeftHandedWeyl.rep M) (RightHandedWeyl.rep M) (leftRightToMatrix.symm v) =
     leftRightToMatrix.symm (M.1 * v * (M.1)ᴴ) := by
   have h1 := leftRightToMatrix_ρ (leftRightToMatrix.symm v) M
   simp only [LinearEquiv.apply_symm_apply] at h1
@@ -723,7 +779,7 @@ open Lorentz
 
 lemma dualLeftDualRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2) ℂ)
     (hv : IsSelfAdjoint v) (M : SL(2,ℂ)) :
-    TensorProduct.map (dualLeftHandedRep M) (dualRightHandedRep M)
+    TensorProduct.map (DualLeftHandedWeyl.rep M) (DualRightHandedWeyl.rep M)
       (dualLeftDualRightToMatrix.symm v) =
     dualLeftDualRightToMatrix.symm (SL2C.toSelfAdjointMap (M.transpose⁻¹) ⟨v, hv⟩) := by
   rw [dualLeftDualRightToMatrix_ρ_symm]
@@ -741,7 +797,7 @@ lemma dualLeftDualRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2)
 
 lemma leftRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2) ℂ)
     (hv : IsSelfAdjoint v) (M : SL(2,ℂ)) :
-    TensorProduct.map (leftHandedRep M) (rightHandedRep M) (leftRightToMatrix.symm v) =
+    TensorProduct.map (LeftHandedWeyl.rep M) (RightHandedWeyl.rep M) (leftRightToMatrix.symm v) =
     leftRightToMatrix.symm (SL2C.toSelfAdjointMap M ⟨v, hv⟩) := by
   rw [leftRightToMatrix_ρ_symm]
   rfl
diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Unit.lean b/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Unit.lean
index 244f4e7d2..38f5c77b8 100644
--- a/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Unit.lean
+++ b/Physlib/Relativity/Tensors/ComplexTensor/Weyl/Unit.lean
@@ -32,7 +32,8 @@ def leftDualLeftUnitVal : (LeftHandedWeyl ⊗[ℂ] DualLeftHandedWeyl) :=
 
 /-- Expansion of `leftDualLeftUnitVal` into the basis. -/
 lemma leftDualLeftUnitVal_expand_tmul : leftDualLeftUnitVal =
-    leftBasis 0 ⊗ₜ[ℂ] dualLeftBasis 0 + leftBasis 1 ⊗ₜ[ℂ] dualLeftBasis 1 := by
+    LeftHandedWeyl.basis 0 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 0 +
+      LeftHandedWeyl.basis 1 ⊗ₜ[ℂ] DualLeftHandedWeyl.basis 1 := by
   simp only [leftDualLeftUnitVal, Fin.isValue]
   erw [leftDualLeftToMatrix_symm_expand_tmul]
   simp only [Fin.sum_univ_two, Fin.isValue, one_apply_eq, one_smul, ne_eq, zero_ne_one,
@@ -41,7 +42,7 @@ lemma leftDualLeftUnitVal_expand_tmul : leftDualLeftUnitVal =
 /-- The left-dual-left unit `δᵃₐ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ leftHanded ⊗ dualLeftHanded `,
   manifesting the invariance under the `SL(2,ℂ)` action. -/
 def leftDualLeftUnit : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
-    (leftHandedRep.tprod dualLeftHandedRep) where
+    (LeftHandedWeyl.rep.tprod DualLeftHandedWeyl.rep) where
   toFun := fun a =>
     let a' : ℂ := a
     a' • leftDualLeftUnitVal
@@ -53,7 +54,8 @@ def leftDualLeftUnit : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMa
   isIntertwining' M := by
     refine LinearMap.ext fun x : ℂ => ?_
     change x • leftDualLeftUnitVal =
-      (TensorProduct.map (leftHandedRep M) (dualLeftHandedRep M)) (x • leftDualLeftUnitVal)
+      (TensorProduct.map (LeftHandedWeyl.rep M) (DualLeftHandedWeyl.rep M))
+        (x • leftDualLeftUnitVal)
     simp only [map_smul]
     apply congrArg
     simp only [leftDualLeftUnitVal]
@@ -71,17 +73,18 @@ def dualLeftLeftUnitVal : (DualLeftHandedWeyl ⊗[ℂ] LeftHandedWeyl) :=
 
 /-- Expansion of `dualLeftLeftUnitVal` into the basis. -/
 lemma dualLeftLeftUnitVal_expand_tmul : dualLeftLeftUnitVal =
-    dualLeftBasis 0 ⊗ₜ[ℂ] leftBasis 0 + dualLeftBasis 1 ⊗ₜ[ℂ] leftBasis 1 := by
+    DualLeftHandedWeyl.basis 0 ⊗ₜ[ℂ] LeftHandedWeyl.basis 0 +
+      DualLeftHandedWeyl.basis 1 ⊗ₜ[ℂ] LeftHandedWeyl.basis 1 := by
   simp only [dualLeftLeftUnitVal, Fin.isValue]
   rw [dualLeftLeftToMatrix_symm_expand_tmul]
   simp only [Fin.sum_univ_two, Fin.isValue, one_apply_eq, one_smul, ne_eq, zero_ne_one,
     not_false_eq_true, one_apply_ne, zero_smul, add_zero, one_ne_zero, zero_add]
 
-/-- The dual-left-left unit `δₐᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ dualLeftHanded ⊗ leftHanded `,
-  manifesting the invariance under the `SL(2,ℂ)` action. -/
+/-- The dual-left-left unit `δₐᵃ` as a morphism `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶
+  dualLeftHanded ⊗ leftHanded `, manifesting the invariance under the `SL(2,ℂ)` action. -/
 def dualLeftLeftUnit :
     (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
-      (dualLeftHandedRep.tprod leftHandedRep) where
+      (DualLeftHandedWeyl.rep.tprod LeftHandedWeyl.rep) where
   toFun := fun a =>
       let a' : ℂ := a
       a' • dualLeftLeftUnitVal
@@ -93,7 +96,8 @@ def dualLeftLeftUnit :
   isIntertwining' M := by
     refine LinearMap.ext fun x : ℂ => ?_
     change x • dualLeftLeftUnitVal =
-      (TensorProduct.map (dualLeftHandedRep M) (leftHandedRep M)) (x • dualLeftLeftUnitVal)
+      (TensorProduct.map (DualLeftHandedWeyl.rep M) (LeftHandedWeyl.rep M))
+        (x • dualLeftLeftUnitVal)
     simp only [map_smul]
     apply congrArg
     simp only [dualLeftLeftUnitVal]
@@ -114,7 +118,8 @@ def rightDualRightUnitVal : RightHandedWeyl ⊗[ℂ] DualRightHandedWeyl :=
 
 /-- Expansion of `rightDualRightUnitVal` into the basis. -/
 lemma rightDualRightUnitVal_expand_tmul : rightDualRightUnitVal =
-    rightBasis 0 ⊗ₜ[ℂ] dualRightBasis 0 + rightBasis 1 ⊗ₜ[ℂ] dualRightBasis 1 := by
+    RightHandedWeyl.basis 0 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 0 +
+      RightHandedWeyl.basis 1 ⊗ₜ[ℂ] DualRightHandedWeyl.basis 1 := by
   simp only [rightDualRightUnitVal, Fin.isValue]
   rw [rightDualRightToMatrix_symm_expand_tmul]
   simp only [Fin.sum_univ_two, Fin.isValue, one_apply_eq, one_smul, ne_eq, zero_ne_one,
@@ -124,7 +129,7 @@ lemma rightDualRightUnitVal_expand_tmul : rightDualRightUnitVal =
   `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ rightHanded ⊗ dualRightHanded`, manifesting
   the invariance under the `SL(2,ℂ)` action. -/
 def rightDualRightUnit : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
-    (rightHandedRep.tprod dualRightHandedRep) where
+    (RightHandedWeyl.rep.tprod DualRightHandedWeyl.rep) where
   toFun := fun a =>
     let a' : ℂ := a
     a' • rightDualRightUnitVal
@@ -136,7 +141,8 @@ def rightDualRightUnit : (Representation.trivial ℂ SL(2,ℂ) ℂ).Intertwining
   isIntertwining' M := by
     refine LinearMap.ext fun x : ℂ => ?_
     change x • rightDualRightUnitVal =
-      (TensorProduct.map (rightHandedRep M) (dualRightHandedRep M)) (x • rightDualRightUnitVal)
+      (TensorProduct.map (RightHandedWeyl.rep M) (DualRightHandedWeyl.rep M))
+        (x • rightDualRightUnitVal)
     simp only [map_smul]
     apply congrArg
     simp only [rightDualRightUnitVal]
@@ -161,7 +167,8 @@ def dualRightRightUnitVal : (DualRightHandedWeyl ⊗[ℂ] RightHandedWeyl) :=
 
 /-- Expansion of `dualRightRightUnitVal` into the basis. -/
 lemma dualRightRightUnitVal_expand_tmul : dualRightRightUnitVal =
-    dualRightBasis 0 ⊗ₜ[ℂ] rightBasis 0 + dualRightBasis 1 ⊗ₜ[ℂ] rightBasis 1 := by
+    DualRightHandedWeyl.basis 0 ⊗ₜ[ℂ] RightHandedWeyl.basis 0 +
+      DualRightHandedWeyl.basis 1 ⊗ₜ[ℂ] RightHandedWeyl.basis 1 := by
   simp only [dualRightRightUnitVal, Fin.isValue]
   rw [dualRightRightToMatrix_symm_expand_tmul]
   simp only [Fin.sum_univ_two, Fin.isValue, one_apply_eq, one_smul, ne_eq, zero_ne_one,
@@ -171,7 +178,7 @@ lemma dualRightRightUnitVal_expand_tmul : dualRightRightUnitVal =
   `𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ dualRightHanded ⊗ rightHanded`, manifesting
   the invariance under the `SL(2,ℂ)` action. -/
 def dualRightRightUnit : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap
-    (dualRightHandedRep.tprod rightHandedRep) where
+    (DualRightHandedWeyl.rep.tprod RightHandedWeyl.rep) where
   toFun := fun a =>
     let a' : ℂ := a
     a' • dualRightRightUnitVal
@@ -183,7 +190,8 @@ def dualRightRightUnit : (Representation.trivial ℂ SL(2,ℂ) ℂ).Intertwining
   isIntertwining' M := by
     refine LinearMap.ext fun x : ℂ => ?_
     change x • dualRightRightUnitVal =
-      (TensorProduct.map (dualRightHandedRep M) (rightHandedRep M)) (x • dualRightRightUnitVal)
+      (TensorProduct.map (DualRightHandedWeyl.rep M) (RightHandedWeyl.rep M))
+        (x • dualRightRightUnitVal)
     simp only [map_smul]
     apply congrArg
     simp only [dualRightRightUnitVal]
@@ -211,7 +219,8 @@ lemma contr_dualLeftLeftUnit (x : LeftHandedWeyl) :
     leftDualContraction.toLinearMap.rTensor _ <|
     (TensorProduct.assoc ℂ _ _ _).symm <|
     x ⊗ₜ[ℂ] (dualLeftLeftUnit (1 : ℂ))) = x := by
-  obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span leftBasis x)
+  obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun ℂ).mp
+    (Basis.mem_span LeftHandedWeyl.basis x)
   subst hc
   simp [- Fintype.sum_sum_type, smul_tmul, leftDualContraction_basis,
     dualLeftLeftUnit_apply_one, dualLeftLeftUnitVal_expand_tmul, add_tmul, tmul_add]
@@ -222,7 +231,8 @@ lemma contr_leftDualLeftUnit (x : DualLeftHandedWeyl) :
     dualLeftContraction.toLinearMap.rTensor _ <|
     (TensorProduct.assoc ℂ _ _ _).symm <|
     x ⊗ₜ[ℂ] (leftDualLeftUnit (1 : ℂ))) = x := by
-  obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span dualLeftBasis x)
+  obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun ℂ).mp
+    (Basis.mem_span DualLeftHandedWeyl.basis x)
   subst hc
   simp [- Fintype.sum_sum_type, smul_tmul, dualLeftContraction_basis,
     leftDualLeftUnit_apply_one, leftDualLeftUnitVal_expand_tmul, add_tmul, tmul_add]
@@ -233,7 +243,8 @@ lemma contr_dualRightRightUnit (x : RightHandedWeyl) :
     rightDualContraction.toLinearMap.rTensor _ <|
     (TensorProduct.assoc ℂ _ _ _).symm <|
     x ⊗ₜ[ℂ] (dualRightRightUnit (1 : ℂ))) = x := by
-  obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span rightBasis x)
+  obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun ℂ).mp
+    (Basis.mem_span RightHandedWeyl.basis x)
   subst hc
   simp [- Fintype.sum_sum_type, smul_tmul, rightDualContraction_basis,
     dualRightRightUnit_apply_one, dualRightRightUnitVal_expand_tmul, add_tmul, tmul_add]
@@ -244,7 +255,8 @@ lemma contr_rightDualRightUnit (x : DualRightHandedWeyl) :
     dualRightContraction.toLinearMap.rTensor _ <|
     (TensorProduct.assoc ℂ _ _ _).symm <|
     x ⊗ₜ[ℂ] (rightDualRightUnit (1 : ℂ))) = x := by
-  obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span dualRightBasis x)
+  obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun ℂ).mp
+    (Basis.mem_span DualRightHandedWeyl.basis x)
   subst hc
   simp [- Fintype.sum_sum_type, smul_tmul, dualRightContraction_basis,
     rightDualRightUnit_apply_one, rightDualRightUnitVal_expand_tmul, add_tmul, tmul_add]
diff --git a/Physlib/Relativity/Tensors/RealTensor/ToComplex.lean b/Physlib/Relativity/Tensors/RealTensor/ToComplex.lean
index 8ce430965..006ff600f 100644
--- a/Physlib/Relativity/Tensors/RealTensor/ToComplex.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/ToComplex.lean
@@ -393,10 +393,10 @@ lemma toComplexPure_component {c : Fin n → Color} (p : Pure realLorentzTensor
   let b (c : Color) : Basis (Fin (complexLorentzTensor.repDim (colorToComplex c))) ℂ
       (complexLorentzTensor.modules (colorToComplex c)) :=
     match colorToComplex c with
-    | Color.upL => Fermion.leftBasis
-    | Color.downL => Fermion.dualLeftBasis
-    | Color.upR => Fermion.rightBasis
-    | Color.downR => Fermion.dualRightBasis
+    | Color.upL => Fermion.LeftHandedWeyl.basis
+    | Color.downL => Fermion.DualLeftHandedWeyl.basis
+    | Color.upR => Fermion.RightHandedWeyl.basis
+    | Color.downR => Fermion.DualRightHandedWeyl.basis
     | complexLorentzTensor.Color.up => Lorentz.complexContrBasisFin4
     | complexLorentzTensor.Color.down => Lorentz.complexCoBasisFin4
   let b' (c : Color) : Basis (Fin 1 ⊕ Fin 3) ℝ (realLorentzTensor.modules 3 c) :=
@@ -450,10 +450,10 @@ lemma actionP_toComplexPure {n : ℕ} (c : Fin n → Color) (p : Pure realLorent
   simp [Pure.actionP_eq, toComplexPure]
   let b (c : Color) : Representation ℂ _ (complexLorentzTensor.modules (colorToComplex c)) :=
     match colorToComplex c with
-    | Color.upL => Fermion.leftHandedRep
-    | Color.downL => Fermion.dualLeftHandedRep
-    | Color.upR => Fermion.rightHandedRep
-    | Color.downR => Fermion.dualRightHandedRep
+    | Color.upL => Fermion.LeftHandedWeyl.rep
+    | Color.downL => Fermion.DualLeftHandedWeyl.rep
+    | Color.upR => Fermion.RightHandedWeyl.rep
+    | Color.downR => Fermion.DualRightHandedWeyl.rep
     | complexLorentzTensor.Color.up => Lorentz.ContrℂModule.SL2CRep
     | complexLorentzTensor.Color.down => Lorentz.CoℂModule.SL2CRep
   let b' (c : Color) : Representation ℝ _ (realLorentzTensor.modules 3 c) :=