mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f : σ.IntertwiningMap τ
x✝² x✝¹ : ρ.IntertwiningMap σ
x✝ : V
⊢ (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x✝² + x✝¹).toLinearMap) ⋯).toLinearMap x✝ =
    (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝².toLinearMap) ⋯ +
          LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝¹.toLinearMap) ⋯).toLinearMap
      x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f : σ.IntertwiningMap τ
x✝² x✝¹ : ρ.IntertwiningMap σ
x✝ : V
⊢ (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x✝² + x✝¹).toLinearMap) ⋯).toLinearMap x✝ =
    (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝².toLinearMap) ⋯ +
          LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝¹.toLinearMap) ⋯).toLinearMap
      x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f : σ.IntertwiningMap τ
x✝² : A
x✝¹ : ρ.IntertwiningMap σ
x✝ : V
⊢ (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x✝² • x✝¹).toLinearMap) ⋯).toLinearMap x✝ =
    ((RingHom.id A) x✝² •
          LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝¹.toLinearMap) ⋯).toLinearMap
      x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f : σ.IntertwiningMap τ
x✝² : A
x✝¹ : ρ.IntertwiningMap σ
x✝ : V
⊢ (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x✝² • x✝¹).toLinearMap) ⋯).toLinearMap x✝ =
    ((RingHom.id A) x✝² •
          LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝¹.toLinearMap) ⋯).toLinearMap
      x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
x✝³ x✝² : σ.IntertwiningMap τ
x✝¹ : ρ.IntertwiningMap σ
x✝ : V
⊢ ({ toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x✝³ + x✝²).toLinearMap ∘ₗ g.toLinearMap) ⋯,
            map_add' := ⋯, map_smul' := ⋯ }
          x✝¹).toLinearMap
      x✝ =
    (({ toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝³.toLinearMap ∘ₗ g.toLinearMap) ⋯,
              map_add' := ⋯, map_smul' := ⋯ } +
            { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝².toLinearMap ∘ₗ g.toLinearMap) ⋯,
              map_add' := ⋯, map_smul' := ⋯ })
          x✝¹).toLinearMap
      x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
x✝³ x✝² : σ.IntertwiningMap τ
x✝¹ : ρ.IntertwiningMap σ
x✝ : V
⊢ ({ toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x✝³ + x✝²).toLinearMap ∘ₗ g.toLinearMap) ⋯,
            map_add' := ⋯, map_smul' := ⋯ }
          x✝¹).toLinearMap
      x✝ =
    (({ toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝³.toLinearMap ∘ₗ g.toLinearMap) ⋯,
              map_add' := ⋯, map_smul' := ⋯ } +
            { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝².toLinearMap ∘ₗ g.toLinearMap) ⋯,
              map_add' := ⋯, map_smul' := ⋯ })
          x✝¹).toLinearMap
      x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
x✝³ : A
x✝² : σ.IntertwiningMap τ
x✝¹ : ρ.IntertwiningMap σ
x✝ : V
⊢ ({ toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x✝³ • x✝²).toLinearMap ∘ₗ g.toLinearMap) ⋯,
            map_add' := ⋯, map_smul' := ⋯ }
          x✝¹).toLinearMap
      x✝ =
    (((RingHom.id A) x✝³ •
            { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝².toLinearMap ∘ₗ g.toLinearMap) ⋯,
              map_add' := ⋯, map_smul' := ⋯ })
          x✝¹).toLinearMap
      x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
x✝³ : A
x✝² : σ.IntertwiningMap τ
x✝¹ : ρ.IntertwiningMap σ
x✝ : V
⊢ ({ toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x✝³ • x✝²).toLinearMap ∘ₗ g.toLinearMap) ⋯,
            map_add' := ⋯, map_smul' := ⋯ }
          x✝¹).toLinearMap
      x✝ =
    (((RingHom.id A) x✝³ •
            { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝².toLinearMap ∘ₗ g.toLinearMap) ⋯,
              map_add' := ⋯, map_smul' := ⋯ })
          x✝¹).toLinearMap
      x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
