R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type ?u.401815
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.402357
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
⊢ comp (trace R (Module.Dual R M)) Module.Dual.transpose = trace R M
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type ?u.401815
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.402357
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
⊢ comp (trace R (Module.Dual R M)) Module.Dual.transpose = trace R M
let e := dualTensorHomEquiv R M M
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type ?u.401815
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.402357
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ↑↑e
⊢ comp (trace R (Module.Dual R M)) Module.Dual.transpose = trace R M
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type ?u.401815
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.402357
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
⊢ comp (trace R (Module.Dual R M)) Module.Dual.transpose = trace R M
have h : Function.Surjective e.toLinearMap := e.surjective
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type ?u.401815
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.402357
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ↑↑e
⊢ comp (comp (trace R (Module.Dual R M)) Module.Dual.transpose) ↑e = comp (trace R M) ↑e
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type ?u.401815
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.402357
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ↑↑e
⊢ comp (trace R (Module.Dual R M)) Module.Dual.transpose = trace R M
refine' (cancel_right h).1 _
case a.h.h
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type ?u.401815
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.402357
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ↑↑e
f : Module.Dual R M
m : M
⊢ ↑(↑(AlgebraTensorModule.curry (comp (comp (trace R (Module.Dual R M)) Module.Dual.transpose) ↑e)) f) m =
    ↑(↑(AlgebraTensorModule.curry (comp (trace R M) ↑e)) f) m
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type ?u.401815
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.402357
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ↑↑e
⊢ comp (comp (trace R (Module.Dual R M)) Module.Dual.transpose) ↑e = comp (trace R M) ↑e
ext (f m)
no goals
case a.h.h
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type ?u.401815
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type ?u.402357
inst✝⁴ : Module.Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Free R N
inst✝¹ : Module.Finite R N
inst✝ : Nontrivial R
e : Module.Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ↑↑e
f : Module.Dual R M
m : M
⊢ ↑(↑(AlgebraTensorModule.curry (comp (comp (trace R (Module.Dual R M)) Module.Dual.transpose) ↑e)) f) m =
    ↑(↑(AlgebraTensorModule.curry (comp (trace R M) ↑e)) f) m
simp