feat: Improvements to index notation

PhysLean.lean

@@ -67,9 +67,10 @@ import PhysLean.Lorentz.ComplexTensor.Lemmas
 import PhysLean.Lorentz.ComplexTensor.Metrics.Basic
 import PhysLean.Lorentz.ComplexTensor.Metrics.Basis
 import PhysLean.Lorentz.ComplexTensor.Metrics.Lemmas
+import PhysLean.Lorentz.ComplexTensor.OfRat
 import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Basic
 import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Basis
-import PhysLean.Lorentz.ComplexTensor.PauliMatrices.CoContractContr
+import PhysLean.Lorentz.ComplexTensor.PauliMatrices.Relations
 import PhysLean.Lorentz.ComplexTensor.Units.Basic
 import PhysLean.Lorentz.ComplexTensor.Units.Symm
 import PhysLean.Lorentz.ComplexVector.Basic
@@ -107,6 +108,7 @@ import PhysLean.Mathematics.List
 import PhysLean.Mathematics.List.InsertIdx
 import PhysLean.Mathematics.List.InsertionSort
 import PhysLean.Mathematics.PiTensorProduct
+import PhysLean.Mathematics.RatComplexNum
 import PhysLean.Mathematics.SO3.Basic
 import PhysLean.Mathematics.SchurTriangulation
 import PhysLean.Meta.AllFilePaths
@@ -197,6 +199,7 @@ import PhysLean.Tensors.TensorSpecies.Contractions.Categorical
 import PhysLean.Tensors.TensorSpecies.Contractions.ContrMap
 import PhysLean.Tensors.TensorSpecies.DualRepIso
 import PhysLean.Tensors.TensorSpecies.MetricTensor
+import PhysLean.Tensors.TensorSpecies.OfInt
 import PhysLean.Tensors.TensorSpecies.Pure
 import PhysLean.Tensors.TensorSpecies.UnitTensor
 import PhysLean.Tensors.Tree.Basic

PhysLean/FlavorPhysics/CKMMatrix/Basic.lean

@@ -323,7 +323,7 @@ lemma VAbs'_equiv (i j : Fin 3) (V U : CKMMatrix) (h : V ≈ U) :
   fin_cases i <;> fin_cases j <;>
     simp only [Fin.zero_eta, Fin.isValue, cons_val_zero, zero_mul, add_zero, mul_zero,
       _root_.map_mul, mul_re, I_re, ofReal_re, I_im, ofReal_im, sub_self, Real.exp_zero,
-      one_mul, mul_one,  Complex.abs_exp, Fin.mk_one, cons_val_one, head_cons, zero_add,
+      one_mul, mul_one, Complex.abs_exp, Fin.mk_one, cons_val_one, head_cons, zero_add,
       head_fin_const, Fin.reduceFinMk, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons,
       tail_val', head_val']
   all_goals change Complex.abs (0 * _ + _) = _

PhysLean/Lorentz/ComplexTensor/Basic.lean

@@ -277,11 +277,24 @@ instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} :
 instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} :
     Fintype (OverColor.mk c).left := Fin.fintype n
 
