refactor: Weyl fermions

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

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]

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
 

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]

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 =>

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,43 +228,43 @@ 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) ⊗ₜ[ℂ]
       (complexLorentzTensor.basis .upL _))
     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) ⊗ₜ[ℂ]
       (complexLorentzTensor.basis .downL _))
     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) ⊗ₜ[ℂ]
       (complexLorentzTensor.basis .upR _))
     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]