Physlib.Relativity.Tensors.RealTensor.Units.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.RealTensor.Matrix.Pre
public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Contraction

Unit for complex Lorentz vectors

@[expose] public section

The contra-co unit for complex lorentz vectors. Usually denoted δⁱᵢ.

def preContrCoUnitVal (d : ℕ := 3) : ContrMod d ⊗[ℝ] CoMod d :=
  contrCoToMatrixRe.symm 1

Expansion of preContrCoUnitVal into basis.


lemma preContrCoUnitVal_expand_tmul {d : ℕ} : preContrCoUnitVal d =
    ∑ i, contrBasis d i ⊗ₜ[ℝ] coBasis d i := byd:ℕ⊢ preContrCoUnitVal d = ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i
  simp only [preContrCoUnitVal]d:ℕ⊢ contrCoToMatrixRe.symm 1 = ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i
  rw [contrCoToMatrixRe_symm_expand_tmuld:ℕ⊢ ∑ i, ∑ j, 1 i j • (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) j = ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) id:ℕ⊢ ∑ i, ∑ j, 1 i j • (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) j = ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i]d:ℕ⊢ ∑ i, ∑ j, 1 i j • (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) j = ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i
  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
    Finset.sum_singleton, ne_eq, reduceCtorEq, not_false_eq_true, one_apply_ne, zero_smul,
    Finset.sum_const_zero, add_zero, one_apply_eq, one_smul, zero_add]d:ℕ⊢ (contrBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (coBasis d) (Sum.inl 0) +
    ∑ x, ∑ a₂, 1 (Sum.inr x) (Sum.inr a₂) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr a₂) =
  (contrBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (coBasis d) (Sum.inl 0) +
    ∑ a₂, (contrBasis d) (Sum.inr a₂) ⊗ₜ[ℝ] (coBasis d) (Sum.inr a₂)
  congre_a.e_fd:ℕ⊢ (fun x => ∑ a₂, 1 (Sum.inr x) (Sum.inr a₂) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr a₂)) = fun a₂ =>
  (contrBasis d) (Sum.inr a₂) ⊗ₜ[ℝ] (coBasis d) (Sum.inr a₂)
  funext xe_a.e_fd:ℕx:Fin d⊢ ∑ a₂, 1 (Sum.inr x) (Sum.inr a₂) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr a₂) =
  (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr x)
  rw [Finset.sum_eq_single xe_a.e_fd:ℕx:Fin d⊢ 1 (Sum.inr x) (Sum.inr x) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr x) =
  (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr x)e_a.e_f.h₀d:ℕx:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ x → 1 (Sum.inr x) (Sum.inr b) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr b) = 0e_a.e_f.h₁d:ℕx:Fin d⊢ x ∉ Finset.univ → 1 (Sum.inr x) (Sum.inr x) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr x) = 0e_a.e_fd:ℕx:Fin d⊢ 1 (Sum.inr x) (Sum.inr x) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr x) =
  (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr x)e_a.e_f.h₀d:ℕx:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ x → 1 (Sum.inr x) (Sum.inr b) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr b) = 0e_a.e_f.h₁d:ℕx:Fin d⊢ x ∉ Finset.univ → 1 (Sum.inr x) (Sum.inr x) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr x) = 0]e_a.e_fd:ℕx:Fin d⊢ 1 (Sum.inr x) (Sum.inr x) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr x) =
  (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr x)e_a.e_f.h₀d:ℕx:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ x → 1 (Sum.inr x) (Sum.inr b) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr b) = 0e_a.e_f.h₁d:ℕx:Fin d⊢ x ∉ Finset.univ → 1 (Sum.inr x) (Sum.inr x) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr x) = 0
  ·e_a.e_fd:ℕx:Fin d⊢ 1 (Sum.inr x) (Sum.inr x) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr x) =
  (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr x) simpAll goals completed! 🐙
  ·e_a.e_f.h₀d:ℕx:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ x → 1 (Sum.inr x) (Sum.inr b) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr b) = 0 simp only [Finset.mem_univ, ne_eq, smul_eq_zero, forall_const]e_a.e_f.h₀d:ℕx:Fin d⊢ ∀ (b : Fin d), ¬b = x → 1 (Sum.inr x) (Sum.inr b) = 0 ∨ (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr b) = 0
    intro b hbe_a.e_f.h₀d:ℕx:Fin db:Fin dhb:¬b = x⊢ 1 (Sum.inr x) (Sum.inr b) = 0 ∨ (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr b) = 0
    lefte_a.e_f.h₀d:ℕx:Fin db:Fin dhb:¬b = x⊢ 1 (Sum.inr x) (Sum.inr b) = 0
    refine one_apply_ne' ?_e_a.e_f.h₀d:ℕx:Fin db:Fin dhb:¬b = x⊢ Sum.inr b ≠ Sum.inr x
    simp [hb]All goals completed! 🐙
  ·e_a.e_f.h₁d:ℕx:Fin d⊢ x ∉ Finset.univ → 1 (Sum.inr x) (Sum.inr x) • (contrBasis d) (Sum.inr x) ⊗ₜ[ℝ] (coBasis d) (Sum.inr x) = 0 simpAll goals completed! 🐙

