case h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ ↑(comp (↑(dualTensorHom R N P) (g ⊗ₜ[R] p)) (↑(dualTensorHom R M N) (f ⊗ₜ[R] n))) m =
    ↑(↑g n • ↑(dualTensorHom R M P) (f ⊗ₜ[R] p)) m
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
n : N
g : Dual R N
p : P
⊢ comp (↑(dualTensorHom R N P) (g ⊗ₜ[R] p)) (↑(dualTensorHom R M N) (f ⊗ₜ[R] n)) =
    ↑g n • ↑(dualTensorHom R M P) (f ⊗ₜ[R] p)
ext m
case h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ ↑f m • ↑g n • p = ↑g n • ↑f m • p
case h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ ↑(comp (↑(dualTensorHom R N P) (g ⊗ₜ[R] p)) (↑(dualTensorHom R M N) (f ⊗ₜ[R] n))) m =
    ↑(↑g n • ↑(dualTensorHom R M P) (f ⊗ₜ[R] p)) m
simp only [coe_comp, Function.comp_apply, dualTensorHom_apply, LinearMap.map_smul,
  RingHom.id_apply, LinearMap.smul_apply]
no goals
case h
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
n : N
g : Dual R N
p : P
m : M
⊢ ↑f m • ↑g n • p = ↑g n • ↑f m • p
rw [smul_comm]