case intro
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ comp (trace R M) (dualTensorHom R M M) = contractLeft R M
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
⊢ comp (trace R M) (dualTensorHom R M M) = contractLeft R M
cases nonempty_fintype ι
case intro
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ ∀ (i : ι × ι),
    ↑(comp (trace R M) (dualTensorHom R M M)) (↑(Basis.tensorProduct (Basis.dualBasis b) b) i) =
      ↑(contractLeft R M) (↑(Basis.tensorProduct (Basis.dualBasis b) b) i)
case intro
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ comp (trace R M) (dualTensorHom R M M) = contractLeft R M
apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
case intro.mk
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ ↑(comp (trace R M) (dualTensorHom R M M)) (↑(Basis.tensorProduct (Basis.dualBasis b) b) (i, j)) =
    ↑(contractLeft R M) (↑(Basis.tensorProduct (Basis.dualBasis b) b) (i, j))
case intro
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ ∀ (i : ι × ι),
    ↑(comp (trace R M) (dualTensorHom R M M)) (↑(Basis.tensorProduct (Basis.dualBasis b) b) i) =
      ↑(contractLeft R M) (↑(Basis.tensorProduct (Basis.dualBasis b) b) i)
rintro ⟨i, j⟩
case intro.mk
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ ↑(trace R M) (↑(dualTensorHom R M M) (Basis.coord b i ⊗ₜ[R] ↑b j)) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
case intro.mk
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ ↑(comp (trace R M) (dualTensorHom R M M)) (↑(Basis.tensorProduct (Basis.dualBasis b) b) (i, j)) =
    ↑(contractLeft R M) (↑(Basis.tensorProduct (Basis.dualBasis b) b) (i, j))
simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
case intro.mk
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ Matrix.trace (stdBasisMatrix j i 1) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
case intro.mk
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ ↑(trace R M) (↑(dualTensorHom R M M) (Basis.coord b i ⊗ₜ[R] ↑b j)) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
case pos
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : i = j
⊢ Matrix.trace (stdBasisMatrix j i 1) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)

case neg
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : ¬i = j
⊢ Matrix.trace (stdBasisMatrix j i 1) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
case intro.mk
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ Matrix.trace (stdBasisMatrix j i 1) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
by_cases hij : i = j
case neg
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : ¬i = j
⊢ 0 = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
case neg
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : ¬i = j
⊢ Matrix.trace (stdBasisMatrix j i 1) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
rw [Matrix.StdBasisMatrix.trace_zero j i (1 : R) hij]
no goals
case neg
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : ¬i = j
⊢ 0 = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
simp [Finsupp.single_eq_pi_single, hij]
case pos
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : i = j
⊢ Matrix.trace (stdBasisMatrix j j 1) = ↑(contractLeft R M) (Basis.coord b j ⊗ₜ[R] ↑b j)
case pos
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : i = j
⊢ Matrix.trace (stdBasisMatrix j i 1) = ↑(contractLeft R M) (Basis.coord b i ⊗ₜ[R] ↑b j)
rw [hij]
no goals
case pos
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.321532
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : i = j
⊢ Matrix.trace (stdBasisMatrix j j 1) = ↑(contractLeft R M) (Basis.coord b j ⊗ₜ[R] ↑b j)
simp