awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
x : W
x_1 : V
⊢ Eq (α := TensorProduct A W V)
    (((((TensorProduct.AlgebraTensorModule.curry (rTensor ρ (id σ)).toLinearMap : W →ₗ[A] V →ₗ[A] TensorProduct A W V) :
                (a : W) → V →ₗ[A] TensorProduct A W V)
              x :
            V →ₗ[A] TensorProduct A W V) :
          (a : V) → TensorProduct A W V)
        x_1 :
      TensorProduct A W V)
    (((((TensorProduct.AlgebraTensorModule.curry (id (σ.tprod ρ)).toLinearMap : W →ₗ[A] V →ₗ[A] TensorProduct A W V) :
                (a : W) → V →ₗ[A] TensorProduct A W V)
              x :
            V →ₗ[A] TensorProduct A W V) :
          (a : V) → TensorProduct A W V)
        x_1 :
      TensorProduct A W V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
h :
  ∀ (x : W) (x_1 : V),
    Eq (α := TensorProduct A U V)
      (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (ρ := σ.tprod ρ) (σ := τ.tprod ρ) (rTensor ρ 0)) :
                    W →ₗ[A] V →ₗ[A] TensorProduct A U V) :
                  (a : W) → V →ₗ[A] TensorProduct A U V)
                x :
              V →ₗ[A] TensorProduct A U V) :
            (a : V) → TensorProduct A U V)
          x_1 :
        TensorProduct A U V)
      (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (G := G) (ρ := σ.tprod ρ) (σ := τ.tprod ρ) 0) :
                    W →ₗ[A] V →ₗ[A] TensorProduct A U V) :
                  (a : W) → V →ₗ[A] TensorProduct A U V)
                x :
              V →ₗ[A] TensorProduct A U V) :
            (a : V) → TensorProduct A U V)
          x_1 :
        TensorProduct A U V)
⊢ Eq (α := (σ.tprod ρ).IntertwiningMap (τ.tprod ρ)) (rTensor ρ 0) 0

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
x : W
x_1 : V
⊢ Eq (α := TensorProduct A U V)
    (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (ρ := σ.tprod ρ) (σ := τ.tprod ρ) (rTensor ρ 0)) :
                  W →ₗ[A] V →ₗ[A] TensorProduct A U V) :
                (a : W) → V →ₗ[A] TensorProduct A U V)
              x :
            V →ₗ[A] TensorProduct A U V) :
          (a : V) → TensorProduct A U V)
        x_1 :
      TensorProduct A U V)
    (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (G := G) (ρ := σ.tprod ρ) (σ := τ.tprod ρ) 0) :
                  W →ₗ[A] V →ₗ[A] TensorProduct A U V) :
                (a : W) → V →ₗ[A] TensorProduct A U V)
              x :
            V →ₗ[A] TensorProduct A U V) :
          (a : V) → TensorProduct A U V)
        x_1 :
      TensorProduct A U V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f₁ f₂ : σ.IntertwiningMap τ
⊢ rTensor ρ (f₁ + f₂) = rTensor ρ f₁ + rTensor ρ f₂

Tactic:
tensor_add_left _ _ _

Premises used: Representation.IntertwiningMap.tensor_add_left, Representation.IntertwiningMap.rTensor
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
a : A
f : σ.IntertwiningMap τ
⊢ rTensor ρ (a • f) = a • rTensor ρ f

Tactic:
tensor_smul_left _ _ _

Premises used: Representation.IntertwiningMap.tensor_smul_left, Representation.IntertwiningMap.rTensor
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
Q : Type u_7
inst_8 : AddCommMonoid Q
inst_9 : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
h :
  ∀ (x : V) (x_1 : W),
    Eq (α := TensorProduct A U Q)
      (((((TensorProduct.AlgebraTensorModule.curry ((rTensor υ f).comp (lTensor ρ g)).toLinearMap :
                    V →ₗ[A] W →ₗ[A] TensorProduct A U Q) :
                  (a : V) → W →ₗ[A] TensorProduct A U Q)
                x :
              W →ₗ[A] TensorProduct A U Q) :
            (a : W) → TensorProduct A U Q)
          x_1 :
        TensorProduct A U Q)
      (((((TensorProduct.AlgebraTensorModule.curry (f.tensor g).toLinearMap : V →ₗ[A] W →ₗ[A] TensorProduct A U Q) :
                  (a : V) → W →ₗ[A] TensorProduct A U Q)
                x :
              W →ₗ[A] TensorProduct A U Q) :
            (a : W) → TensorProduct A U Q)
          x_1 :
        TensorProduct A U Q)
