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
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_1 : V →ₗ[A] W
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x : G
rw :
  TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ
      TensorProduct.map ((ρ : (a : G) → V →ₗ[A] V) x) ((τ : (a : G) → U →ₗ[A] U) x) =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
rw₁ :
  TensorProduct.map (f.toLinearMap ∘ₗ (ρ : (a : G) → V →ₗ[A] V) x) (g.toLinearMap ∘ₗ (τ : (a : G) → U →ₗ[A] U) x) =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap
rw₂ :
  Eq (α := TensorProduct A V U →ₗ[A] TensorProduct A W P)
    (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x ∘ₗ f.toLinearMap) (g.toLinearMap ∘ₗ (τ : (a : G) → U →ₗ[A] U) x))
    ((σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap)
rw₃ :
  Eq (α := TensorProduct A V U →ₗ[A] TensorProduct A W P)
    (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x ∘ₗ f.toLinearMap) ((π : (a : G) → P →ₗ[A] P) x ∘ₗ g.toLinearMap))
    ((σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap)
rw₄ :
  Eq (α := TensorProduct A V U →ₗ[A] TensorProduct A W P)
    (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x) ((π : (a : G) → P →ₗ[A] P) x) ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap)
    ((σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap)
rw₅ rw₆ :
  Eq (α := TensorProduct A V U →ₗ[A] TensorProduct A W P)
    (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x) ((π : (a : G) → P →ₗ[A] P) x) ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap)
    (TensorProduct.map ((σ : (a : G) → W →ₗ[A] W) x) ((π : (a : G) → P →ₗ[A] P) x) ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap)
⊢ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ
      (ρ.tprod τ : (a : G) → TensorProduct A V U →ₗ[A] TensorProduct A V U) x =
    (σ.tprod π : (a : G) → TensorProduct A W P →ₗ[A] TensorProduct A W P) x ∘ₗ
      TensorProduct.map f.toLinearMap g.toLinearMap

Tactic:
rw [tprod_apply, ← TensorProduct.map_comp, f.2, g.2, TensorProduct.map_comp, tprod_apply]

Premises used: Representation.tprod_apply, TensorProduct.map_comp, Representation.IntertwiningMap.isIntertwining'
-- 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
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
⊢ (f.tensor g).toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap

Tactic:
rfl

