case h.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
m : M
f' : Dual R M
m' : M
⊢ ↑(↑(↑Dual.transpose (↑(dualTensorHom R M M) (f ⊗ₜ[R] m))) f') m' =
    ↑(↑(↑(dualTensorHom R (Dual R M) (Dual R M)) (↑(Dual.eval R M) m ⊗ₜ[R] f)) f') 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
m : M
⊢ ↑Dual.transpose (↑(dualTensorHom R M M) (f ⊗ₜ[R] m)) =
    ↑(dualTensorHom R (Dual R M) (Dual R M)) (↑(Dual.eval R M) m ⊗ₜ[R] f)
ext (f' m')
case h.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
m : M
f' : Dual R M
m' : M
⊢ ↑f m' * ↑f' m = ↑f' m * ↑f m'
case h.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
m : M
f' : Dual R M
m' : M
⊢ ↑(↑(↑Dual.transpose (↑(dualTensorHom R M M) (f ⊗ₜ[R] m))) f') m' =
    ↑(↑(↑(dualTensorHom R (Dual R M) (Dual R M)) (↑(Dual.eval R M) m ⊗ₜ[R] f)) f') m'
simp only [Dual.transpose_apply, coe_comp, Function.comp_apply, dualTensorHom_apply,
  LinearMap.map_smulₛₗ, RingHom.id_apply, Algebra.id.smul_eq_mul, Dual.eval_apply,
  LinearMap.smul_apply]
no goals
case h.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
m : M
f' : Dual R M
m' : M
⊢ ↑f m' * ↑f' m = ↑f' m * ↑f m'
exact mul_comm _ _