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.502155
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₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N))) (dualTensorHom R M M) (dualTensorHom R N N) =
    compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M) (dualTensorHom R N 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.502155
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
⊢ compr₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N)) = compl₁₂ (lsmul R R) (trace R M) (trace R N)
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
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.502155
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
f : Module.Dual R M
m : M
g : Module.Dual R N
n : N
⊢ ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compr₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N))) (dualTensorHom R M M)
                          (dualTensorHom R N N)))
                    f)
                m))
          g)
      n =
    ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M)
                          (dualTensorHom R N N)))
                    f)
                m))
          g)
      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.502155
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₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N))) (dualTensorHom R M M) (dualTensorHom R N N) =
    compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M) (dualTensorHom R N N)
ext (f m g 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.502155
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
f : Module.Dual R M
m : M
g : Module.Dual R N
n : N
⊢ ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compr₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N))) (dualTensorHom R M M)
                          (dualTensorHom R N N)))
                    f)
                m))
          g)
      n =
    ↑(↑(AlgebraTensorModule.curry
              (↑(↑(AlgebraTensorModule.curry
                        (compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M)
                          (dualTensorHom R N N)))
                    f)
                m))
          g)
      n
simp only [AlgebraTensorModule.curry_apply_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]