Physlib.Relativity.Tensors.Contraction.Basic

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Relativity.Tensors.Contraction.Pure

Contractions on tensors

i. Overview

This file defines tensor contraction for an arbitrary TensorSpecies.

The colors of a tensor record the type of each index. A pair of positions can be contracted when their colors are dual, expressed by a proof S.τ (c i) = c j, where S.τ is the color involution in the tensor species. For a tensor with colors c : Fin (n + 1 + 1) → C, contraction at positions i and j produces a tensor with two fewer indices and colors c ∘ Fin.succSuccAbove i j.

The construction is first made on pure tensors in Physlib.Relativity.Tensors.Contraction.Pure. There, Pure.dropPair removes the two contracted factors from the remaining pure tensor, Pure.contrPCoeff computes the scalar contraction of the two removed factors using S.contr, and Pure.contrP multiplies that scalar by the dropped tensor. This file extends the operation linearly to arbitrary tensors via contrT.

ii. Key results

TensorSpecies.Tensor.contrT is the linear contraction map on tensors.

TensorSpecies.Tensor.contrT_pure identifies contrT on pure tensors with Pure.contrP.

TensorSpecies.Tensor.contrT_equivariant says contraction commutes with the symmetry-group action.

TensorSpecies.Tensor.contrT_permT, TensorSpecies.Tensor.contrT_symm, and TensorSpecies.Tensor.contrT_comm describe the interaction of contraction with reindexing, swapping the contracted pair, and performing two contractions.

Physlib.Relativity.Tensors.Contraction.SuccSuccAbove contains the finite-index maps used to drop two positions.

Physlib.Relativity.Tensors.Contraction.Pure defines Pure.dropPair, Pure.contrPCoeff, Pure.contrP, and the multilinear map used to define contrT.

Physlib.Relativity.Tensors.Contraction.Products proves compatibility between contractions and tensor products.

iv. Table of contents

A. Tensor contraction

v. References

There are no known references for the material in this module.

@[expose] public section

A. Tensor contraction

              lemma contrT_decide {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)}
    (hx : S.τ (c i) = c j) (hij : i ≠ j := by decide) :
    i ≠ j ∧ S.τ (c i) = c j := byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hx:S.τ (c i) = c jhij:i ≠ j⊢ i ≠ j ∧ S.τ (c i) = c j
  apply And.intro hij hxAll goals completed! 🐙lemma contrT_congr {n : ℕ} {c : Fin (n + 1 + 1) → C}
    {i j : Fin (n + 1 + 1)} {hij : i ≠ j ∧ S.τ (c i) = c j}
    (i' j' : Fin (n + 1 + 1)) (t : S.Tensor c)
    (hii' : i = i' := by decide)
    (hjj' : j = j' := by decide) :
    contrT n i j hij t = permT id (And.intro (Function.bijective_id) (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c ji':Fin (n + 1 + 1)j':Fin (n + 1 + 1)t:S.Tensor chii':autoParam (i = i') contrT_congr._auto_1hjj':autoParam (j = j') contrT_congr._auto_2⊢ ∀ (i_1 : Fin n), (c ∘ i'.succSuccAbove j') (id i_1) = (c ∘ i.succSuccAbove j) i_1 subst hii' hjj'k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor c⊢ ∀ (i_1 : Fin n), (c ∘ i.succSuccAbove j) (id i_1) = (c ∘ i.succSuccAbove j) i_1; simpAll goals completed! 🐙))
      (contrT n i' j' (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c ji':Fin (n + 1 + 1)j':Fin (n + 1 + 1)t:S.Tensor chii':autoParam (i = i') contrT_congr._auto_1hjj':autoParam (j = j') contrT_congr._auto_2⊢ i' ≠ j' ∧ S.τ (c i') = c j' subst hii' hjj'k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor c⊢ i ≠ j ∧ S.τ (c i) = c j; exact hijAll goals completed! 🐙) t) := byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c ji':Fin (n + 1 + 1)j':Fin (n + 1 + 1)t:S.Tensor chii':i = i'hjj':j = j'⊢ (contrT n i j hij) t = (permT id ⋯) ((contrT n i' j' ⋯) t)
  subst hii' hjj'k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor c⊢ (contrT n i j hij) t = (permT id ⋯) ((contrT n i j ⋯) t)
  simpAll goals completed! 🐙@[simp]