The contra-co unit for complex lorentz vectors as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ complexCo, manifesting the invariance under the SL(2, ℂ) action.

set_option backward.isDefEq.respectTransparency false in


def preContrCoUnit (d : ℕ := 3) :
  (Representation.trivial ℝ (LorentzGroup d) ℝ).IntertwiningMap
    ((ContrMod.rep).tprod (CoMod.rep)) where
  toFun := fun a => a • preContrCoUnitVal d
  map_add' := fun x y => byd:ℕx:ℝy:ℝ⊢ (x + y) • preContrCoUnitVal d = x • preContrCoUnitVal d + y • preContrCoUnitVal d
    simp only [add_smul]All goals completed! 🐙
  map_smul' := fun m x => byd:ℕm:ℝx:ℝ⊢ (m • x) • preContrCoUnitVal d = (RingHom.id ℝ) m • x • preContrCoUnitVal d
    simp only [smul_smul]d:ℕm:ℝx:ℝ⊢ (m • x) • preContrCoUnitVal d = ((RingHom.id ℝ) m * x) • preContrCoUnitVal d
    rflAll goals completed! 🐙
  isIntertwining' M := byd:ℕM:↑(LorentzGroup d)⊢ { toFun := fun a => a • preContrCoUnitVal d, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
    (Representation.trivial ℝ ↑(LorentzGroup d) ℝ) M =
  (ContrMod.rep.tprod CoMod.rep) M ∘ₗ { toFun := fun a => a • preContrCoUnitVal d, map_add' := ⋯, map_smul' := ⋯ }
    refine LinearMap.ext fun x : ℝ => ?_d:ℕM:↑(LorentzGroup d)x:ℝ⊢ ({ toFun := fun a => a • preContrCoUnitVal d, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      (Representation.trivial ℝ ↑(LorentzGroup d) ℝ) M)
    x =
  ((ContrMod.rep.tprod CoMod.rep) M ∘ₗ { toFun := fun a => a • preContrCoUnitVal d, map_add' := ⋯, map_smul' := ⋯ }) x
    simp only [LinearMap.coe_comp, Function.comp_apply]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ { toFun := fun a => a • preContrCoUnitVal d, map_add' := ⋯, map_smul' := ⋯ }
    (((Representation.trivial ℝ ↑(LorentzGroup d) ℝ) M) x) =
  ((ContrMod.rep.tprod CoMod.rep) M) ({ toFun := fun a => a • preContrCoUnitVal d, map_add' := ⋯, map_smul' := ⋯ } x)
    change x • preContrCoUnitVal d =
      (TensorProduct.map (ContrMod.rep M) (CoMod.rep M)) (x • preContrCoUnitVal d)d:ℕM:↑(LorentzGroup d)x:ℝ⊢ x • preContrCoUnitVal d = (TensorProduct.map (ContrMod.rep M) (CoMod.rep M)) (x • preContrCoUnitVal d)
    simp only [map_smul]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ x • preContrCoUnitVal d = x • (TensorProduct.map (ContrMod.rep M) (CoMod.rep M)) (preContrCoUnitVal d)
    apply congrArgd:ℕM:↑(LorentzGroup d)x:ℝ⊢ preContrCoUnitVal d = (TensorProduct.map (ContrMod.rep M) (CoMod.rep M)) (preContrCoUnitVal d)
    simp only [preContrCoUnitVal]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ contrCoToMatrixRe.symm 1 = (TensorProduct.map (ContrMod.rep M) (CoMod.rep M)) (contrCoToMatrixRe.symm 1)
    rw [contrCoToMatrixRe_ρ_symmd:ℕM:↑(LorentzGroup d)x:ℝ⊢ contrCoToMatrixRe.symm 1 = contrCoToMatrixRe.symm (↑M * 1 * (↑M)⁻¹)d:ℕM:↑(LorentzGroup d)x:ℝ⊢ contrCoToMatrixRe.symm 1 = contrCoToMatrixRe.symm (↑M * 1 * (↑M)⁻¹)]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ contrCoToMatrixRe.symm 1 = contrCoToMatrixRe.symm (↑M * 1 * (↑M)⁻¹)
    apply congrArgd:ℕM:↑(LorentzGroup d)x:ℝ⊢ 1 = ↑M * 1 * (↑M)⁻¹
    simpAll goals completed! 🐙



lemma preContrCoUnit_apply_one {d : ℕ} : (preContrCoUnit d) (1 : ℝ) = preContrCoUnitVal d := byd:ℕ⊢ (preContrCoUnit d) 1 = preContrCoUnitVal d
  change (1 : ℝ) • preContrCoUnitVal d = preContrCoUnitVal dd:ℕ⊢ 1 • preContrCoUnitVal d = preContrCoUnitVal d
  rw [one_smuld:ℕ⊢ preContrCoUnitVal d = preContrCoUnitVal dAll goals completed! 🐙]All goals completed! 🐙

The co-contra unit for complex lorentz vectors. Usually denoted δᵢⁱ.

def preCoContrUnitVal (d : ℕ := 3) : CoMod d ⊗[ℝ] ContrMod d :=
  coContrToMatrixRe.symm 1

Expansion of preCoContrUnitVal into basis.


lemma preCoContrUnitVal_expand_tmul {d : ℕ} : preCoContrUnitVal d =
    ∑ i, coBasis d i ⊗ₜ[ℝ] contrBasis d i := byd:ℕ⊢ preCoContrUnitVal d = ∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i
  simp only [preCoContrUnitVal]d:ℕ⊢ coContrToMatrixRe.symm 1 = ∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i
  rw [coContrToMatrixRe_symm_expand_tmuld:ℕ⊢ ∑ i, ∑ j, 1 i j • (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) j = ∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) id:ℕ⊢ ∑ i, ∑ j, 1 i j • (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) j = ∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i]d:ℕ⊢ ∑ i, ∑ j, 1 i j • (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) j = ∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i
  simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
    Finset.sum_singleton, ne_eq, reduceCtorEq, not_false_eq_true, one_apply_ne, zero_smul,
    Finset.sum_const_zero, add_zero, one_apply_eq, one_smul, zero_add]d:ℕ⊢ (coBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (contrBasis d) (Sum.inl 0) +
    ∑ x, ∑ a₂, 1 (Sum.inr x) (Sum.inr a₂) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr a₂) =
  (coBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (contrBasis d) (Sum.inl 0) +
    ∑ a₂, (coBasis d) (Sum.inr a₂) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr a₂)
  congre_a.e_fd:ℕ⊢ (fun x => ∑ a₂, 1 (Sum.inr x) (Sum.inr a₂) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr a₂)) = fun a₂ =>
  (coBasis d) (Sum.inr a₂) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr a₂)
  funext xe_a.e_fd:ℕx:Fin d⊢ ∑ a₂, 1 (Sum.inr x) (Sum.inr a₂) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr a₂) =
  (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr x)
  rw [Finset.sum_eq_single xe_a.e_fd:ℕx:Fin d⊢ 1 (Sum.inr x) (Sum.inr x) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr x) =
  (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr x)e_a.e_f.h₀d:ℕx:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ x → 1 (Sum.inr x) (Sum.inr b) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr b) = 0e_a.e_f.h₁d:ℕx:Fin d⊢ x ∉ Finset.univ → 1 (Sum.inr x) (Sum.inr x) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr x) = 0e_a.e_fd:ℕx:Fin d⊢ 1 (Sum.inr x) (Sum.inr x) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr x) =
  (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr x)e_a.e_f.h₀d:ℕx:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ x → 1 (Sum.inr x) (Sum.inr b) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr b) = 0e_a.e_f.h₁d:ℕx:Fin d⊢ x ∉ Finset.univ → 1 (Sum.inr x) (Sum.inr x) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr x) = 0]e_a.e_fd:ℕx:Fin d⊢ 1 (Sum.inr x) (Sum.inr x) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr x) =
  (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr x)e_a.e_f.h₀d:ℕx:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ x → 1 (Sum.inr x) (Sum.inr b) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr b) = 0e_a.e_f.h₁d:ℕx:Fin d⊢ x ∉ Finset.univ → 1 (Sum.inr x) (Sum.inr x) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr x) = 0
  ·e_a.e_fd:ℕx:Fin d⊢ 1 (Sum.inr x) (Sum.inr x) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr x) =
  (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr x) simpAll goals completed! 🐙
  ·e_a.e_f.h₀d:ℕx:Fin d⊢ ∀ b ∈ Finset.univ, b ≠ x → 1 (Sum.inr x) (Sum.inr b) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr b) = 0 simp only [Finset.mem_univ, ne_eq, smul_eq_zero, forall_const]e_a.e_f.h₀d:ℕx:Fin d⊢ ∀ (b : Fin d), ¬b = x → 1 (Sum.inr x) (Sum.inr b) = 0 ∨ (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr b) = 0
    intro b hbe_a.e_f.h₀d:ℕx:Fin db:Fin dhb:¬b = x⊢ 1 (Sum.inr x) (Sum.inr b) = 0 ∨ (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr b) = 0
    lefte_a.e_f.h₀d:ℕx:Fin db:Fin dhb:¬b = x⊢ 1 (Sum.inr x) (Sum.inr b) = 0
    refine one_apply_ne' ?_e_a.e_f.h₀d:ℕx:Fin db:Fin dhb:¬b = x⊢ Sum.inr b ≠ Sum.inr x
    simp [hb]All goals completed! 🐙
  ·e_a.e_f.h₁d:ℕx:Fin d⊢ x ∉ Finset.univ → 1 (Sum.inr x) (Sum.inr x) • (coBasis d) (Sum.inr x) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr x) = 0 simpAll goals completed! 🐙

