-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_eq_contract_of_basis [Finite ι] (b : Basis ι R M) :
    LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M

Proof state:
case intro.mk
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ (Matrix.stdBasisMatrix j i 1).trace = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)

Tactic:
by_cases hij : i = j

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : i = j
⊢ (Matrix.stdBasisMatrix j i 1).trace = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)

case neg
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : ¬i = j
⊢ (Matrix.stdBasisMatrix j i 1).trace = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)

Proof state:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : ¬i = j
⊢ 0 = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)

Tactic:
simp [Finsupp.single_eq_pi_single, hij]

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ trace R M ∘ₗ dualTensorHom R M M = contractLeft R M

Tactic:
apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ ∀ (i : ι × ι),
    (trace R M ∘ₗ dualTensorHom R M M) ((b.dualBasis.tensorProduct b) i) =
      (contractLeft R M) ((b.dualBasis.tensorProduct b) i)

Proof state:
case intro.mk
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ (trace R M ∘ₗ dualTensorHom R M M) ((b.dualBasis.tensorProduct b) (i, j)) =
    (contractLeft R M) ((b.dualBasis.tensorProduct b) (i, j))

Tactic:
simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]

Result:
case intro.mk
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ (trace R M) ((dualTensorHom R M M) (b.coord i ⊗ₜ[R] b j)) = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ ∀ (i : ι × ι),
    (trace R M ∘ₗ dualTensorHom R M M) ((b.dualBasis.tensorProduct b) i) =
      (contractLeft R M) ((b.dualBasis.tensorProduct b) i)

Tactic:
rintro ⟨i, j⟩

Result:
case intro.mk
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ (trace R M ∘ₗ dualTensorHom R M M) ((b.dualBasis.tensorProduct b) (i, j)) =
    (contractLeft R M) ((b.dualBasis.tensorProduct b) (i, j))

Proof state:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : ¬i = j
⊢ (Matrix.stdBasisMatrix j i 1).trace = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)

Tactic:
rw [Matrix.StdBasisMatrix.trace_zero j i (1 : R) hij]

Result:
case neg
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : ¬i = j
⊢ 0 = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
⊢ trace R M ∘ₗ dualTensorHom R M M = contractLeft R M

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ trace R M ∘ₗ dualTensorHom R M M = contractLeft R M

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : i = j
⊢ (Matrix.stdBasisMatrix j i 1).trace = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)

Tactic:
rw [hij]

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : i = j
⊢ (Matrix.stdBasisMatrix j j 1).trace = (contractLeft R M) (b.coord j ⊗ₜ[R] b j)

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : i = j
⊢ (Matrix.stdBasisMatrix j j 1).trace = (contractLeft R M) (b.coord j ⊗ₜ[R] b j)

Tactic:
simp

Result:
no goals

Proof state:
case intro.mk
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ (trace R M) ((dualTensorHom R M M) (b.coord i ⊗ₜ[R] b j)) = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)

Tactic:
rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]

Result:
case intro.mk
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
⊢ (Matrix.stdBasisMatrix j i 1).trace = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)