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.584160
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
f : M →ₗ[R] M
g : N →ₗ[R] N
h :
  ↑(↑(compr₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N))) f) g = ↑(↑(compl₁₂ (lsmul R R) (trace R M) (trace R N)) f) g
⊢ ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
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.584160
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
have h := ext_iff.1 (ext_iff.1 (trace_tensorProduct R M N) f) g
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.584160
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
f : M →ₗ[R] M
g : N →ₗ[R] N
h : ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
⊢ ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
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.584160
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
f : M →ₗ[R] M
g : N →ₗ[R] N
h :
  ↑(↑(compr₂ (mapBilinear R M N M N) (trace R (M ⊗[R] N))) f) g = ↑(↑(compl₁₂ (lsmul R R) (trace R M) (trace R N)) f) g
⊢ ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
simp only [compr₂_apply, mapBilinear_apply, compl₁₂_apply, lsmul_apply,
  Algebra.id.smul_eq_mul] at h
no goals
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.584160
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
f : M →ₗ[R] M
g : N →ₗ[R] N
h : ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
⊢ ↑(trace R (M ⊗[R] N)) (TensorProduct.map f g) = ↑(trace R M) f * ↑(trace R N) g
exact h