k : Type u_1
G : Type u_2
V : Type u_4
W : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ ↑(↑(asAlgebraHom (1 ⊗ ρW)) r) (x ⊗ₜ[k] y) = x ⊗ₜ[k] ↑(↑(asAlgebraHom ρW) r) y
k : Type u_1
G : Type u_2
V : Type u_4
W : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ let y' := y;
  let z := x ⊗ₜ[k] y;
  r • z = x ⊗ₜ[k] (r • y')
show asAlgebraHom (1 ⊗ ρW) _ _ = _ ⊗ₜ asAlgebraHom ρW _ _
k : Type u_1
G : Type u_2
V : Type u_4
W : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ (Finsupp.sum r fun i d => d • x ⊗ₜ[k] ↑(↑ρW i) y) = x ⊗ₜ[k] Finsupp.sum r fun i d => d • ↑(↑ρW i) y
k : Type u_1
G : Type u_2
V : Type u_4
W : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ ↑(↑(asAlgebraHom (1 ⊗ ρW)) r) (x ⊗ₜ[k] y) = x ⊗ₜ[k] ↑(↑(asAlgebraHom ρW) r) y
simp only [asAlgebraHom_def, MonoidAlgebra.lift_apply, tprod_apply, MonoidHom.one_apply,
  LinearMap.finsupp_sum_apply, LinearMap.smul_apply, TensorProduct.map_tmul, LinearMap.one_apply]
no goals
k : Type u_1
G : Type u_2
V : Type u_4
W : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ (Finsupp.sum r fun i d => d • x ⊗ₜ[k] ↑(↑ρW i) y) = x ⊗ₜ[k] Finsupp.sum r fun i d => d • ↑(↑ρW i) y
simp only [Finsupp.sum, TensorProduct.tmul_sum, TensorProduct.tmul_smul]