-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_comp_comm :
    compr₂ (llcomp R M N M) (trace R M) = compr₂ (llcomp R N M N).flip (trace R 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
⊢ ((llcomp R M N M).compr₂ (trace R M)).compl₁₂ (dualTensorHom R N M) (dualTensorHom R M N) =
    ((llcomp R N M N).flip.compr₂ (trace R N)).compl₁₂ (dualTensorHom R N M) (dualTensorHom R M N)

Tactic:
ext g m f 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
g : Dual R N
m : M
f : Dual R M
n : N
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (((llcomp R M N M).compr₂ (trace R M)).compl₁₂ (dualTensorHom R N M) (dualTensorHom R M N)))
              g)
            m))
        f)
      n =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (((llcomp R N M N).flip.compr₂ (trace R N)).compl₁₂ (dualTensorHom R N M) (dualTensorHom R M N)))
              g)
            m))
        f)
      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
g : Dual R N
m : M
f : Dual R M
n : N
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (((llcomp R M N M).compr₂ (trace R M)).compl₁₂ (dualTensorHom R N M) (dualTensorHom R M N)))
              g)
            m))
        f)
      n =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (((llcomp R N M N).flip.compr₂ (trace R N)).compl₁₂ (dualTensorHom R N M) (dualTensorHom R M N)))
              g)
            m))
        f)
      n

Tactic:
simp only [AlgebraTensorModule.curry_apply, TensorProduct.curry_apply,
  coe_restrictScalars, compl₁₂_apply, compr₂_apply, flip_apply, llcomp_apply',
  comp_dualTensorHom, LinearMapClass.map_smul, trace_eq_contract_apply,
  contractLeft_apply, smul_eq_mul, mul_comm]

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
⊢ (llcomp R M N M).compr₂ (trace R M) = (llcomp R N M N).flip.compr₂ (trace R N)

Tactic:
apply
  (compl₁₂_inj (show Surjective (dualTensorHom R N M) from (dualTensorHomEquiv R N M).surjective)
      (show Surjective (dualTensorHom R M N) from (dualTensorHomEquiv R M 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
⊢ ((llcomp R M N M).compr₂ (trace R M)).compl₁₂ (dualTensorHom R N M) (dualTensorHom R M N) =
    ((llcomp R N M N).flip.compr₂ (trace R N)).compl₁₂ (dualTensorHom R N M) (dualTensorHom R M N)