-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
intro : ∀ (val : Fintype ι), Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
intro₁ :
  ∀ (val : Fintype ι) (i : ι × ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
intro₂ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
            Dual R M ⊗[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
            Dual R M ⊗[R] M) :
        R)
intro₃ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j) :
            M →ₗ[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
intro₄ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
intro₅ :
  ∀ (val : Fintype ι) (i : ι),
    Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single i i 1) : R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) i : Dual R M ⊗[R] M) : R)
intro₆ intro₇ :
  ∀ (val : Fintype ι) (i j : ι) (hij : i ≠ j),
    Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
intro₈ :
  ∀ (val : Fintype ι) (i j : ι) (hij : i ≠ j),
    Eq.{u_1 + 1} (α := R) (0 : R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)

Tactic:
classical
    cases nonempty_fintype ι
    apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
    rintro ⟨i, j⟩
    simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
    rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
    obtain rfl | hij := eq_or_ne i j
    · simp
    rw [Matrix.trace_single_eq_of_ne j i (1 : R) hij.symm]
    simp [hij]

Premises used: Module.Basis.tensorProduct_apply, Module.Basis.coe_dualBasis, toMatrix_dualTensorHom, nonempty_fintype, LinearMap.coe_comp, Function.comp_apply, rfl