Help improving Pauli matrix relations

Stream: PhysLean

[Joseph Tooby-Smith]

So I've recently set up an online version of PhysLean: live.physlean.com.

Which allows me to ask questions like this:

In PhysLean I want to prove some relations between the Pauli matrices.
The code I currently have is the below, which can be opened here:

view on web

import PhysLean.Relativity.Lorentz.PauliMatrices.Basis

open IndexNotation
open CategoryTheory
open MonoidalCategory
open Matrix
open TensorProduct
open CategoryTheory
open TensorTree

namespace PauliMatrix
open Fermion
open complexLorentzTensor


/-- The statement that ` σᵥᵃᵇ σᵛᵃ'ᵇ' = 2 εᵃᵃ' εᵇᵇ'`. -/
lemma pauliCo_contr_pauliContr : {σ_^^ | ν α β ⊗ σ^^^ | ν α' β' = 2 •ₜ εL | α α' ⊗ εR | β β'}ᵀ := by
  apply (complexLorentzTensor.tensorBasis _).repr.injective
  ext b
  conv_rhs =>
    rw [TensorTree.perm_tensorBasis_repr_apply]
    rw [TensorTree.smul_tensorBasis_repr]
    simp only [Nat.reduceAdd, Nat.succ_eq_add_one, Fin.isValue, Fin.succAbove_zero,
      Function.comp_apply, OverColor.mk_hom, OverColor.equivToHomEq_toEquiv, Finsupp.coe_smul,
      Pi.smul_apply, smul_eq_mul]
    rw (transparency := .instances) [TensorTree.prod_tensorBasis_repr_apply]
    simp only [Nat.reduceAdd, Nat.succ_eq_add_one, Fin.isValue, Fin.succAbove_zero,
      Function.comp_apply, tensorNode_tensor]
    rw [leftMetric_eq_ofRat, rightMetric_eq_ofRat]
    simp only [Nat.reduceAdd, Nat.succ_eq_add_one, Fin.isValue, Fin.succAbove_zero,
      Function.comp_apply, cons_val_zero, cons_val_one, head_cons, ofRat_tensorBasis_repr_apply]
    rw [← PhysLean.RatComplexNum.toComplexNum.map_mul]
    erw [PhysLean.RatComplexNum.ofNat_mul_toComplexNum 2]
  rw [TensorTree.contr_tensorBasis_repr_apply]
  conv_lhs =>
    enter [2, x]
    rw [TensorTree.prod_tensorBasis_repr_apply]
    simp only [pauliCo_ofRat, pauliContr_ofRat]
    simp only [Fin.isValue, Function.comp_apply,
      tensorNode_tensor, ofRat_tensorBasis_repr_apply, Monoidal.tensorUnit_obj,
      Action.instMonoidalCategory_tensorUnit_V, Equivalence.symm_inverse,
      Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
      Functor.comp_obj, Discrete.functor_obj_eq_as, Fin.zero_succAbove, Fin.reduceSucc,
      Fin.cast_eq_self, Nat.cast_ofNat, mul_ite, mul_neg, mul_one, mul_zero]
    left
    rw (transparency := .instances) [ofRat_tensorBasis_repr_apply]
    rw [← PhysLean.RatComplexNum.toComplexNum.map_mul]
  conv_lhs =>
    enter [2, x]
    right
    rw (transparency := .instances) [contr_basis_ratComplexNum]
  conv_lhs =>
    enter [2, x]
    rw [← PhysLean.RatComplexNum.toComplexNum.map_mul]
  rw [← map_sum PhysLean.RatComplexNum.toComplexNum]
  apply (Function.Injective.eq_iff PhysLean.RatComplexNum.toComplexNum_injective).mpr
  revert b
  decide +kernel

end PauliMatrix

The last line decide +kernel is very slow. Any suggestions on how to improve this proof is welcome!

(This all comes with the caveat that the server is not the most powerful - and may struggle a bit if multiple users are trying to use it).

[Joseph Tooby-Smith]

(I have managed to speed up the decide +kernel in the above by a factor of around 10 in this PR. It still has some 'sorry's in it which need filling in - but I believe this should be easy)