lemma contrT_pure {n : ℕ} {c : Fin (n + 1 + 1) → C} (i j : Fin (n + 1 + 1))
    (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) :
    contrT n i j hij p.toTensor = p.contrP i j hij := byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S c⊢ (contrT n i j hij) p.toTensor = contrP i j hij p
  simp only [contrT, Pure.toTensor]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S c⊢ (PiTensorProduct.lift (contrPMultilinear i j hij)) ((PiTensorProduct.tprod k) p) = contrP i j hij p
  change _ = Pure.contrPMultilinear i j hij pk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S c⊢ (PiTensorProduct.lift (contrPMultilinear i j hij)) ((PiTensorProduct.tprod k) p) = (contrPMultilinear i j hij) p
  conv_rhs => rw [← PiTensorProduct.lift.tprod]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S c| (PiTensorProduct.lift (contrPMultilinear i j hij)) ((PiTensorProduct.tprod k) p)

@[simp]
lemma contrT_equivariant {n : ℕ} {c : Fin (n + 1 + 1) → C}
    (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) (g : G)
    (t : Tensor S c) :
    contrT n i j hij (g • t) = g • contrT n i j hij t := byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor c⊢ (contrT n i j hij) (g • t) = g • (contrT n i j hij) t
  let P (t : Tensor S c) : Prop := contrT n i j hij (g • t) = g • contrT n i j hij tk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) t⊢ (contrT n i j hij) (g • t) = g • (contrT n i j hij) t
  change P tk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) t⊢ P t
  apply induction_on_purehk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) t⊢ ∀ (p : Pure S c), P p.toTensorhsmulk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) t⊢ ∀ (r : k) (t : S.Tensor c), P t → P (r • t)haddk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) t⊢ ∀ (t1 t2 : S.Tensor c), P t1 → P t2 → P (t1 + t2)
  ·hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) t⊢ ∀ (p : Pure S c), P p.toTensor intro phk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) tp:Pure S c⊢ P p.toTensor
    simp only [contrT_pure, P]hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) tp:Pure S c⊢ (contrT n i j hij) (g • p.toTensor) = g • contrP i j hij p
    rw [actionT_pure,hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) tp:Pure S c⊢ (contrT n i j hij) (g • p).toTensor = g • contrP i j hij phk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) tp:Pure S c⊢ contrP i j hij (g • p) = g • contrP i j hij p contrT_purehk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) tp:Pure S c⊢ contrP i j hij (g • p) = g • contrP i j hij phk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) tp:Pure S c⊢ contrP i j hij (g • p) = g • contrP i j hij p]hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) tp:Pure S c⊢ contrP i j hij (g • p) = g • contrP i j hij p
    simp only [contrP, contrPCoeff_invariant, dropPair_equivariant, actionT_smul]hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) tp:Pure S c⊢ contrPCoeff i j hij p • (g • dropPair i j ⋯ p).toTensor = contrPCoeff i j hij p • g • (dropPair i j ⋯ p).toTensor
    congr 1h.e_ak:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) tp:Pure S c⊢ (g • dropPair i j ⋯ p).toTensor = g • (dropPair i j ⋯ p).toTensor
    exact Eq.symm actionT_pureAll goals completed! 🐙
  ·hsmulk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) t⊢ ∀ (r : k) (t : S.Tensor c), P t → P (r • t) intro p q hphsmulk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) tp:kq:S.Tensor chp:P q⊢ P (p • q)
    simp [P, hp]All goals completed! 🐙
  ·haddk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) t⊢ ∀ (t1 t2 : S.Tensor c), P t1 → P t2 → P (t1 + t2) intro p r hr hphaddk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jg:Gt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) (g • t) = g • (contrT n i j hij) tp:S.Tensor cr:S.Tensor chr:P php:P r⊢ P (p + r)
    simp [P, hp, hr]All goals completed! 🐙