The co-contra unit for complex lorentz vectors as a morphism 𝟙_ (Rep ℝ (LorentzGroup d)) ⟶ CoMod.rep ⊗ ContrMod.rep, manifesting the invariance under the LorentzGroup d action.

set_option backward.isDefEq.respectTransparency false in


def preCoContrUnit (d : ℕ) : (Representation.trivial ℝ (LorentzGroup d) ℝ).IntertwiningMap
    ((CoMod.rep).tprod (ContrMod.rep)) where
  toFun := fun a => a • preCoContrUnitVal d
  map_add' := fun x y => byd:ℕx:ℝy:ℝ⊢ (x + y) • preCoContrUnitVal d = x • preCoContrUnitVal d + y • preCoContrUnitVal d
    simp only [add_smul]All goals completed! 🐙
  map_smul' := fun m x => byd:ℕm:ℝx:ℝ⊢ (m • x) • preCoContrUnitVal d = (RingHom.id ℝ) m • x • preCoContrUnitVal d
    simp only [smul_smul]d:ℕm:ℝx:ℝ⊢ (m • x) • preCoContrUnitVal d = ((RingHom.id ℝ) m * x) • preCoContrUnitVal d
    rflAll goals completed! 🐙
  isIntertwining' M := byd:ℕM:↑(LorentzGroup d)⊢ { toFun := fun a => a • preCoContrUnitVal d, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
    (Representation.trivial ℝ ↑(LorentzGroup d) ℝ) M =
  (CoMod.rep.tprod ContrMod.rep) M ∘ₗ { toFun := fun a => a • preCoContrUnitVal d, map_add' := ⋯, map_smul' := ⋯ }
    refine LinearMap.ext fun x : ℝ => ?_d:ℕM:↑(LorentzGroup d)x:ℝ⊢ ({ toFun := fun a => a • preCoContrUnitVal d, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      (Representation.trivial ℝ ↑(LorentzGroup d) ℝ) M)
    x =
  ((CoMod.rep.tprod ContrMod.rep) M ∘ₗ { toFun := fun a => a • preCoContrUnitVal d, map_add' := ⋯, map_smul' := ⋯ }) x
    simp only [LinearMap.coe_comp, Function.comp_apply]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ { toFun := fun a => a • preCoContrUnitVal d, map_add' := ⋯, map_smul' := ⋯ }
    (((Representation.trivial ℝ ↑(LorentzGroup d) ℝ) M) x) =
  ((CoMod.rep.tprod ContrMod.rep) M) ({ toFun := fun a => a • preCoContrUnitVal d, map_add' := ⋯, map_smul' := ⋯ } x)
    change x • preCoContrUnitVal d =
      (TensorProduct.map (CoMod.rep M) (ContrMod.rep M)) (x • preCoContrUnitVal d)d:ℕM:↑(LorentzGroup d)x:ℝ⊢ x • preCoContrUnitVal d = (TensorProduct.map (CoMod.rep M) (ContrMod.rep M)) (x • preCoContrUnitVal d)
    simp only [map_smul]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ x • preCoContrUnitVal d = x • (TensorProduct.map (CoMod.rep M) (ContrMod.rep M)) (preCoContrUnitVal d)
    apply congrArgd:ℕM:↑(LorentzGroup d)x:ℝ⊢ preCoContrUnitVal d = (TensorProduct.map (CoMod.rep M) (ContrMod.rep M)) (preCoContrUnitVal d)
    simp only [preCoContrUnitVal]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ coContrToMatrixRe.symm 1 = (TensorProduct.map (CoMod.rep M) (ContrMod.rep M)) (coContrToMatrixRe.symm 1)
    rw [coContrToMatrixRe_ρ_symmd:ℕM:↑(LorentzGroup d)x:ℝ⊢ coContrToMatrixRe.symm 1 = coContrToMatrixRe.symm ((↑M)⁻¹ᵀ * 1 * (↑M)ᵀ)d:ℕM:↑(LorentzGroup d)x:ℝ⊢ coContrToMatrixRe.symm 1 = coContrToMatrixRe.symm ((↑M)⁻¹ᵀ * 1 * (↑M)ᵀ)]d:ℕM:↑(LorentzGroup d)x:ℝ⊢ coContrToMatrixRe.symm 1 = coContrToMatrixRe.symm ((↑M)⁻¹ᵀ * 1 * (↑M)ᵀ)
    apply congrArgd:ℕM:↑(LorentzGroup d)x:ℝ⊢ 1 = (↑M)⁻¹ᵀ * 1 * (↑M)ᵀ
    symmd:ℕM:↑(LorentzGroup d)x:ℝ⊢ (↑M)⁻¹ᵀ * 1 * (↑M)ᵀ = 1
    refine transpose_eq_one.mp ?h.h.h.ah.h.h.ad:ℕM:↑(LorentzGroup d)x:ℝ⊢ ((↑M)⁻¹ᵀ * 1 * (↑M)ᵀ)ᵀ = 1
    simpAll goals completed! 🐙



lemma preCoContrUnit_apply_one {d : ℕ} : (preCoContrUnit d) (1 : ℝ) = preCoContrUnitVal d := byd:ℕ⊢ (preCoContrUnit d) 1 = preCoContrUnitVal d
  change (1 : ℝ) • preCoContrUnitVal d = preCoContrUnitVal dd:ℕ⊢ 1 • preCoContrUnitVal d = preCoContrUnitVal d
  rw [one_smuld:ℕ⊢ preCoContrUnitVal d = preCoContrUnitVal dAll goals completed! 🐙]All goals completed! 🐙

Contraction of the units

Contraction on the right with contrCoUnit does nothing.


lemma contr_preContrCoUnit {d : ℕ} (x : CoMod d) :
    (TensorProduct.lid ℝ _ <|
    coContrContract.toLinearMap.rTensor _ <|
    (TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm <|
    x ⊗ₜ[ℝ] (preContrCoUnit d (1 : ℝ))) = x := byd:ℕx:CoMod d⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
      ((TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1))) =
  x
  have h1 : (TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm
      (x ⊗ₜ[ℝ] (preContrCoUnit d) (1 : ℝ))
      = ∑ i, (x ⊗ₜ[ℝ] contrBasis d i) ⊗ₜ[ℝ] coBasis d i := by
    rw [preContrCoUnit_apply_one,d:ℕx:CoMod d⊢ (TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] preContrCoUnitVal d) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) id:ℕx:CoMod d⊢ (TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) id:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
      ((TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1))) =
  x preContrCoUnitVal_expand_tmuld:ℕx:CoMod d⊢ (TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) id:ℕx:CoMod d⊢ (TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) id:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
      ((TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1))) =
  x]d:ℕx:CoMod d⊢ (TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) id:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
      ((TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1))) =
  x
    simp only [tmul_sum]d:ℕx:CoMod d⊢ (TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (∑ a, x ⊗ₜ[ℝ] ((contrBasis d) a ⊗ₜ[ℝ] (coBasis d) a)) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) id:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
      ((TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1))) =
  x
    simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
      Finset.sum_singleton, map_add, map_sum]d:ℕx:CoMod d⊢ (TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm
      (x ⊗ₜ[ℝ] ((contrBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (coBasis d) (Sum.inl 0))) +
    ∑ x_1,
      (TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm
        (x ⊗ₜ[ℝ] ((contrBasis d) (Sum.inr x_1) ⊗ₜ[ℝ] (coBasis d) (Sum.inr x_1))) =
  x ⊗ₜ[ℝ] (contrBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (coBasis d) (Sum.inl 0) +
    ∑ a₂, x ⊗ₜ[ℝ] (contrBasis d) (Sum.inr a₂) ⊗ₜ[ℝ] (coBasis d) (Sum.inr a₂)d:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
      ((TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1))) =
  x
    rfld:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
      ((TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1))) =
  xd:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
      ((TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1))) =
  x
  rw [h1d:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i)) =
  xd:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i)) =
  x]d:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i)) =
  x
  have h2 : coContrContract.toLinearMap.rTensor _ (∑ i, (x ⊗ₜ[ℝ] contrBasis d i) ⊗ₜ[ℝ] coBasis d i)
      = ∑ i, ((coContrContract) (x ⊗ₜ[ℝ] contrBasis d i)) ⊗ₜ[ℝ] coBasis d i := byd:ℕx:CoMod d⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
      ((TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1))) =
  xd:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract (x ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i)) =
  x
    rw [map_sumd:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i⊢ ∑ x_1, (LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (x ⊗ₜ[ℝ] (contrBasis d) x_1 ⊗ₜ[ℝ] (coBasis d) x_1) =
  ∑ i, coContrContract (x ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) id:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i⊢ ∑ x_1, (LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (x ⊗ₜ[ℝ] (contrBasis d) x_1 ⊗ₜ[ℝ] (coBasis d) x_1) =
  ∑ i, coContrContract (x ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) id:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract (x ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i)) =
  x]d:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i⊢ ∑ x_1, (LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (x ⊗ₜ[ℝ] (contrBasis d) x_1 ⊗ₜ[ℝ] (coBasis d) x_1) =
  ∑ i, coContrContract (x ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) id:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract (x ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i)) =
  x
    rfld:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract (x ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i)) =
  xd:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract (x ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i)) =
  x
  erw [h2d:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract (x ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d)) (∑ i, coContrContract (x ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) = x]d:ℕx:CoMod dh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract (x ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d)) (∑ i, coContrContract (x ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) = x
  obtain ⟨c, rfl⟩ := (Submodule.mem_span_range_iff_exists_fun ℝ).mp (Basis.mem_span (coBasis d) x)d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i⊢ (TensorProduct.lid ℝ (CoMod d))
    (∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, c i • (coBasis d) i
  have h3 (i : Fin 1 ⊕ Fin d) : (coContrContract)
        ((∑ i : Fin 1 ⊕ Fin d, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) = c i := byd:ℕx:CoMod d⊢ (TensorProduct.lid ℝ (CoMod d))
    ((LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
      ((TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm (x ⊗ₜ[ℝ] (preContrCoUnit d) 1))) =
  xd:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) = c i⊢ (TensorProduct.lid ℝ (CoMod d))
    (∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, c i • (coBasis d) i
      simp only [sum_tmul, smul_tmul, tmul_smul, map_sum, _root_.map_smul, smul_eq_mul]d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) ii:Fin 1 ⊕ Fin d⊢ ∑ x, c x * coContrContract ((coBasis d) x ⊗ₜ[ℝ] (contrBasis d) i) = c id:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) = c i⊢ (TensorProduct.lid ℝ (CoMod d))
    (∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, c i • (coBasis d) i
      conv_lhs =>
        enter [2, x]d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) ii:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin d| c x * coContrContract ((coBasis d) x ⊗ₜ[ℝ] (contrBasis d) i)d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) = c i⊢ (TensorProduct.lid ℝ (CoMod d))
    (∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, c i • (coBasis d) i
        rw [coContrContract_basis]d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) ii:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin d| c x * if x = i then 1 else 0d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) = c i⊢ (TensorProduct.lid ℝ (CoMod d))
    (∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, c i • (coBasis d) i
      simpd:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) = c i⊢ (TensorProduct.lid ℝ (CoMod d))
    (∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, c i • (coBasis d) id:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) = c i⊢ (TensorProduct.lid ℝ (CoMod d))
    (∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, c i • (coBasis d) i
  conv_lhs =>
    enter [2, 2, i]d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) = c ii:Fin 1 ⊕ Fin d| coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i
    rw [h3 i]d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) = c ii:Fin 1 ⊕ Fin d| c i ⊗ₜ[ℝ] (coBasis d) i
  rw [map_sumd:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) = c i⊢ ∑ x, (TensorProduct.lid ℝ (CoMod d)) (c x ⊗ₜ[ℝ] (coBasis d) x) = ∑ i, c i • (coBasis d) id:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) = c i⊢ ∑ x, (TensorProduct.lid ℝ (CoMod d)) (c x ⊗ₜ[ℝ] (coBasis d) x) = ∑ i, c i • (coBasis d) i]d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (CoMod d) (ContrMod d) (CoMod d)).symm ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (preContrCoUnit d) 1) =
  ∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) ih2:(LinearMap.rTensor (CoMod d) coContrContract.toLinearMap)
    (∑ i, (∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i) =
  ∑ i, coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), coContrContract ((∑ i, c i • (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) = c i⊢ ∑ x, (TensorProduct.lid ℝ (CoMod d)) (c x ⊗ₜ[ℝ] (coBasis d) x) = ∑ i, c i • (coBasis d) i
  rflAll goals completed! 🐙

Contraction on the right with coContrUnit.


lemma contr_preCoContrUnit {d : ℕ} (x : ContrMod d) :
    (TensorProduct.lid ℝ _ <|
    contrCoContract.toLinearMap.rTensor _ <|
    (TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm <|
    x ⊗ₜ[ℝ] (preCoContrUnit d (1 : ℝ))) = x := byd:ℕx:ContrMod d⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
      ((TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1))) =
  x
  have h1 : ((TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
      (x ⊗ₜ[ℝ] (preCoContrUnit d) (1 : ℝ)))
      = ∑ i, (x ⊗ₜ[ℝ] coBasis d i) ⊗ₜ[ℝ] contrBasis d i := by
    rw [preCoContrUnit_apply_one,d:ℕx:ContrMod d⊢ (TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] preCoContrUnitVal d) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) id:ℕx:ContrMod d⊢ (TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] ∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) id:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
      ((TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1))) =
  x preCoContrUnitVal_expand_tmuld:ℕx:ContrMod d⊢ (TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] ∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) id:ℕx:ContrMod d⊢ (TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] ∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) id:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
      ((TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1))) =
  x]d:ℕx:ContrMod d⊢ (TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] ∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) id:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
      ((TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1))) =
  x
    simp only [tmul_sum]d:ℕx:ContrMod d⊢ (TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (∑ a, x ⊗ₜ[ℝ] ((coBasis d) a ⊗ₜ[ℝ] (contrBasis d) a)) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) id:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
      ((TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1))) =
  x
    simp only [Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
      Finset.sum_singleton, map_add, map_sum]d:ℕx:ContrMod d⊢ (TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
      (x ⊗ₜ[ℝ] ((coBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (contrBasis d) (Sum.inl 0))) +
    ∑ x_1,
      (TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
        (x ⊗ₜ[ℝ] ((coBasis d) (Sum.inr x_1) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr x_1))) =
  x ⊗ₜ[ℝ] (coBasis d) (Sum.inl 0) ⊗ₜ[ℝ] (contrBasis d) (Sum.inl 0) +
    ∑ a₂, x ⊗ₜ[ℝ] (coBasis d) (Sum.inr a₂) ⊗ₜ[ℝ] (contrBasis d) (Sum.inr a₂)d:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
      ((TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1))) =
  x
    rfld:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
      ((TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1))) =
  xd:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
      ((TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1))) =
  x
  rw [h1d:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i)) =
  xd:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i)) =
  x]d:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i)) =
  x
  have h2 :contrCoContract.toLinearMap.rTensor _ (∑ i, (x ⊗ₜ[ℝ] coBasis d i) ⊗ₜ[ℝ] contrBasis d i)
      = ∑ i, ((contrCoContract) (x ⊗ₜ[ℝ] coBasis d i)) ⊗ₜ[ℝ] contrBasis d i := byd:ℕx:ContrMod d⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
      ((TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1))) =
  xd:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract (x ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i)) =
  x
    rw [map_sumd:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i⊢ ∑ x_1, (LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (x ⊗ₜ[ℝ] (coBasis d) x_1 ⊗ₜ[ℝ] (contrBasis d) x_1) =
  ∑ i, contrCoContract (x ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) id:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i⊢ ∑ x_1, (LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (x ⊗ₜ[ℝ] (coBasis d) x_1 ⊗ₜ[ℝ] (contrBasis d) x_1) =
  ∑ i, contrCoContract (x ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) id:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract (x ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i)) =
  x]d:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i⊢ ∑ x_1, (LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (x ⊗ₜ[ℝ] (coBasis d) x_1 ⊗ₜ[ℝ] (contrBasis d) x_1) =
  ∑ i, contrCoContract (x ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) id:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract (x ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i)) =
  x
    rfld:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract (x ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i)) =
  xd:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract (x ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i)) =
  x
  erw [h2d:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract (x ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d)) (∑ i, contrCoContract (x ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) = x]d:ℕx:ContrMod dh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap) (∑ i, x ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract (x ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d)) (∑ i, contrCoContract (x ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) = x
  obtain ⟨c, rfl⟩ := (Submodule.mem_span_range_iff_exists_fun ℝ).mp
    (Basis.mem_span (contrBasis d) x)d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i⊢ (TensorProduct.lid ℝ (ContrMod d))
    (∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, c i • (contrBasis d) i
  have h3 (i : Fin 1 ⊕ Fin d) : (contrCoContract)
        ((∑ i : Fin 1 ⊕ Fin d, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) = c i := byd:ℕx:ContrMod d⊢ (TensorProduct.lid ℝ (ContrMod d))
    ((LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
      ((TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm (x ⊗ₜ[ℝ] (preCoContrUnit d) 1))) =
  xd:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) = c i⊢ (TensorProduct.lid ℝ (ContrMod d))
    (∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, c i • (contrBasis d) i
      simp only [sum_tmul, smul_tmul, tmul_smul, map_sum, map_smul, smul_eq_mul]d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) ii:Fin 1 ⊕ Fin d⊢ ∑ x, c x * contrCoContract ((contrBasis d) x ⊗ₜ[ℝ] (coBasis d) i) = c id:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) = c i⊢ (TensorProduct.lid ℝ (ContrMod d))
    (∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, c i • (contrBasis d) i
      conv_lhs =>
        enter [2, x]d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) ii:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin d| c x * contrCoContract ((contrBasis d) x ⊗ₜ[ℝ] (coBasis d) i)d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) = c i⊢ (TensorProduct.lid ℝ (ContrMod d))
    (∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, c i • (contrBasis d) i
        rw [contrCoContract_basis]d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) ii:Fin 1 ⊕ Fin dx:Fin 1 ⊕ Fin d| c x * if x = i then 1 else 0d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) = c i⊢ (TensorProduct.lid ℝ (ContrMod d))
    (∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, c i • (contrBasis d) i
      simpd:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) = c i⊢ (TensorProduct.lid ℝ (ContrMod d))
    (∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, c i • (contrBasis d) id:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) = c i⊢ (TensorProduct.lid ℝ (ContrMod d))
    (∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, c i • (contrBasis d) i
  conv_lhs =>
    enter [2, 2, i]d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) = c ii:Fin 1 ⊕ Fin d| contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) i
    rw [h3 i]d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) = c ii:Fin 1 ⊕ Fin d| c i ⊗ₜ[ℝ] (contrBasis d) i
  rw [map_sumd:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) = c i⊢ ∑ x, (TensorProduct.lid ℝ (ContrMod d)) (c x ⊗ₜ[ℝ] (contrBasis d) x) = ∑ i, c i • (contrBasis d) id:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) = c i⊢ ∑ x, (TensorProduct.lid ℝ (ContrMod d)) (c x ⊗ₜ[ℝ] (contrBasis d) x) = ∑ i, c i • (contrBasis d) i]d:ℕc:Fin 1 ⊕ Fin d → ℝh1:(TensorProduct.assoc ℝ (ContrMod d) (CoMod d) (ContrMod d)).symm
    ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (preCoContrUnit d) 1) =
  ∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) ih2:(LinearMap.rTensor (ContrMod d) contrCoContract.toLinearMap)
    (∑ i, (∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i) =
  ∑ i, contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) ⊗ₜ[ℝ] (contrBasis d) ih3:∀ (i : Fin 1 ⊕ Fin d), contrCoContract ((∑ i, c i • (contrBasis d) i) ⊗ₜ[ℝ] (coBasis d) i) = c i⊢ ∑ x, (TensorProduct.lid ℝ (ContrMod d)) (c x ⊗ₜ[ℝ] (contrBasis d) x) = ∑ i, c i • (contrBasis d) i
  rflAll goals completed! 🐙