Premises used: TensorProduct.map, TensorProduct.lift, 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
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f₁ f₂ : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
h :
  ∀ (x : V) (x_1 : U),
    Eq (α := TensorProduct A W P)
      (((((TensorProduct.AlgebraTensorModule.curry ((f₁ + f₂).tensor g).toLinearMap :
                    V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                  (a : V) → U →ₗ[A] TensorProduct A W P)
                x :
              U →ₗ[A] TensorProduct A W P) :
            (a : U) → TensorProduct A W P)
          x_1 :
        TensorProduct A W P)
      (((((TensorProduct.AlgebraTensorModule.curry (f₁.tensor g + f₂.tensor g).toLinearMap :
                    V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                  (a : V) → U →ₗ[A] TensorProduct A W P)
                x :
              U →ₗ[A] TensorProduct A W P) :
            (a : U) → TensorProduct A W P)
          x_1 :
        TensorProduct A W P)
⊢ (f₁ + f₂).tensor g = f₁.tensor 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
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f₁ f₂ : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x : V
x_1 : U
⊢ Eq (α := TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry ((f₁ + f₂).tensor g).toLinearMap :
                  V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry (f₁.tensor g + f₂.tensor g).toLinearMap :
                  V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)

Tactic:
simp [TensorProduct.add_tmul]

Premises used: TensorProduct.add_tmul
-- 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
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g₁ g₂ : τ.IntertwiningMap π
h :
  ∀ (x : V) (x_1 : U),
    Eq (α := TensorProduct A W P)
      (((((TensorProduct.AlgebraTensorModule.curry (f.tensor (g₁ + g₂)).toLinearMap :
                    V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                  (a : V) → U →ₗ[A] TensorProduct A W P)
                x :
              U →ₗ[A] TensorProduct A W P) :
            (a : U) → TensorProduct A W P)
          x_1 :
        TensorProduct A W P)
      (((((TensorProduct.AlgebraTensorModule.curry (f.tensor g₁ + f.tensor g₂).toLinearMap :
                    V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                  (a : V) → U →ₗ[A] TensorProduct A W P)
                x :
              U →ₗ[A] TensorProduct A W P) :
            (a : U) → TensorProduct A W P)
          x_1 :
        TensorProduct A W P)
⊢ f.tensor (g₁ + g₂) = f.tensor 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
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g₁ g₂ : τ.IntertwiningMap π
x : V
x_1 : U
⊢ Eq (α := TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry (f.tensor (g₁ + g₂)).toLinearMap :
                  V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry (f.tensor g₁ + f.tensor g₂).toLinearMap :
                  V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)

Tactic:
simp [TensorProduct.tmul_add]

Premises used: TensorProduct.tmul_add
-- 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
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
a : A
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
h :
  ∀ (x : V) (x_1 : U),
    Eq (α := TensorProduct A W P)
      (((((TensorProduct.AlgebraTensorModule.curry ((a • f).tensor g).toLinearMap :
                    V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                  (a : V) → U →ₗ[A] TensorProduct A W P)
                x :
              U →ₗ[A] TensorProduct A W P) :
            (a : U) → TensorProduct A W P)
          x_1 :
        TensorProduct A W P)
      (((((TensorProduct.AlgebraTensorModule.curry (a • f.tensor g).toLinearMap : V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                  (a : V) → U →ₗ[A] TensorProduct A W P)
                x :
              U →ₗ[A] TensorProduct A W P) :
            (a : U) → TensorProduct A W P)
          x_1 :
        TensorProduct A W P)
⊢ (a • f).tensor g = a • 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
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
a : A
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x : V
x_1 : U
⊢ Eq (α := TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry ((a • f).tensor g).toLinearMap : V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry (a • f.tensor g).toLinearMap : V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)

Tactic:
simp [TensorProduct.smul_tmul]

Premises used: TensorProduct.smul_tmul
-- 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
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
a : A
g : τ.IntertwiningMap π
h :
  ∀ (x : V) (x_1 : U),
    Eq (α := TensorProduct A W P)
      (((((TensorProduct.AlgebraTensorModule.curry (f.tensor (a • g)).toLinearMap :
                    V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                  (a : V) → U →ₗ[A] TensorProduct A W P)
                x :
              U →ₗ[A] TensorProduct A W P) :
            (a : U) → TensorProduct A W P)
          x_1 :
        TensorProduct A W P)
      (((((TensorProduct.AlgebraTensorModule.curry (a • f.tensor g).toLinearMap : V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                  (a : V) → U →ₗ[A] TensorProduct A W P)
                x :
              U →ₗ[A] TensorProduct A W P) :
            (a : U) → TensorProduct A W P)
          x_1 :
        TensorProduct A W P)
⊢ f.tensor (a • g) = a • 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
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
a : A
g : τ.IntertwiningMap π
x : V
x_1 : U
⊢ Eq (α := TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry (f.tensor (a • g)).toLinearMap : V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)
    (((((TensorProduct.AlgebraTensorModule.curry (a • f.tensor g).toLinearMap : V →ₗ[A] U →ₗ[A] TensorProduct A W P) :
                (a : V) → U →ₗ[A] TensorProduct A W P)
              x :
            U →ₗ[A] TensorProduct A W P) :
          (a : U) → TensorProduct A W P)
        x_1 :
      TensorProduct A W P)

Tactic:
simp [TensorProduct.tmul_smul]

Premises used: TensorProduct.tmul_smul
-- 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
P : Type u_6
inst_8 : AddCommMonoid P
inst_9 : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
v : V
w : U
⊢ Eq (α := TensorProduct A W P)
    ((f.tensor g : (a : TensorProduct A V U) → TensorProduct A W P) (v ⊗ₜ[A] w) : TensorProduct A W P)
    ((f : (a : V) → W) v ⊗ₜ[A] (g : (a : U) → P) w : TensorProduct A W P)

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 σ
⊢ (lTensor τ f).toLinearMap = LinearMap.lTensor U f.toLinearMap

Tactic:
rfl

Premises used: LinearMap.lTensor, TensorProduct.map, TensorProduct.lift, 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 τ
v : V
w : W
⊢ Eq (α := TensorProduct A V U)
    ((lTensor ρ f : (a : TensorProduct A V W) → TensorProduct A V U) (v ⊗ₜ[A] w) : TensorProduct A V U)
    (v ⊗ₜ[A] (f : (a : W) → U) w : TensorProduct A V U)

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
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
h :
  ∀ (x : V) (x_1 : W),
    Eq (α := TensorProduct A V W)
      (((((TensorProduct.AlgebraTensorModule.curry (lTensor ρ (id σ)).toLinearMap :
                    V →ₗ[A] W →ₗ[A] TensorProduct A V W) :
                  (a : V) → W →ₗ[A] TensorProduct A V W)
                x :
              W →ₗ[A] TensorProduct A V W) :
            (a : W) → TensorProduct A V W)
          x_1 :
        TensorProduct A V W)
      (((((TensorProduct.AlgebraTensorModule.curry (id (ρ.tprod σ)).toLinearMap : V →ₗ[A] W →ₗ[A] TensorProduct A V W) :
                  (a : V) → W →ₗ[A] TensorProduct A V W)
                x :
              W →ₗ[A] TensorProduct A V W) :
            (a : W) → TensorProduct A V W)
          x_1 :
        TensorProduct A V W)
⊢ lTensor ρ (id σ) = id (ρ.tprod σ)

Tactic:
ext
-- 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 : V
x_1 : W
⊢ Eq (α := TensorProduct A V W)
    (((((TensorProduct.AlgebraTensorModule.curry (lTensor ρ (id σ)).toLinearMap : V →ₗ[A] W →ₗ[A] TensorProduct A V W) :
                (a : V) → W →ₗ[A] TensorProduct A V W)
              x :
            W →ₗ[A] TensorProduct A V W) :
          (a : W) → TensorProduct A V W)
        x_1 :
      TensorProduct A V W)
    (((((TensorProduct.AlgebraTensorModule.curry (id (ρ.tprod σ)).toLinearMap : V →ₗ[A] W →ₗ[A] TensorProduct A V W) :
                (a : V) → W →ₗ[A] TensorProduct A V W)
              x :
            W →ₗ[A] TensorProduct A V W) :
          (a : W) → TensorProduct A V W)
        x_1 :
      TensorProduct A V W)

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 : V) (x_1 : W),
    Eq (α := TensorProduct A V U)
      (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (ρ := ρ.tprod σ) (σ := ρ.tprod τ) (lTensor ρ 0)) :
                    V →ₗ[A] W →ₗ[A] TensorProduct A V U) :
                  (a : V) → W →ₗ[A] TensorProduct A V U)
                x :
              W →ₗ[A] TensorProduct A V U) :
            (a : W) → TensorProduct A V U)
          x_1 :
        TensorProduct A V U)
      (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (G := G) (ρ := ρ.tprod σ) (σ := ρ.tprod τ) 0) :
                    V →ₗ[A] W →ₗ[A] TensorProduct A V U) :
                  (a : V) → W →ₗ[A] TensorProduct A V U)
                x :
              W →ₗ[A] TensorProduct A V U) :
            (a : W) → TensorProduct A V U)
          x_1 :
        TensorProduct A V U)
