1. Physlib
  2. Relativity
  3. Tensors
  4. ComplexTensor
  5. Metrics
  6. Pre
Imports
/- Copyright (c) 2024 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.Tensors.ComplexTensor.Units.Pre

Metric for complex Lorentz vectors

@[expose] public section

The metric ηᵃᵃ as an element of (complexContr ⊗ complexContr).V.

def contrMetricVal : (ContrℂModule ⊗[ℂ] ContrℂModule) := contrContrToMatrix.symm ((@minkowskiMatrix 3).map ofRealHom)

The expansion of contrMetricVal into basis vectors.

set_option backward.isDefEq.respectTransparency false in⊢ ↑1 • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) + (↑0 • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) + ↑0 • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) + ↑0 • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) + (↑0 • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) + (↑(-1) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) + ↑0 • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) + ↑0 • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) + (↑0 • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) + (↑0 • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) + ↑(-1) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) + ↑0 • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2))) + (↑0 • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) + (↑0 • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) + ↑0 • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) + ↑(-1) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)))) = complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) ⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) + (-1 • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) + -1 • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) + -1 • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) = complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) All goals completed! 🐙

The metric ηᵃᵃ as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexContr, making its invariance under the action of SL(2,ℂ).

M:SL(2, ℂ)x:ℂ⊢ contrContrToMatrix.symm (minkowskiMatrix.map ⇑ofRealHom) = contrContrToMatrix.symm (LorentzGroup.toComplex (SL2C.toLorentzGroup M) * minkowskiMatrix.map ⇑ofRealHom * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ) M:SL(2, ℂ)x:ℂ⊢ minkowskiMatrix.map ⇑ofRealHom = LorentzGroup.toComplex (SL2C.toLorentzGroup M) * minkowskiMatrix.map ⇑ofRealHom * (LorentzGroup.toComplex (SL2C.toLorentzGroup M))ᵀ All goals completed! 🐙
lemma contrMetric_apply_one : contrMetric (1 : ℂ) = contrMetricVal := ⊢ contrMetric 1 = contrMetricVal ⊢ 1 • contrMetricVal = contrMetricVal All goals completed! 🐙

The metric ηᵢᵢ as an element of (complexCo ⊗ complexCo).V.

def coMetricVal : (CoℂModule ⊗[ℂ] CoℂModule) := coCoToMatrix.symm ((@minkowskiMatrix 3).map ofRealHom)

The expansion of coMetricVal into basis vectors.

set_option backward.isDefEq.respectTransparency false in⊢ ↑1 • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) + (↑0 • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) + ↑0 • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) + ↑0 • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) + (↑0 • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) + (↑(-1) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) + ↑0 • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) + ↑0 • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) + (↑0 • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) + (↑0 • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) + ↑(-1) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) + ↑0 • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2))) + (↑0 • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) + (↑0 • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) + ↑0 • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) + ↑(-1) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)))) = complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) ⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) + (-1 • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) + -1 • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) + -1 • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) = complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) All goals completed! 🐙

The metric ηᵢᵢ as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexCo, making its invariance under the action of SL(2,ℂ).

M:SL(2, ℂ)x:ℂ⊢ minkowskiMatrix.map ⇑ofRealHom = (LorentzGroup.toComplex (SL2C.toLorentzGroup M)⁻¹)ᵀ * minkowskiMatrix.map ⇑ofRealHom * LorentzGroup.toComplex (SL2C.toLorentzGroup M)⁻¹ All goals completed! 🐙
lemma coMetric_apply_one : coMetric (1 : ℂ) = coMetricVal := ⊢ coMetric 1 = coMetricVal ⊢ 1 • coMetricVal = coMetricVal All goals completed! 🐙

Contraction of metrics