+instance : CharZero complexLorentzTensor.k := instCharZero
+
 /-- The equality of two maps in `OverColor C` from objects based on `Fin _` is decidable. -/
 instance {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     {c1 : Fin m → complexLorentzTensor.C} (σ σ' : OverColor.mk c ⟶ OverColor.mk c1) :
     Decidable (σ = σ') :=
   decidable_of_iff _ (OverColor.Hom.ext_iff σ σ')
 
+@[simp]
+lemma k_instSub : @HSub.hSub complexLorentzTensor.k complexLorentzTensor.k complexLorentzTensor.k
+    instHSub = @HSub.hSub ℂ ℂ ℂ instHSub := by rfl
+
+@[simp]
+lemma k_instAdd : @HAdd.hAdd complexLorentzTensor.k
+    complexLorentzTensor.k complexLorentzTensor.k instHAdd = @HAdd.hAdd ℂ ℂ ℂ instHAdd := by rfl
+
+@[simp]
+lemma k_neg : @Neg.neg complexLorentzTensor.k = @Neg.neg ℂ := by rfl
+
 end complexLorentzTensor
 end

PhysLean/Lorentz/ComplexTensor/Basis.lean

@@ -42,6 +42,13 @@ def basisVector {n : ℕ} (c : Fin n → complexLorentzTensor.C)
     complexLorentzTensor.F.obj (OverColor.mk c) :=
   PiTensorProduct.tprod ℂ (fun i => complexLorentzTensor.basis (c i) (b i))
 
+lemma basisVector_eq_tensorBasis {n : ℕ} (c : Fin n → complexLorentzTensor.C)
+    (b : Π j, Fin (complexLorentzTensor.repDim (c j))) :
+    basisVector c b = complexLorentzTensor.tensorBasis c b := by
+  rw [basisVector, TensorSpecies.tensorBasis_eq_basisVector]
+  simp only [OverColor.mk_left, Functor.id_obj, OverColor.mk_hom, TensorSpecies.basisVector]
+  rfl
+
 lemma perm_basisVector_cast {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     {c1 : Fin m → complexLorentzTensor.C}
     (σ : OverColor.mk c ⟶ OverColor.mk c1) (i : Fin m) :

PhysLean/Lorentz/ComplexTensor/Metrics/Basis.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Lorentz.ComplexTensor.Metrics.Basic
+import PhysLean.Lorentz.ComplexTensor.OfRat
 import PhysLean.Lorentz.ComplexTensor.Basis
+import PhysLean.Tensors.TensorSpecies.OfInt
 /-!
 
 ## Metrics and basis expansions
@@ -52,6 +54,30 @@ lemma coMetric_basis_expand : {η' | μ ν}ᵀ.tensor =
       simp only [Fin.isValue, Lorentz.complexCoBasisFin4, Basis.coe_reindex, Function.comp_apply]
       rfl
 
+lemma coMetric_tensorBasis : η' =
+    complexLorentzTensor.tensorBasis ![Color.down, Color.down] (fun _ => 0)
+    - complexLorentzTensor.tensorBasis ![Color.down, Color.down] (fun _ => 1)
+    - complexLorentzTensor.tensorBasis ![Color.down, Color.down] (fun _ => 2)
+    - complexLorentzTensor.tensorBasis ![Color.down, Color.down] (fun _ => 3) := by
+  trans {η' | μ ν}ᵀ.tensor
+  · simp
+  · rw [coMetric_basis_expand]
+    simp [basisVector_eq_tensorBasis]
+
+lemma coMetric_eq_ofRat : η' = ofRat fun f =>
+    if f 0 = 0 ∧ f 1 = 0 then 1 else
+    if f 0 = f 1 then - 1 else 0 := by
+  apply (complexLorentzTensor.tensorBasis _).repr.injective
+  ext b
+  rw [coMetric_tensorBasis]
+  repeat rw [tensorBasis_eq_ofRat]
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, map_sub, Finsupp.coe_sub, Pi.sub_apply,
+    ofRat_tensorBasis_repr_apply, k_instSub, Fin.isValue, cons_val_zero, cons_val_one, head_cons]
+  simp only [← map_sub, Fin.isValue]
+  apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr
+  revert b
+  with_unfolding_all decide
+
 /-- Provides the explicit expansion of the co-metric tensor in terms of the basis elements, as
 a tensor tree. -/
 lemma coMetric_basis_expand_tree : {η' | μ ν}ᵀ.tensor =
@@ -61,8 +87,13 @@ lemma coMetric_basis_expand_tree : {η' | μ ν}ᵀ.tensor =
     (smul (-1) (tensorNode (basisVector ![Color.down, Color.down] (fun _ => 3))))).tensor :=
   coMetric_basis_expand
 
+/-!
+
+## contrMetric
+
+-/
 /-- The expansion of the Lorentz contravariant metric in terms of basis vectors. -/
-lemma contrMatrix_basis_expand : {η | μ ν}ᵀ.tensor =
+lemma contrMetric_basis_expand : {η | μ ν}ᵀ.tensor =
     basisVector ![Color.up, Color.up] (fun _ => 0)
     - basisVector ![Color.up, Color.up] (fun _ => 1)
     - basisVector ![Color.up, Color.up] (fun _ => 2)
@@ -87,14 +118,38 @@ lemma contrMatrix_basis_expand : {η | μ ν}ᵀ.tensor =
       simp only [Fin.isValue, Lorentz.complexContrBasisFin4, Basis.coe_reindex, Function.comp_apply]
       rfl
 
+lemma contrMetric_tensorBasis : η =
+    complexLorentzTensor.tensorBasis ![Color.up, Color.up] (fun _ => 0)
+    - complexLorentzTensor.tensorBasis ![Color.up, Color.up] (fun _ => 1)
+    - complexLorentzTensor.tensorBasis ![Color.up, Color.up] (fun _ => 2)
+    - complexLorentzTensor.tensorBasis ![Color.up, Color.up] (fun _ => 3) := by
+  trans {η | μ ν}ᵀ.tensor
+  · simp
+  · rw [contrMetric_basis_expand]
+    simp [basisVector_eq_tensorBasis]
+
+lemma contrMetric_eq_ofRat : η = ofRat fun f =>
+    if f 0 = 0 ∧ f 1 = 0 then 1 else
+    if f 0 = f 1 then - 1 else 0 := by
+  apply (complexLorentzTensor.tensorBasis _).repr.injective
+  ext b
+  rw [contrMetric_tensorBasis]
+  repeat rw [tensorBasis_eq_ofRat]
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, map_sub, Finsupp.coe_sub, Pi.sub_apply,
+    ofRat_tensorBasis_repr_apply, k_instSub, Fin.isValue, cons_val_zero, cons_val_one, head_cons]
+  simp only [← map_sub, Fin.isValue]
+  apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr
+  revert b
+  with_unfolding_all decide
+
 /-- The expansion of the Lorentz contravariant metric in terms of basis vectors as
   a structured tensor tree. -/
-lemma contrMatrix_basis_expand_tree : {η | μ ν}ᵀ.tensor =
+lemma contrMetric_basis_expand_tree : {η | μ ν}ᵀ.tensor =
     (TensorTree.add (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 0))) <|
     TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 1)))) <|
     TensorTree.add (smul (-1) (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 2)))) <|
     (smul (-1) (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 3))))).tensor :=