⊢ Eq (α := (ρ.tprod σ).IntertwiningMap (ρ.tprod τ)) (lTensor ρ 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 : V
x_1 : W
⊢ Eq (α := TensorProduct A V U)
    (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (ρ := ρ.tprod σ) (σ := ρ.tprod τ) (lTensor ρ 0)) :
                  V →ₗ[A] W →ₗ[A] TensorProduct A V U) :
                (a : V) → W →ₗ[A] TensorProduct A V U)
              x :
            W →ₗ[A] TensorProduct A V U) :
          (a : W) → TensorProduct A V U)
        x_1 :
      TensorProduct A V U)
    (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (G := G) (ρ := ρ.tprod σ) (σ := ρ.tprod τ) 0) :
                  V →ₗ[A] W →ₗ[A] TensorProduct A V U) :
                (a : V) → W →ₗ[A] TensorProduct A V U)
              x :
            W →ₗ[A] TensorProduct A V U) :
          (a : W) → 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
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 τ
⊢ lTensor ρ (f₁ + f₂) = lTensor ρ f₁ + lTensor ρ f₂

Tactic:
tensor_add_right _ _ _

Premises used: Representation.IntertwiningMap.tensor_add_right, Representation.IntertwiningMap.lTensor
-- 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 τ
⊢ lTensor ρ (a • f) = a • lTensor ρ f

Tactic:
tensor_smul_right _ _ _

Premises used: Representation.IntertwiningMap.tensor_smul_right, Representation.IntertwiningMap.lTensor
-- 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 τ
⊢ (rTensor ρ f).toLinearMap = LinearMap.rTensor V f.toLinearMap

Tactic:
rfl

Premises used: TensorProduct.map, TensorProduct.lift, rfl, LinearMap.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
f : σ.IntertwiningMap τ
v : V
w : W
⊢ Eq (α := TensorProduct A U V)
    ((rTensor ρ f : (a : TensorProduct A W V) → TensorProduct A U V) (w ⊗ₜ[A] v) : TensorProduct A U V)
    ((f : (a : W) → U) w ⊗ₜ[A] v : TensorProduct A U 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
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
h :
  ∀ (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)
⊢ rTensor ρ (id σ) = id (σ.tprod ρ)

Tactic:
ext