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.485168
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 :
  ↑(comp (trace R (M × N)) (prodMapLinear R M N M N R)) (f, g) =
    ↑(comp (coprod id id) (prodMap (trace R M) (trace R N))) (f, g)
⊢ ↑(trace R (M × N)) (prodMap 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.485168
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 × N)) (prodMap f g) = ↑(trace R M) f + ↑(trace R N) g
have h := ext_iff.1 (trace_prodMap 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.485168
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 × N)) (prodMap f g) = ↑(trace R M) f + ↑(trace R N) g
⊢ ↑(trace R (M × N)) (prodMap 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.485168
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 :
  ↑(comp (trace R (M × N)) (prodMapLinear R M N M N R)) (f, g) =
    ↑(comp (coprod id id) (prodMap (trace R M) (trace R N))) (f, g)
⊢ ↑(trace R (M × N)) (prodMap f g) = ↑(trace R M) f + ↑(trace R N) g
simp only [coe_comp, Function.comp_apply, prodMap_apply, coprod_apply, id_coe, id.def,
  prodMapLinear_apply] 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.485168
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 × N)) (prodMap f g) = ↑(trace R M) f + ↑(trace R N) g
⊢ ↑(trace R (M × N)) (prodMap f g) = ↑(trace R M) f + ↑(trace R N) g
exact h