⊢ (rTensor υ f).comp (lTensor ρ g) = f.tensor g

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
Q : Type u_7
inst_8 : AddCommMonoid Q
inst_9 : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
x : V
x_1 : W
⊢ Eq (α := TensorProduct A U Q)
    (((((TensorProduct.AlgebraTensorModule.curry ((rTensor υ f).comp (lTensor ρ g)).toLinearMap :
                  V →ₗ[A] W →ₗ[A] TensorProduct A U Q) :
                (a : V) → W →ₗ[A] TensorProduct A U Q)
              x :
            W →ₗ[A] TensorProduct A U Q) :
          (a : W) → TensorProduct A U Q)
        x_1 :
      TensorProduct A U Q)
    (((((TensorProduct.AlgebraTensorModule.curry (f.tensor g).toLinearMap : V →ₗ[A] W →ₗ[A] TensorProduct A U Q) :
                (a : V) → W →ₗ[A] TensorProduct A U Q)
              x :
            W →ₗ[A] TensorProduct A U Q) :
          (a : W) → TensorProduct A U Q)
        x_1 :
      TensorProduct A U Q)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
Q : Type u_7
inst_8 : AddCommMonoid Q
inst_9 : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
h :
  ∀ (x : V) (x_1 : W),
    Eq (α := TensorProduct A U Q)
      (((((TensorProduct.AlgebraTensorModule.curry ((lTensor τ g).comp (rTensor σ f)).toLinearMap :
                    V →ₗ[A] W →ₗ[A] TensorProduct A U Q) :
                  (a : V) → W →ₗ[A] TensorProduct A U Q)
                x :
              W →ₗ[A] TensorProduct A U Q) :
            (a : W) → TensorProduct A U Q)
          x_1 :
        TensorProduct A U Q)
      (((((TensorProduct.AlgebraTensorModule.curry (f.tensor g).toLinearMap : V →ₗ[A] W →ₗ[A] TensorProduct A U Q) :
                  (a : V) → W →ₗ[A] TensorProduct A U Q)
                x :
              W →ₗ[A] TensorProduct A U Q) :
            (a : W) → TensorProduct A U Q)
          x_1 :
        TensorProduct A U Q)
⊢ (lTensor τ g).comp (rTensor σ f) = f.tensor g

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
Q : Type u_7
inst_8 : AddCommMonoid Q
inst_9 : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
x : V
x_1 : W
⊢ Eq (α := TensorProduct A U Q)
    (((((TensorProduct.AlgebraTensorModule.curry ((lTensor τ g).comp (rTensor σ f)).toLinearMap :
                  V →ₗ[A] W →ₗ[A] TensorProduct A U Q) :
                (a : V) → W →ₗ[A] TensorProduct A U Q)
              x :
            W →ₗ[A] TensorProduct A U Q) :
          (a : W) → TensorProduct A U Q)
        x_1 :
      TensorProduct A U Q)
    (((((TensorProduct.AlgebraTensorModule.curry (f.tensor g).toLinearMap : V →ₗ[A] W →ₗ[A] TensorProduct A U Q) :
                (a : V) → W →ₗ[A] TensorProduct A U Q)
              x :
            W →ₗ[A] TensorProduct A U Q) :
          (a : W) → TensorProduct A U Q)
        x_1 :
      TensorProduct A U Q)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