-  contrMatrix_basis_expand
+  contrMetric_basis_expand
 
 /-- The expansion of the Fermionic left metric in terms of basis vectors. -/
 lemma leftMetric_expand : {εL | α β}ᵀ.tensor =
@@ -115,6 +170,31 @@ lemma leftMetric_expand : {εL | α β}ᵀ.tensor =
     · rfl
     · rfl
 
+lemma leftMetric_tensorBasis : εL =
+    - complexLorentzTensor.tensorBasis ![Color.upL, Color.upL] (fun | 0 => 0 | 1 => 1)
+    + complexLorentzTensor.tensorBasis ![Color.upL, Color.upL] (fun | 0 => 1 | 1 => 0) := by
+  trans {εL | μ ν}ᵀ.tensor
+  · simp
+  · rw [leftMetric_expand]
+    simp [basisVector_eq_tensorBasis]
+
+lemma leftMetric_eq_ofRat : εL = ofRat fun f =>
+    if f 0 = 0 ∧ f 1 = 1 then - 1 else
+    if f 1 = 0 ∧ f 0 = 1 then 1 else 0 := by
+  apply (complexLorentzTensor.tensorBasis _).repr.injective
+  ext b
+  rw [leftMetric_tensorBasis]
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, map_add, map_neg,
+    Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply, Pi.neg_apply, cons_val_zero, cons_val_one,
+    head_cons]
+  repeat rw [tensorBasis_eq_ofRat]
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, map_sub, Finsupp.coe_sub, Pi.sub_apply,
+    ofRat_tensorBasis_repr_apply, k_instSub, Fin.isValue, cons_val_zero, cons_val_one, head_cons]
+  simp only [Fin.isValue, k_neg, ← map_neg, k_instAdd, ← map_add]
+  apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr
+  revert b
+  with_unfolding_all decide
+
 /-- The expansion of the Fermionic left metric in terms of basis vectors as a structured
   tensor tree. -/
 lemma leftMetric_expand_tree : {εL | α β}ᵀ.tensor =
