case a.h.h.h
k : Type u_1
G : Type u_4
V : Type u_2
W : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Group 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
g : G
x✝² : Module.Dual k V
x✝¹ : W
x✝ : V
⊢ ↑(↑(↑(TensorProduct.AlgebraTensorModule.curry (comp (dualTensorHom k V W) (TensorProduct.map (↑(dual ρV) g) (↑ρW g))))
              x✝²)
          x✝¹)
      x✝ =
    ↑(↑(↑(TensorProduct.AlgebraTensorModule.curry (comp (↑(linHom ρV ρW) g) (dualTensorHom k V W))) x✝²) x✝¹) x✝
k : Type u_1
G : Type u_4
V : Type u_2
W : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Group 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
g : G
⊢ comp (dualTensorHom k V W) (TensorProduct.map (↑(dual ρV) g) (↑ρW g)) = comp (↑(linHom ρV ρW) g) (dualTensorHom k V W)
ext
no goals
case a.h.h.h
k : Type u_1
G : Type u_4
V : Type u_2
W : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Group 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
g : G
x✝² : Module.Dual k V
x✝¹ : W
x✝ : V
⊢ ↑(↑(↑(TensorProduct.AlgebraTensorModule.curry (comp (dualTensorHom k V W) (TensorProduct.map (↑(dual ρV) g) (↑ρW g))))
              x✝²)
          x✝¹)
      x✝ =
    ↑(↑(↑(TensorProduct.AlgebraTensorModule.curry (comp (↑(linHom ρV ρW) g) (dualTensorHom k V W))) x✝²) x✝¹) x✝
simp [Module.Dual.transpose_apply]