Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Relativity.PauliMatrices.ToTensor public import Physlib.Relativity.Tensors.ComplexTensor.Units.Basic

Contraction of indices of Pauli matrix.

The main result of this file is pauliMatrix_contract_pauliMatrix which states that η_{μν} σ^{μ α dot β} σ^{ν α' dot β'} = 2 ε^{αα'} ε^{dot β dot β'}.

The current way this result is proved is by using tensor tree manipulations. There is likely a more direct path to this result.

@[expose] public section

The statement that σᵥᵃᵇ σᵛᵃ'ᵇ' = 2 εᵃᵃ' εᵇᵇ'.

b:ComponentIdx (Fin.append ![Color.down, Color.upL, Color.upR] ![Color.up, Color.upL, Color.upR] Fin.succSuccAbove 0 3)Physlib.RatComplexNum.toComplexNum (∑ x, ((if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 (ComponentIdx.prod x).1 1 = (ComponentIdx.prod x).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 (ComponentIdx.prod x).1 1 (ComponentIdx.prod x).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod x).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod x).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod x).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod x).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod x).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod x).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod x).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod x).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod x).2 1 = (ComponentIdx.prod x).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod x).2 1 (ComponentIdx.prod x).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod x).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod x).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod x).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod x).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod x).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod x).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod x).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod x).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) * if (x 0) = ((basisIdxCongr ) (x 3)) then 1 else 0) = Physlib.RatComplexNum.toComplexNum (2 * ((if (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).1 0 = Fin.cast leftMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).1 1 = Fin.cast leftMetric_eq_ofRat._proof_2 1 then -1 else if (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).1 1 = Fin.cast leftMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).1 0 = Fin.cast leftMetric_eq_ofRat._proof_1 1 then 1 else 0) * if (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).2 0 = Fin.cast rightMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).2 1 = Fin.cast rightMetric_eq_ofRat._proof_2 1 then -1 else if (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).2 1 = Fin.cast rightMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).2 0 = Fin.cast rightMetric_eq_ofRat._proof_1 1 then 1 else 0)) b:ComponentIdx (Fin.append ![Color.down, Color.upL, Color.upR] ![Color.up, Color.upL, Color.upR] Fin.succSuccAbove 0 3)(∑ x, ((if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 (ComponentIdx.prod x).1 1 = (ComponentIdx.prod x).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 (ComponentIdx.prod x).1 1 (ComponentIdx.prod x).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod x).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod x).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod x).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod x).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod x).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod x).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod x).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod x).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod x).2 1 = (ComponentIdx.prod x).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod x).2 1 (ComponentIdx.prod x).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod x).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod x).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod x).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod x).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod x).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod x).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod x).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod x).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) * if (x 0) = ((basisIdxCongr ) (x 3)) then 1 else 0) = 2 * ((if (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).1 0 = Fin.cast leftMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).1 1 = Fin.cast leftMetric_eq_ofRat._proof_2 1 then -1 else if (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).1 1 = Fin.cast leftMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).1 0 = Fin.cast leftMetric_eq_ofRat._proof_1 1 then 1 else 0) * if (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).2 0 = Fin.cast rightMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).2 1 = Fin.cast rightMetric_eq_ofRat._proof_2 1 then -1 else if (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).2 1 = Fin.cast rightMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).2 0 = Fin.cast rightMetric_eq_ofRat._proof_1 1 then 1 else 0) (b : ComponentIdx (Fin.append ![Color.down, Color.upL, Color.upR] ![Color.up, Color.upL, Color.upR] Fin.succSuccAbove 0 3)), (∑ x, ((if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 (ComponentIdx.prod x).1 1 = (ComponentIdx.prod x).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 (ComponentIdx.prod x).1 1 (ComponentIdx.prod x).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod x).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod x).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod x).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod x).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod x).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod x).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod x).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod x).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod x).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod x).2 1 = (ComponentIdx.prod x).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod x).2 1 (ComponentIdx.prod x).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod x).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod x).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod x).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod x).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod x).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod x).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod x).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod x).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod x).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) * if (x 0) = ((basisIdxCongr ) (x 3)) then 1 else 0) = 2 * ((if (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).1 0 = Fin.cast leftMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).1 1 = Fin.cast leftMetric_eq_ofRat._proof_2 1 then -1 else if (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).1 1 = Fin.cast leftMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).1 0 = Fin.cast leftMetric_eq_ofRat._proof_1 1 then 1 else 0) * if (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).2 0 = Fin.cast rightMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).2 1 = Fin.cast rightMetric_eq_ofRat._proof_2 1 then -1 else if (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).2 1 = Fin.cast rightMetric_eq_ofRat._proof_2 0 (ComponentIdx.prod fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 2, 1, 3] i))).2 0 = Fin.cast rightMetric_eq_ofRat._proof_1 1 then 1 else 0) All goals completed! 🐙
lemma pauliCoDown_trace_pauliCo : {(σ___ | μ β α σ_^^ | ν α β) = (2 •ₜ η' | μ ν)}ᵀ := (contrT 2 1 3 ) ((contrT 4 2 4 ) ((prodT σ___) σ_^^)) = (permT ![0, 1] ) (2 η') conv_lhs => | ofRat fun b => x, x_1, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 } conv_rhs => | (permT ![0, 1] ) (2 ofRat fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0) | (permT ![0, 1] ) (ofRat (2 fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0)) (Tensor.basis ((Fin.append ![Color.down, Color.downR, Color.downL] ![Color.down, Color.upL, Color.upR] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)).repr (ofRat fun b => x, x_1, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) = (Tensor.basis ((Fin.append ![Color.down, Color.downR, Color.downL] ![Color.down, Color.upL, Color.upR] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)).repr ((permT ![0, 1] ) (ofRat (2 fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0))) b:ComponentIdx ((Fin.append ![Color.down, Color.downR, Color.downL] ![Color.down, Color.upL, Color.upR] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)((Tensor.basis ((Fin.append ![Color.down, Color.downR, Color.downL] ![Color.down, Color.upL, Color.upR] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)).repr (ofRat fun b => x, x_1, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 })) b = ((Tensor.basis ((Fin.append ![Color.down, Color.downR, Color.downL] ![Color.down, Color.upL, Color.upR] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)).repr ((permT ![0, 1] ) (ofRat (2 fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0)))) b conv_rhs => b:ComponentIdx ((Fin.append ![Color.down, Color.downR, Color.downL] ![Color.down, Color.upL, Color.upR] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)| ((Tensor.basis ![Color.down, Color.down]).repr (ofRat (2 fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0))) fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 1] i)) b:ComponentIdx ((Fin.append ![Color.down, Color.downR, Color.downL] ![Color.down, Color.upL, Color.upR] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)Physlib.RatComplexNum.toComplexNum (∑ x, x_1, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) = Physlib.RatComplexNum.toComplexNum ((2 fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0) fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 1] i))) b:ComponentIdx ((Fin.append ![Color.down, Color.downR, Color.downL] ![Color.down, Color.upL, Color.upR] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)(∑ x, x_1, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) = (2 fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0) fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 1] i)) (b : ComponentIdx ((Fin.append ![Color.down, Color.downR, Color.downL] ![Color.down, Color.upL, Color.upR] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)), (∑ x, x_1, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) = (2 fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0) fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 1] i)) All goals completed! 🐙lemma pauliCo_trace_pauliCoDown: {σ_^^ | μ α β σ___ | ν β α = 2 •ₜ η' | μ ν}ᵀ := (contrT 2 1 3 ) ((contrT 4 2 4 ) ((prodT σ_^^) σ___)) = (permT ![0, 1] ) (2 η') conv_lhs => | (contrT 2 1 3 ) ((contrT 4 2 4 ) ((prodT (ofRat fun b => if b 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 b 1 b 2 then { fst := -1, snd := 0 } else if b 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 b 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 b 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if b 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 b 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 b 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if b 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 b 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 b 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if b 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 b 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 b 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 })) (ofRat fun b => if b 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 0 b 1 = b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 1 b 1 b 2 then { fst := 1, snd := 0 } else if b 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 b 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 b 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if b 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 b 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 b 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if b 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 b 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 b 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else if b 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 b 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 b 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }))) | ofRat fun b => x, x_1, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 } conv_rhs => | (permT ![0, 1] ) (2 ofRat fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0) | (permT ![0, 1] ) (ofRat (2 fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0)) (Tensor.basis ((Fin.append ![Color.down, Color.upL, Color.upR] ![Color.down, Color.downR, Color.downL] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)).repr (ofRat fun b => x, x_1, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) = (Tensor.basis ((Fin.append ![Color.down, Color.upL, Color.upR] ![Color.down, Color.downR, Color.downL] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)).repr ((permT ![0, 1] ) (ofRat (2 fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0))) b:ComponentIdx ((Fin.append ![Color.down, Color.upL, Color.upR] ![Color.down, Color.downR, Color.downL] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)((Tensor.basis ((Fin.append ![Color.down, Color.upL, Color.upR] ![Color.down, Color.downR, Color.downL] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)).repr (ofRat fun b => x, x_1, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 })) b = ((Tensor.basis ((Fin.append ![Color.down, Color.upL, Color.upR] ![Color.down, Color.downR, Color.downL] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)).repr ((permT ![0, 1] ) (ofRat (2 fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0)))) b conv_rhs => b:ComponentIdx ((Fin.append ![Color.down, Color.upL, Color.upR] ![Color.down, Color.downR, Color.downL] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)| ((Tensor.basis ![Color.down, Color.down]).repr (ofRat (2 fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0))) fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 1] i)) b:ComponentIdx ((Fin.append ![Color.down, Color.upL, Color.upR] ![Color.down, Color.downR, Color.downL] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)Physlib.RatComplexNum.toComplexNum (∑ x, x_1, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) = Physlib.RatComplexNum.toComplexNum ((2 fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0) fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 1] i))) b:ComponentIdx ((Fin.append ![Color.down, Color.upL, Color.upR] ![Color.down, Color.downR, Color.downL] Fin.succSuccAbove 2 4) Fin.succSuccAbove 1 3)(∑ x, x_1, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 0 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 0 = Fin.cast pauliCo_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 1 = Fin.cast pauliCo_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).1 2 = Fin.cast pauliCo_eq_ofRat._proof_3 1 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 0 = Fin.cast pauliCoDown_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 1 = Fin.cast pauliCoDown_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))) (x_1, Fin.cast x_1))).2 2 = Fin.cast pauliCoDown_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else { fst := 0, snd := 0 }) = (2 fun f => if f 0 = Fin.cast coMetric_eq_ofRat._proof_1 0 f 1 = Fin.cast coMetric_eq_ofRat._proof_2 0 then 1 else if f 0 = f 1 then -1 else 0) fun i => (basisIdxCongr ) (b (IsReindexing.inv ![0, 1] i)) All goals completed! 🐙lemma pauliContr_mul_pauliContrDown_add : {((σ^^^ | μ α β σ^__ | ν β α') + (σ^^^ | ν α β σ^__ | μ β α')) = 2 •ₜ η | μ ν δL | α α'}ᵀ := (contrT 4 2 4 ) ((prodT (Tensorial.toTensor σ)) σ^__) + (permT ![2, 1, 0, 3] ) ((contrT 4 2 4 ) ((prodT (Tensorial.toTensor σ)) σ^__)) = (permT ![0, 2, 1, 3] ) (2 (prodT η) δL) conv_lhs => | ofRat ((fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) + fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) conv_rhs => | ofRat fun b => (2 fun b => (if (ComponentIdx.prod b).1 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod b).1 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if (ComponentIdx.prod b).1 0 = (ComponentIdx.prod b).1 1 then -1 else 0) * if (ComponentIdx.prod b).2 0 = (ComponentIdx.prod b).2 1 then 1 else 0) fun i => Fin.cast (b (IsReindexing.inv ![0, 2, 1, 3] i)) (Tensor.basis (Fin.append ![Color.up, Color.upL, Color.upR] ![Color.up, Color.downR, Color.downL] Fin.succSuccAbove 2 4)).repr (ofRat ((fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) + fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0)) = (Tensor.basis (Fin.append ![Color.up, Color.upL, Color.upR] ![Color.up, Color.downR, Color.downL] Fin.succSuccAbove 2 4)).repr (ofRat fun b => (2 fun b => (if (ComponentIdx.prod b).1 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod b).1 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if (ComponentIdx.prod b).1 0 = (ComponentIdx.prod b).1 1 then -1 else 0) * if (ComponentIdx.prod b).2 0 = (ComponentIdx.prod b).2 1 then 1 else 0) fun i => Fin.cast (b (IsReindexing.inv ![0, 2, 1, 3] i))) b:ComponentIdx (Fin.append ![Color.up, Color.upL, Color.upR] ![Color.up, Color.downR, Color.downL] Fin.succSuccAbove 2 4)((Tensor.basis (Fin.append ![Color.up, Color.upL, Color.upR] ![Color.up, Color.downR, Color.downL] Fin.succSuccAbove 2 4)).repr (ofRat ((fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) + fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0))) b = ((Tensor.basis (Fin.append ![Color.up, Color.upL, Color.upR] ![Color.up, Color.downR, Color.downL] Fin.succSuccAbove 2 4)).repr (ofRat fun b => (2 fun b => (if (ComponentIdx.prod b).1 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod b).1 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if (ComponentIdx.prod b).1 0 = (ComponentIdx.prod b).1 1 then -1 else 0) * if (ComponentIdx.prod b).2 0 = (ComponentIdx.prod b).2 1 then 1 else 0) fun i => Fin.cast (b (IsReindexing.inv ![0, 2, 1, 3] i)))) b b:ComponentIdx (Fin.append ![Color.up, Color.upL, Color.upR] ![Color.up, Color.downR, Color.downL] Fin.succSuccAbove 2 4)Physlib.RatComplexNum.toComplexNum (((fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) + fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) b) = Physlib.RatComplexNum.toComplexNum ((2 fun b => (if (ComponentIdx.prod b).1 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod b).1 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if (ComponentIdx.prod b).1 0 = (ComponentIdx.prod b).1 1 then -1 else 0) * if (ComponentIdx.prod b).2 0 = (ComponentIdx.prod b).2 1 then 1 else 0) fun i => Fin.cast (b (IsReindexing.inv ![0, 2, 1, 3] i))) b:ComponentIdx (Fin.append ![Color.up, Color.upL, Color.upR] ![Color.up, Color.downR, Color.downL] Fin.succSuccAbove 2 4)((fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) + fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) b = (2 fun b => (if (ComponentIdx.prod b).1 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod b).1 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if (ComponentIdx.prod b).1 0 = (ComponentIdx.prod b).1 1 then -1 else 0) * if (ComponentIdx.prod b).2 0 = (ComponentIdx.prod b).2 1 then 1 else 0) fun i => Fin.cast (b (IsReindexing.inv ![0, 2, 1, 3] i)) All goals completed! 🐙lemma auliContrDown_pauliContr_mul_add : {((σ^__ | μ β α σ^^^ | ν α β') + (σ^__ | ν β α σ^^^ | μ α β')) = 2 •ₜ η | μ ν δR' | β β'}ᵀ := (contrT 4 2 4 ) ((prodT σ^__) (Tensorial.toTensor σ)) + (permT ![2, 1, 0, 3] ) ((contrT 4 2 4 ) ((prodT σ^__) (Tensorial.toTensor σ))) = (permT ![0, 2, 1, 3] ) (2 (prodT η) δR') conv_lhs => | ofRat ((fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) + fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) conv_rhs => | ofRat fun b => (2 fun b => (if (ComponentIdx.prod b).1 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod b).1 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if (ComponentIdx.prod b).1 0 = (ComponentIdx.prod b).1 1 then -1 else 0) * if (ComponentIdx.prod b).2 0 = (ComponentIdx.prod b).2 1 then 1 else 0) fun i => Fin.cast (b (IsReindexing.inv ![0, 2, 1, 3] i)) (Tensor.basis (Fin.append ![Color.up, Color.downR, Color.downL] ![Color.up, Color.upL, Color.upR] Fin.succSuccAbove 2 4)).repr (ofRat ((fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) + fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0)) = (Tensor.basis (Fin.append ![Color.up, Color.downR, Color.downL] ![Color.up, Color.upL, Color.upR] Fin.succSuccAbove 2 4)).repr (ofRat fun b => (2 fun b => (if (ComponentIdx.prod b).1 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod b).1 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if (ComponentIdx.prod b).1 0 = (ComponentIdx.prod b).1 1 then -1 else 0) * if (ComponentIdx.prod b).2 0 = (ComponentIdx.prod b).2 1 then 1 else 0) fun i => Fin.cast (b (IsReindexing.inv ![0, 2, 1, 3] i))) b:ComponentIdx (Fin.append ![Color.up, Color.downR, Color.downL] ![Color.up, Color.upL, Color.upR] Fin.succSuccAbove 2 4)((Tensor.basis (Fin.append ![Color.up, Color.downR, Color.downL] ![Color.up, Color.upL, Color.upR] Fin.succSuccAbove 2 4)).repr (ofRat ((fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) + fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0))) b = ((Tensor.basis (Fin.append ![Color.up, Color.downR, Color.downL] ![Color.up, Color.upL, Color.upR] Fin.succSuccAbove 2 4)).repr (ofRat fun b => (2 fun b => (if (ComponentIdx.prod b).1 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod b).1 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if (ComponentIdx.prod b).1 0 = (ComponentIdx.prod b).1 1 then -1 else 0) * if (ComponentIdx.prod b).2 0 = (ComponentIdx.prod b).2 1 then 1 else 0) fun i => Fin.cast (b (IsReindexing.inv ![0, 2, 1, 3] i)))) b b:ComponentIdx (Fin.append ![Color.up, Color.downR, Color.downL] ![Color.up, Color.upL, Color.upR] Fin.succSuccAbove 2 4)Physlib.RatComplexNum.toComplexNum (((fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) + fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) b) = Physlib.RatComplexNum.toComplexNum ((2 fun b => (if (ComponentIdx.prod b).1 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod b).1 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if (ComponentIdx.prod b).1 0 = (ComponentIdx.prod b).1 1 then -1 else 0) * if (ComponentIdx.prod b).2 0 = (ComponentIdx.prod b).2 1 then 1 else 0) fun i => Fin.cast (b (IsReindexing.inv ![0, 2, 1, 3] i))) b:ComponentIdx (Fin.append ![Color.up, Color.downR, Color.downL] ![Color.up, Color.upL, Color.upR] Fin.succSuccAbove 2 4)((fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv b) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) + fun b => x, (if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 then { fst := -1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 1 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 0 = Fin.cast pauliContrDown_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 1 = Fin.cast pauliContrDown_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).1 2 = Fin.cast pauliContrDown_ofRat._proof_3 0 then { fst := -1, snd := 0 } else 0) * if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := 0, snd := -1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 2 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 0, snd := 1 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 0 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 0 then { fst := 1, snd := 0 } else if (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 0 = Fin.cast toTensor_eq_ofRat._proof_1 3 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 1 = Fin.cast toTensor_eq_ofRat._proof_2 1 (ComponentIdx.prod ((ComponentIdx.DropPairSection.ofFinEquiv fun i => Fin.cast (b (IsReindexing.inv ![2, 1, 0, 3] i))) (x, Fin.cast x))).2 2 = Fin.cast toTensor_eq_ofRat._proof_3 1 then { fst := -1, snd := 0 } else 0) b = (2 fun b => (if (ComponentIdx.prod b).1 0 = Fin.cast contrMetric_eq_ofRat._proof_1 0 (ComponentIdx.prod b).1 1 = Fin.cast contrMetric_eq_ofRat._proof_2 0 then 1 else if (ComponentIdx.prod b).1 0 = (ComponentIdx.prod b).1 1 then -1 else 0) * if (ComponentIdx.prod b).2 0 = (ComponentIdx.prod b).2 1 then 1 else 0) fun i => Fin.cast (b (IsReindexing.inv ![0, 2, 1, 3] i)) All goals completed! 🐙