@@ -141,6 +221,31 @@ lemma altLeftMetric_expand : {εL' | α β}ᵀ.tensor =
     · rfl
     · rfl
 
+lemma altLeftMetric_tensorBasis : εL' =
+    complexLorentzTensor.tensorBasis ![Color.downL, Color.downL] (fun | 0 => 0 | 1 => 1)
+    - complexLorentzTensor.tensorBasis ![Color.downL, Color.downL] (fun | 0 => 1 | 1 => 0) := by
+  trans {εL' | μ ν}ᵀ.tensor
+  · simp
+  · rw [altLeftMetric_expand]
+    simp [basisVector_eq_tensorBasis]
+
+lemma altLeftMetric_eq_ofRat : εL' = ofRat fun f =>
+    if f 0 = 0 ∧ f 1 = 1 then 1 else
+    if f 1 = 0 ∧ f 0 = 1 then - 1 else 0 := by
+  apply (complexLorentzTensor.tensorBasis _).repr.injective
+  ext b
+  rw [altLeftMetric_tensorBasis]
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, map_add, map_neg,
+    Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply, Pi.neg_apply, cons_val_zero, cons_val_one,
+    head_cons]
+  repeat rw [tensorBasis_eq_ofRat]
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, map_sub, Finsupp.coe_sub, Pi.sub_apply,
+    ofRat_tensorBasis_repr_apply, k_instSub, Fin.isValue, cons_val_zero, cons_val_one, head_cons]
+  simp only [Fin.isValue, ← map_sub]
+  apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr
+  revert b
+  with_unfolding_all decide
+
 /-- The expansion of the Fermionic alt-left metric in terms of basis vectors as a
   structured tensor tree. -/
 lemma altLeftMetric_expand_tree : {εL' | α β}ᵀ.tensor =
@@ -169,6 +274,31 @@ lemma rightMetric_expand : {εR | α β}ᵀ.tensor =
     · rfl
     · rfl
 
+lemma rightMetric_tensorBasis : εR =
+    - complexLorentzTensor.tensorBasis ![Color.upR, Color.upR] (fun | 0 => 0 | 1 => 1)
+    + complexLorentzTensor.tensorBasis ![Color.upR, Color.upR] (fun | 0 => 1 | 1 => 0) := by
+  trans {εR | μ ν}ᵀ.tensor
+  · simp
+  · rw [rightMetric_expand]
+    simp [basisVector_eq_tensorBasis]
+
+lemma rightMetric_eq_ofRat : εR = ofRat fun f =>
+    if f 0 = 0 ∧ f 1 = 1 then - 1 else
+    if f 1 = 0 ∧ f 0 = 1 then 1 else 0 := by
+  apply (complexLorentzTensor.tensorBasis _).repr.injective
+  ext b
+  rw [rightMetric_tensorBasis]
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, map_add, map_neg,
+    Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply, Pi.neg_apply, cons_val_zero, cons_val_one,
+    head_cons]
+  repeat rw [tensorBasis_eq_ofRat]
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, map_sub, Finsupp.coe_sub, Pi.sub_apply,
+    ofRat_tensorBasis_repr_apply, k_instSub, Fin.isValue, cons_val_zero, cons_val_one, head_cons]
+  simp only [Fin.isValue, k_neg, ← map_neg, k_instAdd, ← map_add]
+  apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr
+  revert b
+  with_unfolding_all decide
+
 /-- The expansion of the Fermionic right metric in terms of basis vectors as a
   structured tensor tree. -/
 lemma rightMetric_expand_tree : {εR | α β}ᵀ.tensor =