Symmetry properties of the units



lemma preContrCoUnit_symm {d : ℕ} :
    (preContrCoUnit d) (1 : ℝ) = LinearMap.lTensor _ (LinearEquiv.cast (byd:ℕ⊢ d = d rflAll goals completed! 🐙)).toLinearMap
      (TensorProduct.comm ℝ _ _ ((preCoContrUnit d) (1 : ℝ))) := byd:ℕ⊢ (preContrCoUnit d) 1 =
  (LinearMap.lTensor (ContrMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (CoMod d) (ContrMod d)) ((preCoContrUnit d) 1))
  rw [preContrCoUnit_apply_one,d:ℕ⊢ preContrCoUnitVal d =
  (LinearMap.lTensor (ContrMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (CoMod d) (ContrMod d)) ((preCoContrUnit d) 1))d:ℕ⊢ ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i =
  (LinearMap.lTensor (ContrMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (CoMod d) (ContrMod d)) ((preCoContrUnit d) 1)) preContrCoUnitVal_expand_tmuld:ℕ⊢ ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i =
  (LinearMap.lTensor (ContrMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (CoMod d) (ContrMod d)) ((preCoContrUnit d) 1))d:ℕ⊢ ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i =
  (LinearMap.lTensor (ContrMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (CoMod d) (ContrMod d)) ((preCoContrUnit d) 1))]d:ℕ⊢ ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i =
  (LinearMap.lTensor (ContrMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (CoMod d) (ContrMod d)) ((preCoContrUnit d) 1))
  rw [preCoContrUnit_apply_one,d:ℕ⊢ ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i =
  (LinearMap.lTensor (ContrMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (CoMod d) (ContrMod d)) (preCoContrUnitVal d))d:ℕ⊢ ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i =
  (LinearMap.lTensor (ContrMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (CoMod d) (ContrMod d)) (∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i)) preCoContrUnitVal_expand_tmuld:ℕ⊢ ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i =
  (LinearMap.lTensor (ContrMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (CoMod d) (ContrMod d)) (∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i))d:ℕ⊢ ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i =
  (LinearMap.lTensor (ContrMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (CoMod d) (ContrMod d)) (∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i))]d:ℕ⊢ ∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i =
  (LinearMap.lTensor (ContrMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (CoMod d) (ContrMod d)) (∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i))
  simpAll goals completed! 🐙