a :
  ∀ (x : V) (x_1 : W),
    Eq (α := TensorProduct A W V)
      (((((TensorProduct.AlgebraTensorModule.curry
                      ((↑(_root_.TensorProduct.comm A V W) : TensorProduct A V W →ₗ[A] TensorProduct A W V) ∘ₗ
                        (ρ.tprod σ : (a : G) → TensorProduct A V W →ₗ[A] TensorProduct A V W) g) :
                    V →ₗ[A] W →ₗ[A] TensorProduct A W V) :
                  (a : V) → W →ₗ[A] TensorProduct A W V)
                x :
              W →ₗ[A] TensorProduct A W V) :
            (a : W) → TensorProduct A W V)
          x_1 :
        TensorProduct A W V)
      (((((TensorProduct.AlgebraTensorModule.curry
                      ((σ.tprod ρ : (a : G) → TensorProduct A W V →ₗ[A] TensorProduct A W V) g ∘ₗ
                        (↑(_root_.TensorProduct.comm A V W) : TensorProduct A V W →ₗ[A] TensorProduct A W V)) :
                    V →ₗ[A] W →ₗ[A] TensorProduct A W V) :
                  (a : V) → W →ₗ[A] TensorProduct A W V)
                x :
              W →ₗ[A] TensorProduct A W V) :
            (a : W) → TensorProduct A W V)
          x_1 :
        TensorProduct A W V)
⊢ Eq (α := TensorProduct A V W →ₗ[A] TensorProduct A W V)
    ((↑(_root_.TensorProduct.comm A V W) : TensorProduct A V W →ₗ[A] TensorProduct A W V) ∘ₗ
      (ρ.tprod σ : (a : G) → TensorProduct A V W →ₗ[A] TensorProduct A V W) g)
    ((σ.tprod ρ : (a : G) → TensorProduct A W V →ₗ[A] TensorProduct A W V) g ∘ₗ
      (↑(_root_.TensorProduct.comm A V W) : TensorProduct A V W →ₗ[A] TensorProduct A W V))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
x : V
x_1 : W
⊢ Eq (α := TensorProduct A W V)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((↑(_root_.TensorProduct.comm A V W) : TensorProduct A V W →ₗ[A] TensorProduct A W V) ∘ₗ
                      (ρ.tprod σ : (a : G) → TensorProduct A V W →ₗ[A] TensorProduct A V W) g) :
                  V →ₗ[A] W →ₗ[A] TensorProduct A W V) :
                (a : V) → W →ₗ[A] TensorProduct A W V)
              x :
            W →ₗ[A] TensorProduct A W V) :
          (a : W) → TensorProduct A W V)
        x_1 :
      TensorProduct A W V)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((σ.tprod ρ : (a : G) → TensorProduct A W V →ₗ[A] TensorProduct A W V) g ∘ₗ
                      (↑(_root_.TensorProduct.comm A V W) : TensorProduct A V W →ₗ[A] TensorProduct A W V)) :
                  V →ₗ[A] W →ₗ[A] TensorProduct A W V) :
                (a : V) → W →ₗ[A] TensorProduct A W V)
              x :
            W →ₗ[A] TensorProduct A W V) :
          (a : W) → TensorProduct A W V)
        x_1 :
      TensorProduct A W V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
⊢ (↑(comm ρ σ) : (ρ.tprod σ).IntertwiningMap (σ.tprod ρ)).toLinearMap =
    (↑(_root_.TensorProduct.comm A V W) : TensorProduct A V W →ₗ[A] TensorProduct A W V)

Tactic:
rfl

Premises used: TensorProduct.lift, rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
v : V
w : W
⊢ Eq (α := TensorProduct A W V)
    ((comm ρ σ : (a : TensorProduct A V W) → TensorProduct A W V) (v ⊗ₜ[A] w) : TensorProduct A W V)
    (w ⊗ₜ[A] v : TensorProduct A W V)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