@@ -195,6 +325,31 @@ lemma altRightMetric_expand : {εR' | α β}ᵀ.tensor =
     · rfl
     · rfl
 
+lemma altRightMetric_tensorBasis : εR' =
+    complexLorentzTensor.tensorBasis ![Color.downR, Color.downR] (fun | 0 => 0 | 1 => 1)
+    - complexLorentzTensor.tensorBasis ![Color.downR, Color.downR] (fun | 0 => 1 | 1 => 0) := by
+  trans {εR' | μ ν}ᵀ.tensor
+  · simp
+  · rw [altRightMetric_expand]
+    simp [basisVector_eq_tensorBasis]
+
+lemma altRightMetric_eq_ofRat : εR' = ofRat fun f =>
+    if f 0 = 0 ∧ f 1 = 1 then 1 else
+    if f 1 = 0 ∧ f 0 = 1 then - 1 else 0 := by
+  apply (complexLorentzTensor.tensorBasis _).repr.injective
+  ext b
+  rw [altRightMetric_tensorBasis]
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, map_add, map_neg,
+    Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply, Pi.neg_apply, cons_val_zero, cons_val_one,
+    head_cons]
+  repeat rw [tensorBasis_eq_ofRat]
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, map_sub, Finsupp.coe_sub, Pi.sub_apply,
+    ofRat_tensorBasis_repr_apply, k_instSub, Fin.isValue, cons_val_zero, cons_val_one, head_cons]
+  simp only [Fin.isValue, ← map_sub]
+  apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr
+  revert b
+  with_unfolding_all decide
+
 /-- The expansion of the Fermionic alt-right metric in terms of basis vectors as a
   structured tensor tree. -/
 lemma altRightMetric_expand_tree : {εR' | α β}ᵀ.tensor =

PhysLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean

@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Lorentz.ComplexTensor.Metrics.Basis
 import PhysLean.Lorentz.ComplexTensor.Units.Basic
+import PhysLean.Tensors.TensorSpecies.OfInt
 /-!
 
 ## Basic lemmas regarding metrics
@@ -32,28 +33,78 @@ namespace complexLorentzTensor
 -/
 
 /-- The covariant metric is symmetric `{η' | μ ν = η' | ν μ}ᵀ`. -/
-informal_lemma coMetric_symm where
-  deps := [``coMetric]
+lemma coMetric_symm : {η' | μ ν = η' | ν μ}ᵀ := by
+  apply (complexLorentzTensor.tensorBasis _).repr.injective
+  ext b
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, coMetric_eq_ofRat, Fin.isValue, cons_val_zero,
+    cons_val_one, head_cons, tensorNode_tensor, ofRat_tensorBasis_repr_apply,
+    perm_tensorBasis_repr_apply, OverColor.mk_hom, OverColor.equivToHomEq_toEquiv]
+  apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr
+  revert b
+  decide
 
 /-- The contravariant metric is symmetric `{η | μ ν = η | ν μ}ᵀ`. -/
-informal_lemma contrMetric_symm where
-  deps := [``contrMetric]
+lemma contrMetric_symm : {η | μ ν = η | ν μ}ᵀ := by
+  apply (complexLorentzTensor.tensorBasis _).repr.injective
+  ext b
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, contrMetric_eq_ofRat, Fin.isValue, cons_val_zero,
+    cons_val_one, head_cons, tensorNode_tensor, ofRat_tensorBasis_repr_apply,
+    perm_tensorBasis_repr_apply, OverColor.mk_hom, OverColor.equivToHomEq_toEquiv]
+  apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr
+  revert b
+  decide
 
 /-- The left metric is antisymmetric `{εL | α α' = - εL | α' α}ᵀ`. -/
