-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_tensorProduct : compr₂ (mapBilinear R M N M N) (trace R (M ⊗ N)) =
    compl₁₂ (lsmul R R : R →ₗ[R] R →ₗ[R] R) (trace R M) (trace R N)

Proof state:
case a.h.h.a.h.h
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : Dual R M
m : M
g : Dual R N
n : N
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (((mapBilinear R M N M N).compr₂ (trace R (M ⊗[R] N))).compl₁₂ (dualTensorHom R M M)
                  (dualTensorHom R N N)))
              f)
            m))
        g)
      n =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (((lsmul R R).compl₁₂ (trace R M) (trace R N)).compl₁₂ (dualTensorHom R M M) (dualTensorHom R N N)))
              f)
            m))
        g)
      n

Tactic:
simp only [AlgebraTensorModule.curry_apply, toFun_eq_coe, TensorProduct.curry_apply,
  coe_restrictScalars, compl₁₂_apply, compr₂_apply, mapBilinear_apply,
  trace_eq_contract_apply, contractLeft_apply, lsmul_apply, Algebra.id.smul_eq_mul,
  map_dualTensorHom, dualDistrib_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
⊢ (mapBilinear R M N M N).compr₂ (trace R (M ⊗[R] N)) = (lsmul R R).compl₁₂ (trace R M) (trace R N)

Tactic:
apply
  (compl₁₂_inj (show Surjective (dualTensorHom R M M) from (dualTensorHomEquiv R M M).surjective)
      (show Surjective (dualTensorHom R N N) from (dualTensorHomEquiv R N N).surjective)).1

Result:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
⊢ ((mapBilinear R M N M N).compr₂ (trace R (M ⊗[R] N))).compl₁₂ (dualTensorHom R M M) (dualTensorHom R N N) =
    ((lsmul R R).compl₁₂ (trace R M) (trace R N)).compl₁₂ (dualTensorHom R M M) (dualTensorHom R N N)

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
⊢ ((mapBilinear R M N M N).compr₂ (trace R (M ⊗[R] N))).compl₁₂ (dualTensorHom R M M) (dualTensorHom R N N) =
    ((lsmul R R).compl₁₂ (trace R M) (trace R N)).compl₁₂ (dualTensorHom R M M) (dualTensorHom R N N)

Tactic:
ext f m g n

Result:
case a.h.h.a.h.h
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : Dual R M
m : M
g : Dual R N
n : N
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (((mapBilinear R M N M N).compr₂ (trace R (M ⊗[R] N))).compl₁₂ (dualTensorHom R M M)
                  (dualTensorHom R N N)))
              f)
            m))
        g)
      n =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (((lsmul R R).compl₁₂ (trace R M) (trace R N)).compl₁₂ (dualTensorHom R M M) (dualTensorHom R N N)))
              f)
            m))
        g)
      n