h :
  ∀ (x : V) (x_1 : W),
    Eq (α := TensorProduct A U V)
      (((((TensorProduct.AlgebraTensorModule.curry
                      ((↑(comm ρ τ) : (ρ.tprod τ).IntertwiningMap (τ.tprod ρ)).comp
                          (IntertwiningMap.lTensor ρ f)).toLinearMap :
                    V →ₗ[A] W →ₗ[A] TensorProduct A U V) :
                  (a : V) → W →ₗ[A] TensorProduct A U V)
                x :
              W →ₗ[A] TensorProduct A U V) :
            (a : W) → TensorProduct A U V)
          x_1 :
        TensorProduct A U V)
      (((((TensorProduct.AlgebraTensorModule.curry
                      ((IntertwiningMap.rTensor ρ f).comp
                          (↑(comm ρ σ) : (ρ.tprod σ).IntertwiningMap (σ.tprod ρ))).toLinearMap :
                    V →ₗ[A] W →ₗ[A] TensorProduct A U V) :
                  (a : V) → W →ₗ[A] TensorProduct A U V)
                x :
              W →ₗ[A] TensorProduct A U V) :
            (a : W) → TensorProduct A U V)
          x_1 :
        TensorProduct A U V)
⊢ (↑(comm ρ τ) : (ρ.tprod τ).IntertwiningMap (τ.tprod ρ)).comp (IntertwiningMap.lTensor ρ f) =
    (IntertwiningMap.rTensor ρ f).comp (↑(comm ρ σ) : (ρ.tprod σ).IntertwiningMap (σ.tprod ρ))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
x : V
x_1 : W
⊢ Eq (α := TensorProduct A U V)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((↑(comm ρ τ) : (ρ.tprod τ).IntertwiningMap (τ.tprod ρ)).comp
                        (IntertwiningMap.lTensor ρ f)).toLinearMap :
                  V →ₗ[A] W →ₗ[A] TensorProduct A U V) :
                (a : V) → W →ₗ[A] TensorProduct A U V)
              x :
            W →ₗ[A] TensorProduct A U V) :
          (a : W) → TensorProduct A U V)
        x_1 :
      TensorProduct A U V)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((IntertwiningMap.rTensor ρ f).comp
                        (↑(comm ρ σ) : (ρ.tprod σ).IntertwiningMap (σ.tprod ρ))).toLinearMap :
                  V →ₗ[A] W →ₗ[A] TensorProduct A U V) :
                (a : V) → W →ₗ[A] TensorProduct A U V)
              x :
            W →ₗ[A] TensorProduct A U V) :
          (a : W) → TensorProduct A U V)
        x_1 :
      TensorProduct A U V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
h :
  ∀ (x : W) (x_1 : V),
    Eq (α := TensorProduct A V U)
      (((((TensorProduct.AlgebraTensorModule.curry
                      ((↑(comm τ ρ) : (τ.tprod ρ).IntertwiningMap (ρ.tprod τ)).comp
                          (IntertwiningMap.rTensor ρ f)).toLinearMap :
                    W →ₗ[A] V →ₗ[A] TensorProduct A V U) :
                  (a : W) → V →ₗ[A] TensorProduct A V U)
                x :
              V →ₗ[A] TensorProduct A V U) :
            (a : V) → TensorProduct A V U)
          x_1 :
        TensorProduct A V U)
      (((((TensorProduct.AlgebraTensorModule.curry
                      ((IntertwiningMap.lTensor ρ f).comp
                          (↑(comm σ ρ) : (σ.tprod ρ).IntertwiningMap (ρ.tprod σ))).toLinearMap :
                    W →ₗ[A] V →ₗ[A] TensorProduct A V U) :
                  (a : W) → V →ₗ[A] TensorProduct A V U)
                x :
              V →ₗ[A] TensorProduct A V U) :
            (a : V) → TensorProduct A V U)
          x_1 :
        TensorProduct A V U)
⊢ (↑(comm τ ρ) : (τ.tprod ρ).IntertwiningMap (ρ.tprod τ)).comp (IntertwiningMap.rTensor ρ f) =
    (IntertwiningMap.lTensor ρ f).comp (↑(comm σ ρ) : (σ.tprod ρ).IntertwiningMap (ρ.tprod σ))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