⊢ (TensorProduct.comm ℂ ContrℂModule CoℂModule) ((LinearEquiv.lTensor ContrℂModule (TensorProduct.lid ℂ CoℂModule)) ((LinearMap.lTensor ContrℂModule (LinearMap.rTensor CoℂModule contrCoContraction.toLinearMap)) ((LinearMap.lTensor ContrℂModule ↑(TensorProduct.assoc ℂ ContrℂModule CoℂModule CoℂModule).symm) ((TensorProduct.assoc ℂ ContrℂModule ContrℂModule (CoℂModule ⊗[ℂ] CoℂModule)) ((complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) ⊗ₜ[ℂ] (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2))))))) = coContrUnit ↑1 ⊢ contrCoContraction (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - contrCoContraction (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - contrCoContraction (complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - contrCoContraction (complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) - (contrCoContraction (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - contrCoContraction (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - contrCoContraction (complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - contrCoContraction (complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) - (contrCoContraction (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - contrCoContraction (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - contrCoContraction (complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - contrCoContraction (complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) - (contrCoContraction (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - contrCoContraction (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - contrCoContraction (complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - contrCoContraction (complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) = coContrUnit 1 ⊢ contrCoContraction.toLinearMap (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) - (contrCoContraction.toLinearMap (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) - (contrCoContraction.toLinearMap (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) - (contrCoContraction.toLinearMap (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) = coContrUnit.toLinearMap 1 repeat erw [⊢ (if Sum.inl 0 = Sum.inl 0 then 1 else 0) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0)) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) - (contrCoContraction.toLinearMap (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0)) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) - (contrCoContraction.toLinearMap (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1)) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) - (contrCoContraction.toLinearMap (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - contrCoContraction.toLinearMap (complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) = coContrUnit.toLinearMap 1⊢ (if Sum.inl 0 = Sum.inl 0 then 1 else 0) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - (if Sum.inr 0 = Sum.inl 0 then 1 else 0) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - (if Sum.inr 1 = Sum.inl 0 then 1 else 0) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - (if Sum.inr 2 = Sum.inl 0 then 1 else 0) • complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) - ((if Sum.inl 0 = Sum.inr 0 then 1 else 0) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - (if Sum.inr 0 = Sum.inr 0 then 1 else 0) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - (if Sum.inr 1 = Sum.inr 0 then 1 else 0) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - (if Sum.inr 2 = Sum.inr 0 then 1 else 0) • complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) - ((if Sum.inl 0 = Sum.inr 1 then 1 else 0) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - (if Sum.inr 0 = Sum.inr 1 then 1 else 0) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - (if Sum.inr 1 = Sum.inr 1 then 1 else 0) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - (if Sum.inr 2 = Sum.inr 1 then 1 else 0) • complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) - ((if Sum.inl 0 = Sum.inr 2 then 1 else 0) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - (if Sum.inr 0 = Sum.inr 2 then 1 else 0) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - (if Sum.inr 1 = Sum.inr 2 then 1 else 0) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - (if Sum.inr 2 = Sum.inr 2 then 1 else 0) • complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) = coContrUnit.toLinearMap 1 ⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) + complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) + complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) + complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) = coContrUnit.toLinearMap 1 erw [⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) + complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) + complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) + complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) = coContrUnitVal ⊢ complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) + complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) + complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) + complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2) = complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) + complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) + complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) + complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)All goals completed! 🐙⊢ (TensorProduct.comm ℂ CoℂModule ContrℂModule) ((LinearEquiv.lTensor CoℂModule (TensorProduct.lid ℂ ContrℂModule)) ((LinearMap.lTensor CoℂModule (LinearMap.rTensor ContrℂModule coContrContraction.toLinearMap)) ((LinearMap.lTensor CoℂModule ↑(TensorProduct.assoc ℂ CoℂModule ContrℂModule ContrℂModule).symm) ((TensorProduct.assoc ℂ CoℂModule CoℂModule (ContrℂModule ⊗[ℂ] ContrℂModule)) ((complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) ⊗ₜ[ℂ] (complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0) - complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0) - complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1) - complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2))))))) = contrCoUnit ↑1 ⊢ coContrContraction (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - coContrContraction (complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - coContrContraction (complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - coContrContraction (complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) - (coContrContraction (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - coContrContraction (complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - coContrContraction (complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - coContrContraction (complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) - (coContrContraction (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - coContrContraction (complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - coContrContraction (complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - coContrContraction (complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) - (coContrContraction (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - coContrContraction (complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - coContrContraction (complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - coContrContraction (complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) = contrCoUnit 1 ⊢ coContrContraction.toLinearMap (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) - (coContrContraction.toLinearMap (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) - (coContrContraction.toLinearMap (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) - (coContrContraction.toLinearMap (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) = contrCoUnit.toLinearMap 1 repeat erw [⊢ (if Sum.inl 0 = Sum.inl 0 then 1 else 0) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inl 0)) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) - (coContrContraction.toLinearMap (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 0)) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) - (coContrContraction.toLinearMap (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 1)) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) - (coContrContraction.toLinearMap (complexCoBasis (Sum.inl 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 0) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 1) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - coContrContraction.toLinearMap (complexCoBasis (Sum.inr 2) ⊗ₜ[ℂ] complexContrBasis (Sum.inr 2)) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) = contrCoUnit.toLinearMap 1⊢ (if Sum.inl 0 = Sum.inl 0 then 1 else 0) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - (if Sum.inr 0 = Sum.inl 0 then 1 else 0) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - (if Sum.inr 1 = Sum.inl 0 then 1 else 0) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - (if Sum.inr 2 = Sum.inl 0 then 1 else 0) • complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) - ((if Sum.inl 0 = Sum.inr 0 then 1 else 0) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - (if Sum.inr 0 = Sum.inr 0 then 1 else 0) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - (if Sum.inr 1 = Sum.inr 0 then 1 else 0) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - (if Sum.inr 2 = Sum.inr 0 then 1 else 0) • complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) - ((if Sum.inl 0 = Sum.inr 1 then 1 else 0) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - (if Sum.inr 0 = Sum.inr 1 then 1 else 0) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - (if Sum.inr 1 = Sum.inr 1 then 1 else 0) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - (if Sum.inr 2 = Sum.inr 1 then 1 else 0) • complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) - ((if Sum.inl 0 = Sum.inr 2 then 1 else 0) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) - (if Sum.inr 0 = Sum.inr 2 then 1 else 0) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) - (if Sum.inr 1 = Sum.inr 2 then 1 else 0) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) - (if Sum.inr 2 = Sum.inr 2 then 1 else 0) • complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)) = contrCoUnit.toLinearMap 1 ⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) + complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) + complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) = contrCoUnit 1 erw [⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) + complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) + complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) = contrCoUnitVal ⊢ complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) + complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) + complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2) = complexContrBasis (Sum.inl 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inl 0) + complexContrBasis (Sum.inr 0) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 0) + complexContrBasis (Sum.inr 1) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 1) + complexContrBasis (Sum.inr 2) ⊗ₜ[ℂ] complexCoBasis (Sum.inr 2)All goals completed! 🐙