lemma preCoContrUnit_symm {d : ℕ} :
    (preCoContrUnit d) (1 : ℝ) = LinearMap.lTensor _ (LinearEquiv.cast (byd:ℕ⊢ d = d simpAll goals completed! 🐙)).toLinearMap
    (TensorProduct.comm ℝ _ _ ((preContrCoUnit d) (1 : ℝ))) := byd:ℕ⊢ (preCoContrUnit d) 1 =
  (LinearMap.lTensor (CoMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (ContrMod d) (CoMod d)) ((preContrCoUnit d) 1))
  rw [preContrCoUnit_apply_one,d:ℕ⊢ (preCoContrUnit d) 1 =
  (LinearMap.lTensor (CoMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (ContrMod d) (CoMod d)) (preContrCoUnitVal d))d:ℕ⊢ (preCoContrUnit d) 1 =
  (LinearMap.lTensor (CoMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (ContrMod d) (CoMod d)) (∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i)) preContrCoUnitVal_expand_tmuld:ℕ⊢ (preCoContrUnit d) 1 =
  (LinearMap.lTensor (CoMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (ContrMod d) (CoMod d)) (∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i))d:ℕ⊢ (preCoContrUnit d) 1 =
  (LinearMap.lTensor (CoMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (ContrMod d) (CoMod d)) (∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i))]d:ℕ⊢ (preCoContrUnit d) 1 =
  (LinearMap.lTensor (CoMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (ContrMod d) (CoMod d)) (∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i))
  rw [preCoContrUnit_apply_one,d:ℕ⊢ preCoContrUnitVal d =
  (LinearMap.lTensor (CoMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (ContrMod d) (CoMod d)) (∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i))d:ℕ⊢ ∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i =
  (LinearMap.lTensor (CoMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (ContrMod d) (CoMod d)) (∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i)) preCoContrUnitVal_expand_tmuld:ℕ⊢ ∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i =
  (LinearMap.lTensor (CoMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (ContrMod d) (CoMod d)) (∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i))d:ℕ⊢ ∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i =
  (LinearMap.lTensor (CoMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (ContrMod d) (CoMod d)) (∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i))]d:ℕ⊢ ∑ i, (coBasis d) i ⊗ₜ[ℝ] (contrBasis d) i =
  (LinearMap.lTensor (CoMod d) ↑(LinearEquiv.cast ⋯))
    ((TensorProduct.comm ℝ (ContrMod d) (CoMod d)) (∑ i, (contrBasis d) i ⊗ₜ[ℝ] (coBasis d) i))
  simpAll goals completed! 🐙