lemma contrT_permT {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
    {c1 : Fin (n1 + 1 + 1) → C}
    (i j : Fin (n1 + 1 + 1)) (hij : i ≠ j ∧ S.τ (c1 i) = (c1 j))
    (σ : Fin (n1 + 1 + 1) → Fin (n + 1 + 1))
    (hσ : IsReindexing c c1 σ) (t : Tensor S c) :
    contrT n1 i j hij (permT σ hσ t) = permT _ (hσ.succSuccAbove i j hij.1)
      (contrT n (σ i) (σ j) (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor c⊢ σ i ≠ σ j ∧ S.τ (c (σ i)) = c (σ j) simp [hσ.2, hij, hσ.1.injective.eq_iff]All goals completed! 🐙) t) := byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor c⊢ (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)
  let P (t : Tensor S c) : Prop := contrT n1 i j hij (permT σ hσ t) =
      permT _ (hσ.succSuccAbove i j hij.1)
        (contrT n (σ i) (σ j) (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt✝:S.Tensor ct:S.Tensor c⊢ σ i ≠ σ j ∧ S.τ (c (σ i)) = c (σ j)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)⊢ (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t) simp [hσ.2, hij, hσ.1.injective.eq_iff]All goals completed! 🐙k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)⊢ (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)) t)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)⊢ (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)
  change P tk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)⊢ P t
  apply induction_on_purehk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)⊢ ∀ (p : Pure S c), P p.toTensorhsmulk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)⊢ ∀ (r : k) (t : S.Tensor c), P t → P (r • t)haddk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)⊢ ∀ (t1 t2 : S.Tensor c), P t1 → P t2 → P (t1 + t2)
  ·hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)⊢ ∀ (p : Pure S c), P p.toTensor intro phk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)p:Pure S c⊢ P p.toTensor
    simp only [contrT_pure, P]hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)p:Pure S c⊢ (contrT n1 i j hij) ((permT σ hσ) p.toTensor) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) (contrP (σ i) (σ j) ⋯ p)
    rw [permT_pure,hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)p:Pure S c⊢ (contrT n1 i j hij) (permP σ hσ p).toTensor = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) (contrP (σ i) (σ j) ⋯ p)hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)p:Pure S c⊢ contrP i j hij (permP σ hσ p) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) (contrP (σ i) (σ j) ⋯ p) contrT_purehk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)p:Pure S c⊢ contrP i j hij (permP σ hσ p) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) (contrP (σ i) (σ j) ⋯ p)hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)p:Pure S c⊢ contrP i j hij (permP σ hσ p) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) (contrP (σ i) (σ j) ⋯ p)]hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)p:Pure S c⊢ contrP i j hij (permP σ hσ p) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) (contrP (σ i) (σ j) ⋯ p)
    simp only [contrP, contrPCoeff_permP, dropPair_permP, map_smul]hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)p:Pure S c⊢ contrPCoeff (σ i) (σ j) ⋯ p • (permP (i.funPredPredAbove j ⋯ σ ⋯) ⋯ (dropPair (σ i) (σ j) ⋯ p)).toTensor =
  contrPCoeff (σ i) (σ j) ⋯ p • (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) (dropPair (σ i) (σ j) ⋯ p).toTensor
    congrh.e_ak:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)p:Pure S c⊢ (permP (i.funPredPredAbove j ⋯ σ ⋯) ⋯ (dropPair (σ i) (σ j) ⋯ p)).toTensor =
  (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) (dropPair (σ i) (σ j) ⋯ p).toTensor
    rw [permT_pureh.e_ak:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)p:Pure S c⊢ (permP (i.funPredPredAbove j ⋯ σ ⋯) ⋯ (dropPair (σ i) (σ j) ⋯ p)).toTensor =
  (permP (i.funPredPredAbove j ⋯ σ ⋯) ⋯ (dropPair (σ i) (σ j) ⋯ p)).toTensorAll goals completed! 🐙]All goals completed! 🐙
  ·hsmulk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)⊢ ∀ (r : k) (t : S.Tensor c), P t → P (r • t) intro r t hthsmulk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt✝:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)r:kt:S.Tensor cht:P t⊢ P (r • t)
    simp_all [P]All goals completed! 🐙
  ·haddk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)⊢ ∀ (t1 t2 : S.Tensor c), P t1 → P t2 → P (t1 + t2) intro t1 t2 ht1 ht2haddk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin (n1 + 1 + 1) → Ci:Fin (n1 + 1 + 1)j:Fin (n1 + 1 + 1)hij:i ≠ j ∧ S.τ (c1 i) = c1 jσ:Fin (n1 + 1 + 1) → Fin (n + 1 + 1)hσ:IsReindexing c c1 σt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n1 i j hij) ((permT σ hσ) t) = (permT (i.funPredPredAbove j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)t1:S.Tensor ct2:S.Tensor cht1:P t1ht2:P t2⊢ P (t1 + t2)
    simp_all [P]All goals completed! 🐙

lemma contrT_symm {n : ℕ} {c : Fin (n + 1 + 1) → C}
    {i j : Fin (n + 1 + 1)} {hij : i ≠ j ∧ S.τ (c i) = c j} (t : Tensor S c) :
    contrT n i j hij t = permT id (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor c⊢ IsReindexing (c ∘ j.succSuccAbove i) (c ∘ i.succSuccAbove j) id simpAll goals completed! 🐙)
      (contrT n j i ⟨hij.1.symm, byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor c⊢ S.τ (c j) = c i simp [← hij.2]All goals completed! 🐙⟩ t) := byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor c⊢ (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)
  let P (t : Tensor S c) : Prop := contrT n i j hij t = permT id (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt✝:S.Tensor ct:S.Tensor c⊢ IsReindexing (c ∘ j.succSuccAbove i) (c ∘ i.succSuccAbove j) idk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)⊢ (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t) simpAll goals completed! 🐙k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)⊢ (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t))
      (contrT n j i ⟨hij.1.symm, byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt✝:S.Tensor ct:S.Tensor c⊢ S.τ (c j) = c ik:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)⊢ (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t) simp [← hij.2]All goals completed! 🐙k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)⊢ (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)⟩ t)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)⊢ (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)
  change P tk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)⊢ P t
  apply induction_on_purehk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)⊢ ∀ (p : Pure S c), P p.toTensorhsmulk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)⊢ ∀ (r : k) (t : S.Tensor c), P t → P (r • t)haddk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)⊢ ∀ (t1 t2 : S.Tensor c), P t1 → P t2 → P (t1 + t2)
  ·hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)⊢ ∀ (p : Pure S c), P p.toTensor intro phk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)p:Pure S c⊢ P p.toTensor
    simp only [contrT_pure, P]hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)p:Pure S c⊢ contrP i j hij p = (permT id ⋯) (contrP j i ⋯ p)
    rw [contrP_symmhk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)p:Pure S c⊢ (permT id ⋯) (contrP j i ⋯ p) = (permT id ⋯) (contrP j i ⋯ p)All goals completed! 🐙]All goals completed! 🐙
  ·hsmulk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)⊢ ∀ (r : k) (t : S.Tensor c), P t → P (r • t) intro p q hphsmulk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)p:kq:S.Tensor chp:P q⊢ P (p • q)
    simp [P, hp]All goals completed! 🐙
  ·haddk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)⊢ ∀ (t1 t2 : S.Tensor c), P t1 → P t2 → P (t1 + t2) intro p r hr hphaddk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cP:S.Tensor c → Prop := fun t => (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)p:S.Tensor cr:S.Tensor chr:P php:P r⊢ P (p + r)
    simp [P, hp, hr]All goals completed! 🐙