-informal_lemma leftMetric_antisymm where
-  deps := [``leftMetric]
+lemma leftMetric_antisymm : {εL | α α' = - (εL| α' α)}ᵀ := by
+  apply (complexLorentzTensor.tensorBasis _).repr.injective
+  ext b
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, leftMetric_eq_ofRat, Fin.isValue, cons_val_zero,
+    cons_val_one, head_cons, tensorNode_tensor, ofRat_tensorBasis_repr_apply,
+    perm_tensorBasis_repr_apply, neg_tensorBasis_repr, OverColor.mk_hom,
+    OverColor.equivToHomEq_toEquiv, Finsupp.coe_neg, Pi.neg_apply, k_neg]
+  simp only [Fin.isValue, ← map_neg]
+  apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr
+  revert b
+  decide
 
 /-- The right metric is antisymmetric `{εR | β β' = - εR | β' β}ᵀ`. -/
-informal_lemma rightMetric_antisymm where
-  deps := [``rightMetric]
+lemma rightMetric_antisymm : {εR | β β' = - (εR| β' β)}ᵀ := by
+  apply (complexLorentzTensor.tensorBasis _).repr.injective
+  ext b
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, rightMetric_eq_ofRat, Fin.isValue, cons_val_zero,
+    cons_val_one, head_cons, tensorNode_tensor, ofRat_tensorBasis_repr_apply,
+    perm_tensorBasis_repr_apply, neg_tensorBasis_repr, OverColor.mk_hom,
+    OverColor.equivToHomEq_toEquiv, Finsupp.coe_neg, Pi.neg_apply, k_neg]
+  simp only [Fin.isValue, ← map_neg]
+  apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr
+  revert b
+  decide
 
 /-- The alt-left metric is antisymmetric `{εL' | α α' = - εL' | α' α}ᵀ`. -/
-informal_lemma altLeftMetric_antisymm where
-  deps := [``altLeftMetric]
+lemma altLeftMetric_antisymm : {εL' | α α' = - (εL' | α' α)}ᵀ := by
+  apply (complexLorentzTensor.tensorBasis _).repr.injective
+  ext b
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, altLeftMetric_eq_ofRat, Fin.isValue, cons_val_zero,
+    cons_val_one, head_cons, tensorNode_tensor, ofRat_tensorBasis_repr_apply,
+    perm_tensorBasis_repr_apply, neg_tensorBasis_repr, OverColor.mk_hom,
+    OverColor.equivToHomEq_toEquiv, Finsupp.coe_neg, Pi.neg_apply, k_neg]
+  simp only [Fin.isValue, ← map_neg]
+  apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr
+  revert b
+  decide
 
 /-- The alt-right metric is antisymmetric `{εR' | β β' = - εR' | β' β}ᵀ`. -/
-informal_lemma altRightMetric_antisymm where
-  deps := [``altRightMetric]
+lemma altRightMetric_antisymm : {εR' | α α' = - (εR' | α' α)}ᵀ := by
+  apply (complexLorentzTensor.tensorBasis _).repr.injective
+  ext b
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, altRightMetric_eq_ofRat, Fin.isValue,
+    cons_val_zero, cons_val_one, head_cons, tensorNode_tensor, ofRat_tensorBasis_repr_apply,
+    perm_tensorBasis_repr_apply, neg_tensorBasis_repr, OverColor.mk_hom,
+    OverColor.equivToHomEq_toEquiv, Finsupp.coe_neg, Pi.neg_apply, k_neg]
+  simp only [Fin.isValue, ← map_neg]
+  apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr
+  revert b
+  decide
 
 /-!