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
ι : Type ?u.549538
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
⊢ compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M) (dualTensorHom R M N) =
    compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M) (dualTensorHom R M N)
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
ι : Type ?u.549538
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
⊢ compr₂ (llcomp R M N M) (trace R M) = compr₂ (flip (llcomp R N M N)) (trace R N)
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
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
ι : Type ?u.549538
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
g : Module.Dual R N
m : M
f : Module.Dual R M
n : N
⊢ ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M) (dualTensorHom R M N)))
                    g)
                m))
          f)
      n =
    ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M)
                          (dualTensorHom R M N)))
                    g)
                m))
          f)
      n
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
ι : Type ?u.549538
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
⊢ compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M) (dualTensorHom R M N) =
    compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M) (dualTensorHom R M N)
ext (g m f n)
no goals
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
ι : Type ?u.549538
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
g : Module.Dual R N
m : M
f : Module.Dual R M
n : N
⊢ ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M) (dualTensorHom R M N)))
                    g)
                m))
          f)
      n =
    ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M)
                          (dualTensorHom R M N)))
                    g)
                m))
          f)
      n
simp only [AlgebraTensorModule.curry_apply_apply, compl₁₂_apply, compr₂_apply, llcomp_apply',
  comp_dualTensorHom, map_smulₛₗ, RingHom.id_apply, trace_eq_contract_apply, contractLeft_apply,
  smul_eq_mul, mul_comm, flip_apply]