x : W
x_1 : V
⊢ Eq (α := TensorProduct A V U)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((↑(comm τ ρ) : (τ.tprod ρ).IntertwiningMap (ρ.tprod τ)).comp
                        (IntertwiningMap.rTensor ρ f)).toLinearMap :
                  W →ₗ[A] V →ₗ[A] TensorProduct A V U) :
                (a : W) → V →ₗ[A] TensorProduct A V U)
              x :
            V →ₗ[A] TensorProduct A V U) :
          (a : V) → TensorProduct A V U)
        x_1 :
      TensorProduct A V U)
    (((((TensorProduct.AlgebraTensorModule.curry
                    ((IntertwiningMap.lTensor ρ f).comp
                        (↑(comm σ ρ) : (σ.tprod ρ).IntertwiningMap (ρ.tprod σ))).toLinearMap :
                  W →ₗ[A] V →ₗ[A] TensorProduct A V U) :
                (a : W) → V →ₗ[A] TensorProduct A V U)
              x :
            V →ₗ[A] TensorProduct A V U) :
          (a : V) → TensorProduct A V U)
        x_1 :
      TensorProduct A V U)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : Module A V
inst_5 : Module A W
ρ : Representation A G V
σ : Representation A G W
⊢ (comm σ ρ).symm = comm ρ σ

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
x : V
x_1 : W
x_2 : U
⊢ Eq (α := TensorProduct A V (TensorProduct A W U))
    (((((((TensorProduct.AlgebraTensorModule.curry
                          (TensorProduct.AlgebraTensorModule.curry
                            ((↑(_root_.TensorProduct.assoc A V W U) :
                                TensorProduct A (TensorProduct A V W) U →ₗ[A]
                                  TensorProduct A V (TensorProduct A W U)) ∘ₗ
                              ((ρ.tprod σ).tprod τ :
                                  (a : G) →
                                    TensorProduct A (TensorProduct A V W) U →ₗ[A]
                                      TensorProduct A (TensorProduct A V W) U)
                                g)) :
                        V →ₗ[A] W →ₗ[A] U →ₗ[A] TensorProduct A V (TensorProduct A W U)) :
                      (a : V) → W →ₗ[A] U →ₗ[A] TensorProduct A V (TensorProduct A W U))
                    x :
                  W →ₗ[A] U →ₗ[A] TensorProduct A V (TensorProduct A W U)) :
                (a : W) → U →ₗ[A] TensorProduct A V (TensorProduct A W U))
              x_1 :
            U →ₗ[A] TensorProduct A V (TensorProduct A W U)) :
          (a : U) → TensorProduct A V (TensorProduct A W U))
        x_2 :
      TensorProduct A V (TensorProduct A W U))
    (((((((TensorProduct.AlgebraTensorModule.curry
                          (TensorProduct.AlgebraTensorModule.curry
                            ((ρ.tprod (σ.tprod τ) :
                                  (a : G) →
                                    TensorProduct A V (TensorProduct A W U) →ₗ[A]
                                      TensorProduct A V (TensorProduct A W U))
                                g ∘ₗ
                              (↑(_root_.TensorProduct.assoc A V W U) :
                                TensorProduct A (TensorProduct A V W) U →ₗ[A]
                                  TensorProduct A V (TensorProduct A W U)))) :
                        V →ₗ[A] W →ₗ[A] U →ₗ[A] TensorProduct A V (TensorProduct A W U)) :
                      (a : V) → W →ₗ[A] U →ₗ[A] TensorProduct A V (TensorProduct A W U))
                    x :
                  W →ₗ[A] U →ₗ[A] TensorProduct A V (TensorProduct A W U)) :
                (a : W) → U →ₗ[A] TensorProduct A V (TensorProduct A W U))
              x_1 :
            U →ₗ[A] TensorProduct A V (TensorProduct A W U)) :
          (a : U) → TensorProduct A V (TensorProduct A W U))
        x_2 :
      TensorProduct A V (TensorProduct A W U))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Intertwining
Goal:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : AddCommMonoid W
inst_4 : AddCommMonoid U
inst_5 : Module A V
inst_6 : Module A W
inst_7 : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
⊢ (↑(assoc ρ σ τ) : ((ρ.tprod σ).tprod τ).IntertwiningMap (ρ.tprod (σ.tprod τ))).toLinearMap =
    (↑(_root_.TensorProduct.assoc A V W U) :
      TensorProduct A (TensorProduct A V W) U →ₗ[A] TensorProduct A V (TensorProduct A W U))

Tactic:
rfl

Premises used: TensorProduct.lift, rfl