a : A
f g : ρ.IntertwiningMap ρ
x✝ : V
⊢ (f * a • g).toLinearMap x✝ = (a • (f * g)).toLinearMap x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
a : A
f g : ρ.IntertwiningMap ρ
x✝ : V
⊢ (f * a • g).toLinearMap x✝ = (a • (f * g)).toLinearMap x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f g : ρ.IntertwiningMap ρ
⊢ (equivLinearMapAsModule ρ ρ) (f * g) = (equivLinearMapAsModule ρ ρ) f * (equivLinearMapAsModule ρ ρ) g

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
f g : ρ.IntertwiningMap ρ
⊢ (equivLinearMapAsModule ρ ρ) (f * g) = (equivLinearMapAsModule ρ ρ) f * (equivLinearMapAsModule ρ ρ) g
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
x✝ : V
⊢ (centralAlgebraMul ρ ⋯).toLinearMap x✝ = (toLinearMap 1) x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
x✝ : V
⊢ (centralAlgebraMul ρ ⋯).toLinearMap x✝ = (toLinearMap 1) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
x✝² x✝¹ : ↥(Submonoid.center A[G])
x✝ : V
⊢ (centralAlgebraMul ρ ⋯).toLinearMap x✝ = (centralAlgebraMul ρ ⋯ * centralAlgebraMul ρ ⋯).toLinearMap x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
x✝² x✝¹ : ↥(Submonoid.center A[G])
x✝ : V
⊢ (centralAlgebraMul ρ ⋯).toLinearMap x✝ = (centralAlgebraMul ρ ⋯ * centralAlgebraMul ρ ⋯).toLinearMap x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f₁ f₂ : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x✝¹ : V
x✝ : U
⊢ ((TensorProduct.AlgebraTensorModule.curry ((f₁ + f₂).tensor g).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (f₁.tensor g + f₂.tensor g).toLinearMap) x✝¹) x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f₁ f₂ : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x✝¹ : V
x✝ : U
⊢ ((TensorProduct.AlgebraTensorModule.curry ((f₁ + f₂).tensor g).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (f₁.tensor g + f₂.tensor g).toLinearMap) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g₁ g₂ : τ.IntertwiningMap π
x✝¹ : V
x✝ : U
⊢ ((TensorProduct.AlgebraTensorModule.curry (f.tensor (g₁ + g₂)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (f.tensor g₁ + f.tensor g₂).toLinearMap) x✝¹) x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g₁ g₂ : τ.IntertwiningMap π
x✝¹ : V
x✝ : U
⊢ ((TensorProduct.AlgebraTensorModule.curry (f.tensor (g₁ + g₂)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (f.tensor g₁ + f.tensor g₂).toLinearMap) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
a : A
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x✝¹ : V
x✝ : U
⊢ ((TensorProduct.AlgebraTensorModule.curry ((a • f).tensor g).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (a • f.tensor g).toLinearMap) x✝¹) x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
a : A
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
x✝¹ : V
x✝ : U
⊢ ((TensorProduct.AlgebraTensorModule.curry ((a • f).tensor g).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (a • f.tensor g).toLinearMap) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
a : A
g : τ.IntertwiningMap π
x✝¹ : V
x✝ : U
⊢ ((TensorProduct.AlgebraTensorModule.curry (f.tensor (a • g)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (a • f.tensor g).toLinearMap) x✝¹) x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
a : A
g : τ.IntertwiningMap π
x✝¹ : V
x✝ : U
⊢ ((TensorProduct.AlgebraTensorModule.curry (f.tensor (a • g)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (a • f.tensor g).toLinearMap) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
a : A
g : τ.IntertwiningMap π
⊢ f.tensor (a • g) = a • f.tensor g

Tactic:
ext; simp [TensorProduct.tmul_smul]

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
x✝¹ : V
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry (lTensor ρ (id σ)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (id (ρ.tprod σ)).toLinearMap) x✝¹) x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
x✝¹ : V
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry (lTensor ρ (id σ)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (id (ρ.tprod σ)).toLinearMap) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
x✝¹ : V
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry (lTensor ρ 0).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (toLinearMap 0)) x✝¹) x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
x✝¹ : V
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry (lTensor ρ 0).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (toLinearMap 0)) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
x✝¹ : W
x✝ : V
⊢ ((TensorProduct.AlgebraTensorModule.curry (rTensor ρ (id σ)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (id (σ.tprod ρ)).toLinearMap) x✝¹) x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
x✝¹ : W
x✝ : V
⊢ ((TensorProduct.AlgebraTensorModule.curry (rTensor ρ (id σ)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (id (σ.tprod ρ)).toLinearMap) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
x✝¹ : W
x✝ : V
⊢ ((TensorProduct.AlgebraTensorModule.curry (rTensor ρ 0).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (toLinearMap 0)) x✝¹) x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
x✝¹ : W
x✝ : V
⊢ ((TensorProduct.AlgebraTensorModule.curry (rTensor ρ 0).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (toLinearMap 0)) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
Q : Type u_7
inst✝¹ : AddCommMonoid Q
inst✝ : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
x✝¹ : V
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry ((rTensor υ f).comp (lTensor ρ g)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (f.tensor g).toLinearMap) x✝¹) x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
Q : Type u_7
inst✝¹ : AddCommMonoid Q
inst✝ : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
x✝¹ : V
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry ((rTensor υ f).comp (lTensor ρ g)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (f.tensor g).toLinearMap) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
Q : Type u_7
inst✝¹ : AddCommMonoid Q
inst✝ : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
x✝¹ : V
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry ((lTensor τ g).comp (rTensor σ f)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (f.tensor g).toLinearMap) x✝¹) x✝

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
Q : Type u_7
inst✝¹ : AddCommMonoid Q
inst✝ : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
x✝¹ : V
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry ((lTensor τ g).comp (rTensor σ f)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (f.tensor g).toLinearMap) x✝¹) x✝