lemma contrT_comm {n : ℕ} {c : Fin (n + 1 + 1 + 1 + 1) → C}
    (i1 j1 : Fin (n + 1 + 1 + 1 + 1)) (i2 j2 : Fin (n + 1 + 1))
    (hij1 : i1 ≠ j1 ∧ S.τ (c i1) = (c j1))
    (hij2 : i2 ≠ j2 ∧ S.τ (c (succSuccAbove i1 j1 i2)) = (c (succSuccAbove i1 j1 j2)))
    (t : Tensor S c) :
    let i2' := (succSuccAbove i1 j1 i2);
    let j2' := (succSuccAbove i1 j1 j2);
    have hi2j2' : i2' ≠ j2' := byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2⊢ i2' ≠ j2' simp [i2', j2', hij2]All goals completed! 🐙;
    let i1' := (predPredAbove i2' j2' hi2j2' i1 (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2hi2j2':i2' ≠ j2'⊢ i1 ≠ i2' ∧ i1 ≠ j2' simp [i2', j2']All goals completed! 🐙));
    let j1' := (predPredAbove i2' j2' hi2j2' j1 (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2hi2j2':i2' ≠ j2'i1':Fin (n + 2) := i2'.predPredAbove j2' hi2j2' i1 ⋯⊢ j1 ≠ i2' ∧ j1 ≠ j2' simp [i2', j2']All goals completed! 🐙));
    contrT n i2 j2 hij2 (contrT (n + 1 + 1) i1 j1 hij1 t) =
    permT id (IsReindexing.succSuccAbove_comm i1 j1 i2 j2 hij1.left hij2.left)
      (contrT n i1' j1' (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2hi2j2':i2' ≠ j2'i1':Fin (n + 2) := i2'.predPredAbove j2' hi2j2' i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' hi2j2' j1 ⋯⊢ i1' ≠ j1' ∧
  S.τ ((c ∘ (i1.succSuccAbove j1 i2).succSuccAbove (i1.succSuccAbove j1 j2)) i1') =
    (c ∘ (i1.succSuccAbove j1 i2).succSuccAbove (i1.succSuccAbove j1 j2)) j1' simp [i1', j1', i2', j2', hij1]All goals completed! 🐙)
      (contrT (n + 1 + 1) i2' j2' (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2hi2j2':i2' ≠ j2'i1':Fin (n + 2) := i2'.predPredAbove j2' hi2j2' i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' hi2j2' j1 ⋯⊢ i2' ≠ j2' ∧ S.τ (c i2') = c j2' simp [i2', j2', hij2]All goals completed! 🐙) t)) := byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor c⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))
  let i2' := (succSuccAbove i1 j1 i2)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t));
  let j2' := (succSuccAbove i1 j1 j2)k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t));
  let i1' := (predPredAbove i2' j2' (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2⊢ i2' ≠ j2'k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t)) simp [i2', j2', hij2]All goals completed! 🐙k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))) i1
    (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2⊢ i1 ≠ i2' ∧ i1 ≠ j2'k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t)) simp [i2', j2']All goals completed! 🐙k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t));
  let j1' := (predPredAbove i2' j2' (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯⊢ i2' ≠ j2'k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t)) simp [i2', j2', hij2]All goals completed! 🐙k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))) j1
    (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯⊢ j1 ≠ i2' ∧ j1 ≠ j2'k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t)) simp [i2', j2']All goals completed! 🐙k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t));
  let P (t : Tensor S c) : Prop := contrT n i2 j2 hij2 (contrT (n + 1 + 1) i1 j1 hij1 t) =
      permT id (IsReindexing.succSuccAbove_comm i1 j1 i2 j2 hij1.left hij2.left)
        (contrT n i1' j1' (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t✝:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯t:S.Tensor c⊢ i1' ≠ j1' ∧
  S.τ ((c ∘ (i1.succSuccAbove j1 i2).succSuccAbove (i1.succSuccAbove j1 j2)) i1') =
    (c ∘ (i1.succSuccAbove j1 i2).succSuccAbove (i1.succSuccAbove j1 j2)) j1'k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t)) simp [i1', j1', i2', j2', hij1]All goals completed! 🐙k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t)))
        (contrT (n + 1 + 1) i2' j2' (byk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t✝:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯t:S.Tensor c⊢ i2' ≠ j2' ∧ S.τ (c i2') = c j2'k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t)) simp [i2', j2', hij2]All goals completed! 🐙k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))) t))k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))⊢ let i2' := i1.succSuccAbove j1 i2;
