Physlib.Relativity.Tensors.Contraction.Products

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.Basic
public import Physlib.Relativity.Tensors.Product

The interaction of contractions and products

@[expose] public sectionattribute [-simp] LinearEquiv.cast_apply

Products and contractions

              lemma Pure.contrPCoeff_natAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
    {c1 : Fin n1 → C}
    (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j)
    (p : Pure S c) (p1 : Pure S c1) :
    contrPCoeff (Fin.natAdd n1 i) (Fin.natAdd n1 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j) simp_all [Fin.ext_iff]All goals completed! 🐙) (p1.prodP p) = contrPCoeff i j hij p := 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ contrPCoeff (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p) = contrPCoeff i j hij p
  simp only [contrPCoeff, prodP_apply_natAdd]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ (S.contr (Fin.append c1 c (Fin.natAdd n1 i)))
    ((LinearEquiv.cast ⋯) (p i) ⊗ₜ[k] (LinearEquiv.cast ⋯) ((LinearEquiv.cast ⋯) (p j))) =
  (S.contr (c i)) (p i ⊗ₜ[k] (LinearEquiv.cast ⋯) (p j))
  generalize_proofs ha hb hc hd hek: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1ha:RingHomInvPair (RingHom.id k) (RingHom.id k)hb:c i = Fin.append c1 c (Fin.natAdd n1 i)hc:Fin.append c1 c (Fin.natAdd n1 j) = S.τ (Fin.append c1 c (Fin.natAdd n1 i))hd:c j = Fin.append c1 c (Fin.natAdd n1 j)he:c j = S.τ (c i)⊢ (S.contr (Fin.append c1 c (Fin.natAdd n1 i)))
    ((LinearEquiv.cast hb) (p i) ⊗ₜ[k] (LinearEquiv.cast hc) ((LinearEquiv.cast hd) (p j))) =
  (S.contr (c i)) (p i ⊗ₜ[k] (LinearEquiv.cast he) (p j))
  generalize p i = pi at *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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1ha:RingHomInvPair (RingHom.id k) (RingHom.id k)hb:c i = Fin.append c1 c (Fin.natAdd n1 i)hc:Fin.append c1 c (Fin.natAdd n1 j) = S.τ (Fin.append c1 c (Fin.natAdd n1 i))hd:c j = Fin.append c1 c (Fin.natAdd n1 j)he:c j = S.τ (c i)pi:V (c i)⊢ (S.contr (Fin.append c1 c (Fin.natAdd n1 i)))
    ((LinearEquiv.cast hb) pi ⊗ₜ[k] (LinearEquiv.cast hc) ((LinearEquiv.cast hd) (p j))) =
  (S.contr (c i)) (pi ⊗ₜ[k] (LinearEquiv.cast he) (p j))
  generalize p j = pj at *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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1ha:RingHomInvPair (RingHom.id k) (RingHom.id k)hb:c i = Fin.append c1 c (Fin.natAdd n1 i)hc:Fin.append c1 c (Fin.natAdd n1 j) = S.τ (Fin.append c1 c (Fin.natAdd n1 i))hd:c j = Fin.append c1 c (Fin.natAdd n1 j)he:c j = S.τ (c i)pi:V (c i)pj:V (c j)⊢ (S.contr (Fin.append c1 c (Fin.natAdd n1 i)))
    ((LinearEquiv.cast hb) pi ⊗ₜ[k] (LinearEquiv.cast hc) ((LinearEquiv.cast hd) pj)) =
  (S.contr (c i)) (pi ⊗ₜ[k] (LinearEquiv.cast he) pj)
  generalize c i = ci at *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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)p:Pure S cp1:Pure S c1ha:RingHomInvPair (RingHom.id k) (RingHom.id k)hc:Fin.append c1 c (Fin.natAdd n1 j) = S.τ (Fin.append c1 c (Fin.natAdd n1 i))hd:c j = Fin.append c1 c (Fin.natAdd n1 j)pj:V (c j)ci:Chij:i ≠ j ∧ S.τ ci = c jhb:ci = Fin.append c1 c (Fin.natAdd n1 i)he:c j = S.τ cipi:V ci⊢ (S.contr (Fin.append c1 c (Fin.natAdd n1 i)))
    ((LinearEquiv.cast hb) pi ⊗ₜ[k] (LinearEquiv.cast hc) ((LinearEquiv.cast hd) pj)) =
  (S.contr ci) (pi ⊗ₜ[k] (LinearEquiv.cast he) pj)
  generalize c j = cj at *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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)p:Pure S cp1:Pure S c1ha:RingHomInvPair (RingHom.id k) (RingHom.id k)hc:Fin.append c1 c (Fin.natAdd n1 j) = S.τ (Fin.append c1 c (Fin.natAdd n1 i))ci:Chb:ci = Fin.append c1 c (Fin.natAdd n1 i)pi:V cicj:Chd:cj = Fin.append c1 c (Fin.natAdd n1 j)pj:V cjhij:i ≠ j ∧ S.τ ci = cjhe:cj = S.τ ci⊢ (S.contr (Fin.append c1 c (Fin.natAdd n1 i)))
    ((LinearEquiv.cast hb) pi ⊗ₜ[k] (LinearEquiv.cast hc) ((LinearEquiv.cast hd) pj)) =
  (S.contr ci) (pi ⊗ₜ[k] (LinearEquiv.cast he) pj)
  subst hek: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)p:Pure S cp1:Pure S c1ha:RingHomInvPair (RingHom.id k) (RingHom.id k)hc:Fin.append c1 c (Fin.natAdd n1 j) = S.τ (Fin.append c1 c (Fin.natAdd n1 i))ci:Chb:ci = Fin.append c1 c (Fin.natAdd n1 i)pi:V cihd:S.τ ci = Fin.append c1 c (Fin.natAdd n1 j)pj:V (S.τ ci)hij:i ≠ j ∧ S.τ ci = S.τ ci⊢ (S.contr (Fin.append c1 c (Fin.natAdd n1 i)))
    ((LinearEquiv.cast hb) pi ⊗ₜ[k] (LinearEquiv.cast hc) ((LinearEquiv.cast hd) pj)) =
  (S.contr ci) (pi ⊗ₜ[k] (LinearEquiv.cast ⋯) pj)
  subst hbk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)p:Pure S cp1:Pure S c1ha:RingHomInvPair (RingHom.id k) (RingHom.id k)hc:Fin.append c1 c (Fin.natAdd n1 j) = S.τ (Fin.append c1 c (Fin.natAdd n1 i))pi:V (Fin.append c1 c (Fin.natAdd n1 i))hd:S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)pj:V (S.τ (Fin.append c1 c (Fin.natAdd n1 i)))hij:i ≠ j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = S.τ (Fin.append c1 c (Fin.natAdd n1 i))⊢ (S.contr (Fin.append c1 c (Fin.natAdd n1 i)))
    ((LinearEquiv.cast ⋯) pi ⊗ₜ[k] (LinearEquiv.cast hc) ((LinearEquiv.cast hd) pj)) =
  (S.contr (Fin.append c1 c (Fin.natAdd n1 i))) (pi ⊗ₜ[k] (LinearEquiv.cast ⋯) pj)
  simp [LinearEquiv.cast_apply]All goals completed! 🐙lemma Pure.contrPCoeff_castAdd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
    {c1 : Fin n1 → C}
    (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j)
    (p : Pure S c) (p1 : Pure S c1) :
    contrPCoeff (Fin.castAdd n1 i) (Fin.castAdd n1 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ Fin.castAdd n1 i ≠ Fin.castAdd n1 j ∧ S.τ (Fin.append c c1 (Fin.castAdd n1 i)) = Fin.append c c1 (Fin.castAdd n1 j) simp_all [Fin.ext_iff]All goals completed! 🐙) (p.prodP p1) = contrPCoeff i j hij p := 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ contrPCoeff (Fin.castAdd n1 i) (Fin.castAdd n1 j) ⋯ (p.prodP p1) = contrPCoeff i j hij p
  simp only [contrPCoeff, prodP_apply_castAdd]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ (S.contr (Fin.append c c1 (Fin.castAdd n1 i)))
    ((LinearEquiv.cast ⋯) (p i) ⊗ₜ[k] (LinearEquiv.cast ⋯) ((LinearEquiv.cast ⋯) (p j))) =
  (S.contr (c i)) (p i ⊗ₜ[k] (LinearEquiv.cast ⋯) (p j))
  generalize_proofs ha hb hc hd hek: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1ha:RingHomInvPair (RingHom.id k) (RingHom.id k)hb:c i = Fin.append c c1 (Fin.castAdd n1 i)hc:Fin.append c c1 (Fin.castAdd n1 j) = S.τ (Fin.append c c1 (Fin.castAdd n1 i))hd:c j = Fin.append c c1 (Fin.castAdd n1 j)he:c j = S.τ (c i)⊢ (S.contr (Fin.append c c1 (Fin.castAdd n1 i)))
    ((LinearEquiv.cast hb) (p i) ⊗ₜ[k] (LinearEquiv.cast hc) ((LinearEquiv.cast hd) (p j))) =
  (S.contr (c i)) (p i ⊗ₜ[k] (LinearEquiv.cast he) (p j))
  generalize p i = pi at *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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1ha:RingHomInvPair (RingHom.id k) (RingHom.id k)hb:c i = Fin.append c c1 (Fin.castAdd n1 i)hc:Fin.append c c1 (Fin.castAdd n1 j) = S.τ (Fin.append c c1 (Fin.castAdd n1 i))hd:c j = Fin.append c c1 (Fin.castAdd n1 j)he:c j = S.τ (c i)pi:V (c i)⊢ (S.contr (Fin.append c c1 (Fin.castAdd n1 i)))
    ((LinearEquiv.cast hb) pi ⊗ₜ[k] (LinearEquiv.cast hc) ((LinearEquiv.cast hd) (p j))) =
  (S.contr (c i)) (pi ⊗ₜ[k] (LinearEquiv.cast he) (p j))
  generalize p j = pj at *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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1ha:RingHomInvPair (RingHom.id k) (RingHom.id k)hb:c i = Fin.append c c1 (Fin.castAdd n1 i)hc:Fin.append c c1 (Fin.castAdd n1 j) = S.τ (Fin.append c c1 (Fin.castAdd n1 i))hd:c j = Fin.append c c1 (Fin.castAdd n1 j)he:c j = S.τ (c i)pi:V (c i)pj:V (c j)⊢ (S.contr (Fin.append c c1 (Fin.castAdd n1 i)))
    ((LinearEquiv.cast hb) pi ⊗ₜ[k] (LinearEquiv.cast hc) ((LinearEquiv.cast hd) pj)) =
  (S.contr (c i)) (pi ⊗ₜ[k] (LinearEquiv.cast he) pj)
  generalize c i = ci at *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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)p:Pure S cp1:Pure S c1ha:RingHomInvPair (RingHom.id k) (RingHom.id k)hc:Fin.append c c1 (Fin.castAdd n1 j) = S.τ (Fin.append c c1 (Fin.castAdd n1 i))hd:c j = Fin.append c c1 (Fin.castAdd n1 j)pj:V (c j)ci:Chij:i ≠ j ∧ S.τ ci = c jhb:ci = Fin.append c c1 (Fin.castAdd n1 i)he:c j = S.τ cipi:V ci⊢ (S.contr (Fin.append c c1 (Fin.castAdd n1 i)))
    ((LinearEquiv.cast hb) pi ⊗ₜ[k] (LinearEquiv.cast hc) ((LinearEquiv.cast hd) pj)) =
  (S.contr ci) (pi ⊗ₜ[k] (LinearEquiv.cast he) pj)
  generalize c j = cj at *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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)p:Pure S cp1:Pure S c1ha:RingHomInvPair (RingHom.id k) (RingHom.id k)hc:Fin.append c c1 (Fin.castAdd n1 j) = S.τ (Fin.append c c1 (Fin.castAdd n1 i))ci:Chb:ci = Fin.append c c1 (Fin.castAdd n1 i)pi:V cicj:Chd:cj = Fin.append c c1 (Fin.castAdd n1 j)pj:V cjhij:i ≠ j ∧ S.τ ci = cjhe:cj = S.τ ci⊢ (S.contr (Fin.append c c1 (Fin.castAdd n1 i)))
    ((LinearEquiv.cast hb) pi ⊗ₜ[k] (LinearEquiv.cast hc) ((LinearEquiv.cast hd) pj)) =
  (S.contr ci) (pi ⊗ₜ[k] (LinearEquiv.cast he) pj)
  subst hek: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)p:Pure S cp1:Pure S c1ha:RingHomInvPair (RingHom.id k) (RingHom.id k)hc:Fin.append c c1 (Fin.castAdd n1 j) = S.τ (Fin.append c c1 (Fin.castAdd n1 i))ci:Chb:ci = Fin.append c c1 (Fin.castAdd n1 i)pi:V cihd:S.τ ci = Fin.append c c1 (Fin.castAdd n1 j)pj:V (S.τ ci)hij:i ≠ j ∧ S.τ ci = S.τ ci⊢ (S.contr (Fin.append c c1 (Fin.castAdd n1 i)))
    ((LinearEquiv.cast hb) pi ⊗ₜ[k] (LinearEquiv.cast hc) ((LinearEquiv.cast hd) pj)) =
  (S.contr ci) (pi ⊗ₜ[k] (LinearEquiv.cast ⋯) pj)
  subst hbk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)p:Pure S cp1:Pure S c1ha:RingHomInvPair (RingHom.id k) (RingHom.id k)hc:Fin.append c c1 (Fin.castAdd n1 j) = S.τ (Fin.append c c1 (Fin.castAdd n1 i))pi:V (Fin.append c c1 (Fin.castAdd n1 i))hd:S.τ (Fin.append c c1 (Fin.castAdd n1 i)) = Fin.append c c1 (Fin.castAdd n1 j)pj:V (S.τ (Fin.append c c1 (Fin.castAdd n1 i)))hij:i ≠ j ∧ S.τ (Fin.append c c1 (Fin.castAdd n1 i)) = S.τ (Fin.append c c1 (Fin.castAdd n1 i))⊢ (S.contr (Fin.append c c1 (Fin.castAdd n1 i)))
    ((LinearEquiv.cast ⋯) pi ⊗ₜ[k] (LinearEquiv.cast hc) ((LinearEquiv.cast hd) pj)) =
  (S.contr (Fin.append c c1 (Fin.castAdd n1 i))) (pi ⊗ₜ[k] (LinearEquiv.cast ⋯) pj)
  simp [LinearEquiv.cast_apply]All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma Pure.prodP_dropPair {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
    {c1 : Fin n1 → C}
    (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j)
    (p : Pure S c) (p1 : Pure S c1) :
    p1.prodP (dropPair i j hij.1 p) = permP _ (IsReindexing.append_succSuccAbove_natAdd i j)
    (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ Fin.natAdd n1 i ≠ Fin.natAdd n1 j simp_all [Fin.ext_iff]All goals completed! 🐙) (p1.prodP p)) := 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ p1.prodP (dropPair i j ⋯ p) = permP id ⋯ (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p))
  ext xk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x:Fin (n1 + n)⊢ p1.prodP (dropPair i j ⋯ p) x = permP id ⋯ (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)) x
  obtain ⟨x, rfl⟩ := finSumFinEquiv.surjective xk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x:Fin n1 ⊕ Fin n⊢ p1.prodP (dropPair i j ⋯ p) (finSumFinEquiv x) =
  permP id ⋯ (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)) (finSumFinEquiv x)
  rw [prodP_apply_finSumFinEquivk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x:Fin n1 ⊕ Fin n⊢ (match x with
  | Sum.inl i_1 => (LinearEquiv.cast ⋯) (p1 i_1)
  | Sum.inr i_1 => (LinearEquiv.cast ⋯) (dropPair i j ⋯ p i_1)) =
  permP id ⋯ (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)) (finSumFinEquiv x)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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x:Fin n1 ⊕ Fin n⊢ (match x with
  | Sum.inl i_1 => (LinearEquiv.cast ⋯) (p1 i_1)
  | Sum.inr i_1 => (LinearEquiv.cast ⋯) (dropPair i j ⋯ p i_1)) =
  permP id ⋯ (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)) (finSumFinEquiv x)]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x:Fin n1 ⊕ Fin n⊢ (match x with
  | Sum.inl i_1 => (LinearEquiv.cast ⋯) (p1 i_1)
  | Sum.inr i_1 => (LinearEquiv.cast ⋯) (dropPair i j ⋯ p i_1)) =
  permP id ⋯ (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)) (finSumFinEquiv x)
  simp only [Function.comp_apply, finSumFinEquiv_apply_left, finSumFinEquiv_apply_right, dropPair,
    permP, Nat.add_eq, id_eq]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x:Fin n1 ⊕ Fin n⊢ (match x with
  | Sum.inl i_1 => (LinearEquiv.cast ⋯) (p1 i_1)
  | Sum.inr i_1 => (LinearEquiv.cast ⋯) (p (i.succSuccAbove j i_1))) =
  (LinearEquiv.cast ⋯) (p1.prodP p ((Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j) (finSumFinEquiv x)))
  match x with
  | Sum.inl x =>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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x✝:Fin n1 ⊕ Fin nx:Fin n1⊢ (match Sum.inl x with
  | Sum.inl i_1 => (LinearEquiv.cast ⋯) (p1 i_1)
  | Sum.inr i_1 => (LinearEquiv.cast ⋯) (p (i.succSuccAbove j i_1))) =
  (LinearEquiv.cast ⋯) (p1.prodP p ((Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j) (finSumFinEquiv (Sum.inl x))))
    simp only [finSumFinEquiv_apply_left]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x✝:Fin n1 ⊕ Fin nx:Fin n1⊢ (LinearEquiv.cast ⋯) (p1 x) =
  (LinearEquiv.cast ⋯) (p1.prodP p ((Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j) (Fin.castAdd n x)))
    rw [← congr_right (p1.prodP p) _ (Fin.castAdd (n + 1 + 1) x)
      (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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x✝:Fin n1 ⊕ Fin nx:Fin n1⊢ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j) (Fin.castAdd n x) = Fin.castAdd (n + 1 + 1) xk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x✝:Fin n1 ⊕ Fin nx:Fin n1⊢ (LinearEquiv.cast ⋯) (p1 x) = (LinearEquiv.cast ⋯) ((LinearEquiv.cast ⋯) (p1.prodP p (Fin.castAdd (n + 1 + 1) x))) rw [Fin.succSuccAbove_natAdd_apply_castAdd i jk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x✝:Fin n1 ⊕ Fin nx:Fin n1⊢ Fin.castAdd (n + 1 + 1) x = Fin.castAdd (n + 1 + 1) xAll 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x✝:Fin n1 ⊕ Fin nx:Fin n1⊢ (LinearEquiv.cast ⋯) (p1 x) = (LinearEquiv.cast ⋯) ((LinearEquiv.cast ⋯) (p1.prodP p (Fin.castAdd (n + 1 + 1) x)))]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x✝:Fin n1 ⊕ Fin nx:Fin n1⊢ (LinearEquiv.cast ⋯) (p1 x) = (LinearEquiv.cast ⋯) ((LinearEquiv.cast ⋯) (p1.prodP p (Fin.castAdd (n + 1 + 1) x))))]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x✝:Fin n1 ⊕ Fin nx:Fin n1⊢ (LinearEquiv.cast ⋯) (p1 x) = (LinearEquiv.cast ⋯) ((LinearEquiv.cast ⋯) (p1.prodP p (Fin.castAdd (n + 1 + 1) x)))
    simp [LinearEquiv.cast_apply]All goals completed! 🐙
  | Sum.inr m =>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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x:Fin n1 ⊕ Fin nm:Fin n⊢ (match Sum.inr m with
  | Sum.inl i_1 => (LinearEquiv.cast ⋯) (p1 i_1)
  | Sum.inr i_1 => (LinearEquiv.cast ⋯) (p (i.succSuccAbove j i_1))) =
  (LinearEquiv.cast ⋯) (p1.prodP p ((Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j) (finSumFinEquiv (Sum.inr m))))
    simp only [finSumFinEquiv_apply_right]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x:Fin n1 ⊕ Fin nm:Fin n⊢ (LinearEquiv.cast ⋯) (p (i.succSuccAbove j m)) =
  (LinearEquiv.cast ⋯) (p1.prodP p ((Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j) (Fin.natAdd n1 m)))
    rw [← congr_right (p1.prodP p) _ (Fin.natAdd n1 (i.succSuccAbove j m))
      (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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x:Fin n1 ⊕ Fin nm:Fin n⊢ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j) (Fin.natAdd n1 m) = Fin.natAdd n1 (i.succSuccAbove j m)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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x:Fin n1 ⊕ Fin nm:Fin n⊢ (LinearEquiv.cast ⋯) (p (i.succSuccAbove j m)) =
  (LinearEquiv.cast ⋯) ((LinearEquiv.cast ⋯) (p1.prodP p (Fin.natAdd n1 (i.succSuccAbove j m)))) rw [Fin.succSuccAbove_comm_natAdd i jk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x:Fin n1 ⊕ Fin nm:Fin n⊢ Fin.natAdd n1 (i.succSuccAbove j m) = Fin.natAdd n1 (i.succSuccAbove j m)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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x:Fin n1 ⊕ Fin nm:Fin n⊢ (LinearEquiv.cast ⋯) (p (i.succSuccAbove j m)) =
  (LinearEquiv.cast ⋯) ((LinearEquiv.cast ⋯) (p1.prodP p (Fin.natAdd n1 (i.succSuccAbove j m))))]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x:Fin n1 ⊕ Fin nm:Fin n⊢ (LinearEquiv.cast ⋯) (p (i.succSuccAbove j m)) =
  (LinearEquiv.cast ⋯) ((LinearEquiv.cast ⋯) (p1.prodP p (Fin.natAdd n1 (i.succSuccAbove j m)))))]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1x:Fin n1 ⊕ Fin nm:Fin n⊢ (LinearEquiv.cast ⋯) (p (i.succSuccAbove j m)) =
  (LinearEquiv.cast ⋯) ((LinearEquiv.cast ⋯) (p1.prodP p (Fin.natAdd n1 (i.succSuccAbove j m))))
    simp [LinearEquiv.cast_apply]All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma Pure.prodP_contrP_snd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
    {c1 : Fin n1 → C}
    (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j)
    (p : Pure S c) (p1 : Pure S c1) :
    prodT p1.toTensor (contrP i j hij p) =
    ((permT id (IsReindexing.append_succSuccAbove_natAdd i j)) <|
    contrP (Fin.natAdd n1 i) (Fin.natAdd n1 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j) simpa using hijAll goals completed! 🐙) <|
    prodP p1 p) := 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ (prodT p1.toTensor) (contrP i j hij p) = (permT id ⋯) (contrP (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p))
  simp only [contrP, map_smul, Nat.add_eq]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ contrPCoeff i j hij p • (prodT p1.toTensor) (dropPair i j ⋯ p).toTensor =
  (permT id ⋯)
    (contrPCoeff (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p) •
      (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)).toTensor)
  rw [contrPCoeff_natAdd i j hijk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ contrPCoeff i j hij p • (prodT p1.toTensor) (dropPair i j ⋯ p).toTensor =
  (permT id ⋯) (contrPCoeff i j hij p • (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)).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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ contrPCoeff i j hij p • (prodT p1.toTensor) (dropPair i j ⋯ p).toTensor =
  (permT id ⋯) (contrPCoeff i j hij p • (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)).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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ contrPCoeff i j hij p • (prodT p1.toTensor) (dropPair i j ⋯ p).toTensor =
  (permT id ⋯) (contrPCoeff i j hij p • (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)).toTensor)
  rw [prodT_purek: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ contrPCoeff i j hij p • (p1.prodP (dropPair i j ⋯ p)).toTensor =
  (permT id ⋯) (contrPCoeff i j hij p • (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)).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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ contrPCoeff i j hij p • (p1.prodP (dropPair i j ⋯ p)).toTensor =
  (permT id ⋯) (contrPCoeff i j hij p • (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)).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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ contrPCoeff i j hij p • (p1.prodP (dropPair i j ⋯ p)).toTensor =
  (permT id ⋯) (contrPCoeff i j hij p • (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)).toTensor)
  rw [prodP_dropPair _ _ hijk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ contrPCoeff i j hij p • (permP id ⋯ (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p))).toTensor =
  (permT id ⋯) (contrPCoeff i j hij p • (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)).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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ contrPCoeff i j hij p • (permP id ⋯ (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p))).toTensor =
  (permT id ⋯) (contrPCoeff i j hij p • (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)).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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1⊢ contrPCoeff i j hij p • (permP id ⋯ (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p))).toTensor =
  (permT id ⋯) (contrPCoeff i j hij p • (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)).toTensor)
  generalize_proofs ha hb hc hdk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1ha:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhb:Fin.natAdd n1 i ≠ Fin.natAdd n1 jhc:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhd:Fin.natAdd n1 i ≠ Fin.natAdd n1 j⊢ contrPCoeff i j hij p • (permP id ha (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) hb (p1.prodP p))).toTensor =
  (permT id hc) (contrPCoeff i j hij p • (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) hd (p1.prodP p)).toTensor)
  erw [map_smulk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1ha:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhb:Fin.natAdd n1 i ≠ Fin.natAdd n1 jhc:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhd:Fin.natAdd n1 i ≠ Fin.natAdd n1 j⊢ contrPCoeff i j hij p • (permP id ha (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) hb (p1.prodP p))).toTensor =
  contrPCoeff i j hij p • (permT id hc) (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) hd (p1.prodP p)).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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1ha:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhb:Fin.natAdd n1 i ≠ Fin.natAdd n1 jhc:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhd:Fin.natAdd n1 i ≠ Fin.natAdd n1 j⊢ contrPCoeff i j hij p • (permP id ha (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) hb (p1.prodP p))).toTensor =
  contrPCoeff i j hij p • (permT id hc) (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) hd (p1.prodP p)).toTensor
  congre_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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1ha:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhb:Fin.natAdd n1 i ≠ Fin.natAdd n1 jhc:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhd:Fin.natAdd n1 i ≠ Fin.natAdd n1 j⊢ (permP id ha (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) hb (p1.prodP p))).toTensor =
  (permT id hc) (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) hd (p1.prodP p)).toTensor
  erw [permT_puree_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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jp:Pure S cp1:Pure S c1ha:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhb:Fin.natAdd n1 i ≠ Fin.natAdd n1 jhc:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhd:Fin.natAdd n1 i ≠ Fin.natAdd n1 j⊢ (permP id ha (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) hb (p1.prodP p))).toTensor =
  (permP id hc (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) hd (p1.prodP p))).toTensor]All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma prodT_contrT_snd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
    {c1 : Fin n1 → C}
    (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j)
    (t : Tensor S c) (t1 : Tensor S c1) :
    prodT t1 (contrT n i j hij t) =
    ((permT id (IsReindexing.append_succSuccAbove_natAdd i j)) <|
    contrT _ (Fin.natAdd n1 i) (Fin.natAdd n1 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1⊢ Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j) simpa using hijAll goals completed! 🐙) <| prodT t1 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1⊢ (prodT t1) ((contrT n i j hij) t) =
  (permT id ⋯) ((contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯) ((prodT t1) t))
  generalize_proofs ha hb hc hdk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))⊢ (prodT t1) ((contrT n i j hij) t) =
  (permT id hb) ((contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) hc) ((prodT t1) t))
  let P (t : Tensor S c) (t1 : Tensor S c1) : Prop :=
    prodT t1 (contrT _ i j hij t) =
    ((permT id (IsReindexing.append_succSuccAbove_natAdd i j)) <|
    contrT _
      (finSumFinEquiv (m := n1) (Sum.inr i))
      (finSumFinEquiv (m := n1) (Sum.inr j)) hc <|
    prodT t1 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))⊢ (prodT t1) ((contrT n i j hij) t) =
  (permT id hb) ((contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) hc) ((prodT t1) t))
  let P1 (t : Tensor S c) := P t t1k: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1⊢ (prodT t1) ((contrT n i j hij) t) =
  (permT id hb) ((contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) hc) ((prodT t1) t))
  change P1 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1⊢ P1 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1⊢ ∀ (p : Pure S c), P1 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1⊢ ∀ (r : k) (t : S.Tensor c), P1 t → P1 (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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1⊢ ∀ (t1 t2 : S.Tensor c), P1 t1 → P1 t2 → P1 (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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1⊢ ∀ (p : Pure S c), P1 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S c⊢ P1 p.toTensor
    let P2 (t1 : Tensor S c1) := P p.toTensor t1hk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1⊢ P1 p.toTensor
    change P2 t1hk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1⊢ P2 t1
    apply induction_on_pureh.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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1⊢ ∀ (p : Pure S c1), P2 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1⊢ ∀ (r : k) (t : S.Tensor c1), P2 t → P2 (r • t)h.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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1⊢ ∀ (t1 t2 : S.Tensor c1), P2 t1 → P2 t2 → P2 (t1 + t2)
    ·h.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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1⊢ ∀ (p : Pure S c1), P2 p.toTensor intro p1h.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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1p1:Pure S c1⊢ P2 p1.toTensor
      simp only [Nat.add_eq, finSumFinEquiv_apply_right, contrT_pure, P2, P]h.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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1p1:Pure S c1⊢ (prodT p1.toTensor) (Pure.contrP i j hij p) =
  (permT id ⋯) ((contrT (n1 + n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) hc) ((prodT p1.toTensor) p.toTensor))
      rw [Pure.prodP_contrP_snd,h.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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1p1:Pure S c1⊢ (permT id ⋯) (Pure.contrP (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)) =
  (permT id ⋯) ((contrT (n1 + n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) hc) ((prodT p1.toTensor) p.toTensor))h.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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1p1:Pure S c1⊢ (permT id ⋯) (Pure.contrP (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)) =
  (permT id ⋯) (Pure.contrP (Fin.natAdd n1 i) (Fin.natAdd n1 j) hc (p1.prodP p)) prodT_pure,h.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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1p1:Pure S c1⊢ (permT id ⋯) (Pure.contrP (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)) =
  (permT id ⋯) ((contrT (n1 + n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) hc) (p1.prodP p).toTensor)h.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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1p1:Pure S c1⊢ (permT id ⋯) (Pure.contrP (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)) =
  (permT id ⋯) (Pure.contrP (Fin.natAdd n1 i) (Fin.natAdd n1 j) hc (p1.prodP p)) contrT_pureh.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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1p1:Pure S c1⊢ (permT id ⋯) (Pure.contrP (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)) =
  (permT id ⋯) (Pure.contrP (Fin.natAdd n1 i) (Fin.natAdd n1 j) hc (p1.prodP p))h.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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1p1:Pure S c1⊢ (permT id ⋯) (Pure.contrP (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)) =
  (permT id ⋯) (Pure.contrP (Fin.natAdd n1 i) (Fin.natAdd n1 j) hc (p1.prodP p))]h.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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1p1:Pure S c1⊢ (permT id ⋯) (Pure.contrP (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p)) =
  (permT id ⋯) (Pure.contrP (Fin.natAdd n1 i) (Fin.natAdd n1 j) hc (p1.prodP p))
      rflAll 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1⊢ ∀ (r : k) (t : S.Tensor c1), P2 t → P2 (r • t) intro r t h1hsmulk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt✝:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1r:kt:S.Tensor c1h1:P2 t⊢ P2 (r • t)
      simp_all only [map_smul, LinearMap.smul_apply, P2, P]All goals completed! 🐙
    ·h.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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1⊢ ∀ (t1 t2 : S.Tensor c1), P2 t1 → P2 t2 → P2 (t1 + t2) intro t1 t2 h1 h2h.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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1✝:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1p:Pure S cP2:S.Tensor c1 → Prop := fun t1 => P p.toTensor t1t1:S.Tensor c1t2:S.Tensor c1h1:P2 t1h2:P2 t2⊢ P2 (t1 + t2)
      simp_all only [map_add, LinearMap.add_apply, P2, P]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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1⊢ ∀ (r : k) (t : S.Tensor c), P1 t → P1 (r • t) intro r t h1hsmulk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt✝:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1r:kt:S.Tensor ch1:P1 t⊢ P1 (r • t)
    simp_all only [map_smul, P1, 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1⊢ ∀ (t1 t2 : S.Tensor c), P1 t1 → P1 t2 → P1 (t1 + t2) intro t1 t2 h1 h2haddk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1✝:S.Tensor c1ha:SMulCommClass k k (S.Tensor (Fin.append c1 (c ∘ i.succSuccAbove j)))hb:IsReindexing (Fin.append c1 c ∘ (Fin.natAdd n1 i).succSuccAbove (Fin.natAdd n1 j))
  (Fin.append c1 (c ∘ i.succSuccAbove j)) idhc:Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j)hd:SMulCommClass k k (S.Tensor (Fin.append c1 c))P:S.Tensor c → S.Tensor c1 → Prop := 
  fun t t1 =>
    (prodT t1) ((contrT n i j hij) t) =
      (permT id ⋯) ((contrT (n1.add n) (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)) hc) ((prodT t1) t))P1:S.Tensor c → Prop := fun t => P t t1t1:S.Tensor ct2:S.Tensor ch1:P1 t1h2:P1 t2⊢ P1 (t1 + t2)
    simp_all only [map_add, P1, P]All goals completed! 🐙

lemma contrT_prodT_snd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
    {c1 : Fin n1 → C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j)
    (t : Tensor S c) (t1 : Tensor S c1) :
    (contrT _ (i.natAdd n1) (j.natAdd n1) (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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1⊢ Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j) simpa using hijAll goals completed! 🐙) <| prodT t1 t) =
    ((permT id (IsReindexing.on_id_symm (IsReindexing.append_succSuccAbove_natAdd i j))) <|
      (prodT t1 (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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1⊢ (contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯) ((prodT t1) t) =
  (permT id ⋯) ((prodT t1) ((contrT n i j hij) t))
  rw [prodT_contrT_sndk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1⊢ (contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯) ((prodT t1) t) =
  (permT id ⋯) ((permT id ⋯) ((contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯) ((prodT t1) 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1⊢ (contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯) ((prodT t1) t) =
  (permT id ⋯) ((permT id ⋯) ((contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯) ((prodT t1) 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1⊢ (contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯) ((prodT t1) t) =
  (permT id ⋯) ((permT id ⋯) ((contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯) ((prodT t1) t)))
  simpAll goals completed! 🐙

A contraction internal to the left factor commutes past the outer product with a right spectator. The mirror of prodT_contrT_snd, obtained from it by prodT_swap, so the right-hand side contracts the swapped product prodT t1 t and carries a block swap.


lemma prodT_contrT_fst {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
    {c1 : Fin n1 → C}
    (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j)
    (t : Tensor S c) (t1 : Tensor S c1) :
    prodT (contrT n i j hij t) t1 =
    permT _ IsReindexing.append_swap
      (permT id (IsReindexing.append_succSuccAbove_natAdd i j) <|
      contrT _
        (Fin.natAdd n1 i)
        (Fin.natAdd n1 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1⊢ Fin.natAdd n1 i ≠ Fin.natAdd n1 j ∧ S.τ (Fin.append c1 c (Fin.natAdd n1 i)) = Fin.append c1 c (Fin.natAdd n1 j) simpa using hijAll goals completed! 🐙) <|
      prodT t1 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1⊢ (prodT ((contrT n i j hij) t)) t1 =
  (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯)
    ((permT id ⋯) ((contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯) ((prodT t1) t)))
  rw [prodT_swap,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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1⊢ (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯) ((prodT t1) ((contrT n i j hij) t)) =
  (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯)
    ((permT id ⋯) ((contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯) ((prodT t1) t)))All goals completed! 🐙 prodT_contrT_sndk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕn1:ℕc:Fin (n + 1 + 1) → Cc1:Fin n1 → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor ct1:S.Tensor c1⊢ (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯)
    ((permT id ⋯) ((contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯) ((prodT t1) t))) =
  (permT (Fin.append (Fin.natAdd n1) (Fin.castAdd n)) ⋯)
    ((permT id ⋯) ((contrT (n1.add n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯) ((prodT t1) t)))All goals completed! 🐙]All goals completed! 🐙