-- Mathlib/LinearAlgebra/Coevaluation.lean
theorem contractLeft_assoc_coevaluation :
    (contractLeft K V).rTensor _ ∘ₗ
        (TensorProduct.assoc K _ _ _).symm.toLinearMap ∘ₗ
          (coevaluation K V).lTensor (Module.Dual K V) =
      (TensorProduct.lid K _).symm.toLinearMap ∘ₗ (TensorProduct.rid K _).toLinearMap

Proof state:
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (∑ x : ↑(Basis.ofVectorSpaceIndex K V), if x = j then 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x else 0) =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j

Tactic:
rw [Finset.sum_ite_eq']

Result:
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (if j ∈ Finset.univ then 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j else 0) = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j

Proof state:
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V))
      ((TensorProduct.assoc K (Dual K V) V (Dual K V)).symm
        ((LinearMap.lTensor (Dual K V) (coevaluation K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1))) =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j

Tactic:
simp only [LinearEquiv.coe_toLinearMap, LinearMap.lTensor_tmul, coevaluation_apply_one]

Result:
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V))
      ((TensorProduct.assoc K (Dual K V) V (Dual K V)).symm
        ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K]
          ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i)) =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j

Proof state:
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (if j ∈ Finset.univ then 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j else 0) = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j

Tactic:
simp only [Finset.mem_univ, if_true]

Result:
no goals

Proof state:
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K (Dual K V) V (Dual K V)).symm ∘ₗ LinearMap.lTensor (Dual K V) (coevaluation K V))
      ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1) =
    (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V)))
      ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1)

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_toLinearMap]

Result:
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V))
      ((TensorProduct.assoc K (Dual K V) V (Dual K V)).symm
        ((LinearMap.lTensor (Dual K V) (coevaluation K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1))) =
    (TensorProduct.lid K (Dual K V)).symm
      ((TensorProduct.rid K (Dual K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1))