let j2' := i1.succSuccAbove j1 j2;
have hi2j2' := ⋯;
let i1' := i2'.predPredAbove j2' hi2j2' i1 ⋯;
let j1' := i2'.predPredAbove j2' hi2j2' j1 ⋯;
(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))
  change P tk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))⊢ P t
  apply induction_on_purehk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))⊢ ∀ (p : Pure S c), P p.toTensorhsmulk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))⊢ ∀ (r : k) (t : S.Tensor c), P t → P (r • t)haddk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))⊢ ∀ (t1 t2 : S.Tensor c), P t1 → P t2 → P (t1 + t2)
  ·hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))⊢ ∀ (p : Pure S c), P p.toTensor intro phk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c⊢ P p.toTensor
    dsimp only [P]hk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c⊢ (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) p.toTensor) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) p.toTensor))
    conv_lhs => enter [2]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c| (contrT (n + 1 + 1) i1 j1 hij1) p.toTensor; rw [contrT_pure, contrP]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c| contrPCoeff i1 j1 hij1 p • (dropPair i1 j1 ⋯ p).toTensor
    conv_lhs => rw [map_smul, contrT_pure, contrP, smul_smul]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c| (contrPCoeff i1 j1 hij1 p * contrPCoeff i2 j2 hij2 (dropPair i1 j1 ⋯ p)) •
  (dropPair i2 j2 ⋯ (dropPair i1 j1 ⋯ p)).toTensor
    conv_rhs => enter [2, 2]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c| (contrT (n + 1 + 1) i2' j2' ⋯) p.toTensor; rw [contrT_pure, contrP]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c| contrPCoeff i2' j2' ⋯ p • (dropPair i2' j2' ⋯ p).toTensor
    conv_rhs => enter [2]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c| (contrT n i1' j1' ⋯) (contrPCoeff i2' j2' ⋯ p • (dropPair i2' j2' ⋯ p).toTensor); rw [map_smul]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c| contrPCoeff i2' j2' ⋯ p • (contrT n i1' j1' ⋯) (dropPair i2' j2' ⋯ p).toTensor
    conv_rhs => rw [map_smul]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c| contrPCoeff i2' j2' ⋯ p • (permT id ⋯) ((contrT n i1' j1' ⋯) (dropPair i2' j2' ⋯ p).toTensor)
    conv_rhs => enter [2, 2]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c| (contrT n i1' j1' ⋯) (dropPair i2' j2' ⋯ p).toTensor; rw [contrT_pure, contrP]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c| contrPCoeff i1' j1' ⋯ (dropPair i2' j2' ⋯ p) • (dropPair i1' j1' ⋯ (dropPair i2' j2' ⋯ p)).toTensor
    conv_rhs => enter [2]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c| (permT id ⋯) (contrPCoeff i1' j1' ⋯ (dropPair i2' j2' ⋯ p) • (dropPair i1' j1' ⋯ (dropPair i2' j2' ⋯ p)).toTensor); rw [map_smul, permT_pure]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c| contrPCoeff i1' j1' ⋯ (dropPair i2' j2' ⋯ p) • (permP id ⋯ (dropPair i1' j1' ⋯ (dropPair i2' j2' ⋯ p))).toTensor
    conv_rhs => rw [smul_smul]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c| (contrPCoeff i2' j2' ⋯ p * contrPCoeff i1' j1' ⋯ (dropPair i2' j2' ⋯ p)) •
  (permP id ⋯ (dropPair i1' j1' ⋯ (dropPair i2' j2' ⋯ p))).toTensor
    congr 1h.e_ak:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c⊢ contrPCoeff i1 j1 hij1 p * contrPCoeff i2 j2 hij2 (dropPair i1 j1 ⋯ p) =
  contrPCoeff i2' j2' ⋯ p * contrPCoeff i1' j1' ⋯ (dropPair i2' j2' ⋯ p)h.e_ak:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c⊢ (dropPair i2 j2 ⋯ (dropPair i1 j1 ⋯ p)).toTensor = (permP id ⋯ (dropPair i1' j1' ⋯ (dropPair i2' j2' ⋯ p))).toTensor
    ·h.e_ak:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c⊢ contrPCoeff i1 j1 hij1 p * contrPCoeff i2 j2 hij2 (dropPair i1 j1 ⋯ p) =
  contrPCoeff i2' j2' ⋯ p * contrPCoeff i1' j1' ⋯ (dropPair i2' j2' ⋯ p) exact contrPCoeff_mul_dropPair i1 j1 i2 j2 hij1 hij2 pAll goals completed! 🐙
    ·h.e_ak:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c⊢ (dropPair i2 j2 ⋯ (dropPair i1 j1 ⋯ p)).toTensor = (permP id ⋯ (dropPair i1' j1' ⋯ (dropPair i2' j2' ⋯ p))).toTensor congr 1h.e_ak:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c⊢ dropPair i2 j2 ⋯ (dropPair i1 j1 ⋯ p) = permP id ⋯ (dropPair i1' j1' ⋯ (dropPair i2' j2' ⋯ p))
      rw [dropPair_commh.e_ak:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:Pure S c⊢ permP id ⋯
    (dropPair ((i1.succSuccAbove j1 i2).predPredAbove (i1.succSuccAbove j1 j2) ⋯ i1 ⋯)
      ((i1.succSuccAbove j1 i2).predPredAbove (i1.succSuccAbove j1 j2) ⋯ j1 ⋯) ⋯
      (dropPair (i1.succSuccAbove j1 i2) (i1.succSuccAbove j1 j2) ⋯ p)) =
  permP id ⋯ (dropPair i1' j1' ⋯ (dropPair i2' j2' ⋯ p))All goals completed! 🐙]All goals completed! 🐙
  ·hsmulk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))⊢ ∀ (r : k) (t : S.Tensor c), P t → P (r • t) intro p q hphsmulk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:kq:S.Tensor chp:P q⊢ P (p • q)
    dsimp only [P] at hp ⊢hsmulk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:kq:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) q) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) q))⊢ (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) (p • q)) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) (p • q)))
    conv_lhs => rw [map_smul, map_smul, hp]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:kq:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) q) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) q))| p • (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) q))
    conv_rhs => enter [2, 2]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:kq:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) q) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) q))| (contrT (n + 1 + 1) i2' j2' ⋯) (p • q); rw [map_smul]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:kq:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) q) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) q))| p • (contrT (n + 1 + 1) i2' j2' ⋯) q
    conv_rhs => enter [2]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:kq:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) q) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) q))| (contrT n i1' j1' ⋯) (p • (contrT (n + 1 + 1) i2' j2' ⋯) q); rw [map_smul]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:kq:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) q) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) q))| p • (contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) q)
    conv_rhs => rw [map_smul]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:kq:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) q) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) q))| p • (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) q))
  ·haddk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))⊢ ∀ (t1 t2 : S.Tensor c), P t1 → P t2 → P (t1 + t2) intro p r hp hrhaddk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:S.Tensor cr:S.Tensor chp:P phr:P r⊢ P (p + r)
    dsimp only [P] at hp hr ⊢haddk:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:S.Tensor cr:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) p) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) p))hr:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) r) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) r))⊢ (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) (p + r)) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) (p + r)))
    conv_lhs => rw [map_add, map_add, hp]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:S.Tensor cr:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) p) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) p))hr:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) r) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) r))| (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) p)) +
  (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) r)
    conv_lhs => enter [2]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:S.Tensor cr:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) p) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) p))hr:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) r) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) r))| (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) r); rw [hr]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:S.Tensor cr:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) p) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) p))hr:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) r) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) r))| (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) r))
    conv_rhs => enter [2, 2]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:S.Tensor cr:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) p) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) p))hr:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) r) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) r))| (contrT (n + 1 + 1) i2' j2' ⋯) (p + r); rw [map_add]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:S.Tensor cr:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) p) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) p))hr:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) r) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) r))| (contrT (n + 1 + 1) i2' j2' ⋯) p + (contrT (n + 1 + 1) i2' j2' ⋯) r
    conv_rhs => enter [2]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:S.Tensor cr:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) p) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) p))hr:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) r) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) r))| (contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) p + (contrT (n + 1 + 1) i2' j2' ⋯) r); rw [map_add]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:S.Tensor cr:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) p) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) p))hr:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) r) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) r))| (contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) p) + (contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) r)
    conv_rhs => rw [map_add]k:Typeinst✝⁵:CommRing kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1 + 1 + 1) → Ci1:Fin (n + 1 + 1 + 1 + 1)j1:Fin (n + 1 + 1 + 1 + 1)i2:Fin (n + 1 + 1)j2:Fin (n + 1 + 1)hij1:i1 ≠ j1 ∧ S.τ (c i1) = c j1hij2:i2 ≠ j2 ∧ S.τ (c (i1.succSuccAbove j1 i2)) = c (i1.succSuccAbove j1 j2)t:S.Tensor ci2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 i2j2':Fin (n + 2 + 1 + 1) := i1.succSuccAbove j1 j2i1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ i1 ⋯j1':Fin (n + 2) := i2'.predPredAbove j2' ⋯ j1 ⋯P:S.Tensor c → Prop := 
  fun t =>
    (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) =
      (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))p:S.Tensor cr:S.Tensor chp:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) p) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) p))hr:(contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) r) =
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) r))| (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) p)) +
  (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) r))

Contractions on tensors

i. Overview

ii. Key results

iii. Related files

iv. Table of contents

v. References

A. Tensor contraction