awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Coevaluation
Goal:
K : Type u
inst : Field K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
rw :
  Eq (α := V ⊗[K] Dual K V)
    (∑ i : Unit,
      HSMul.hSMul (α := K) (β := V ⊗[K] Dual K V)
        ((Basis.equivFun (Basis.singleton Unit K) : (a : K) → Unit → K) 1 i : K)
        (∑ i : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
          (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) i ⊗ₜ[K]
            Basis.coord (Basis.ofVectorSpace K V) i))
    (∑ i : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
      (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) i ⊗ₜ[K]
        Basis.coord (Basis.ofVectorSpace K V) i)
⊢ Eq (α := V ⊗[K] Dual K V)
    (((Basis.constr (Basis.singleton Unit K) K : (a : Unit → V ⊗[K] Dual K V) → K →ₗ[K] V ⊗[K] Dual K V)
          fun (x : Unit) ↦
          ∑ i : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
            (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) i ⊗ₜ[K]
              Basis.coord (Basis.ofVectorSpace K V) i :
        (a : K) → V ⊗[K] Dual K V)
      1)
    (∑ i : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
      (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) i ⊗ₜ[K]
        Basis.coord (Basis.ofVectorSpace K V) i)

Tactic:
rw [(Basis.singleton Unit K).constr_apply_fintype K]

Premises used: Module.Basis.constr_apply_fintype, Unit, Module.Basis.singleton
-- Module: Mathlib.LinearAlgebra.Coevaluation
Goal:
K : Type u
inst : Field K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
⊢ Eq (α := V ⊗[K] Dual K V)
    (∑ i : Unit,
      HSMul.hSMul (α := K) (β := V ⊗[K] Dual K V)
        ((Basis.equivFun (Basis.singleton Unit K) : (a : K) → Unit → K) 1 i : K)
        (∑ i : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
          (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) i ⊗ₜ[K]
            Basis.coord (Basis.ofVectorSpace K V) i))
    (∑ i : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
      (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) i ⊗ₜ[K]
        Basis.coord (Basis.ofVectorSpace K V) i)

Tactic:
simp only [Fintype.univ_punit, Finset.sum_const, one_smul, Basis.singleton_repr,
    Basis.equivFun_apply, Basis.coe_ofVectorSpace, Finset.card_singleton]

Premises used: Module.Basis.singleton_repr, one_smul, Module.Basis.coe_ofVectorSpace, Module.Basis.equivFun_apply, Fintype.univ_punit, Finset.sum_const, Finset.card_singleton
-- Module: Mathlib.LinearAlgebra.Coevaluation
Goal:
K : Type u
inst : Field K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
this : DecidableEq (↑(Basis.ofVectorSpaceIndex K V) : Type v) :=
  Classical.decEq (↑(Basis.ofVectorSpaceIndex K V) : Type v)
H :
  Eq (α := Dual K V →ₗ[K] K →ₗ[K] K ⊗[K] Dual K V)
    (LinearMap.compr₂ₛₗ (TensorProduct.mk K (Dual K V) K)
      (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V))) :
            Dual K V ⊗[K] (V ⊗[K] Dual K V) →ₗ[K] Dual K V ⊗[K] V ⊗[K] Dual K V) ∘ₗ
          LinearMap.lTensor (Dual K V) (coevaluation K V)))
    (LinearMap.compr₂ₛₗ (TensorProduct.mk K (Dual K V) K)
      ((↑(LinearEquiv.symm (TensorProduct.lid K (Dual K V))) : Dual K V →ₗ[K] K ⊗[K] Dual K V) ∘ₗ
        (↑(TensorProduct.rid K (Dual K V)) : Dual K V ⊗[K] K →ₗ[K] Dual K V)))
⊢ Eq (α := Dual K V ⊗[K] K →ₗ[K] K ⊗[K] Dual K V)
    (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
      (↑(LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V))) :
          Dual K V ⊗[K] (V ⊗[K] Dual K V) →ₗ[K] Dual K V ⊗[K] V ⊗[K] Dual K V) ∘ₗ
        LinearMap.lTensor (Dual K V) (coevaluation K V))
    ((↑(LinearEquiv.symm (TensorProduct.lid K (Dual K V))) : Dual K V →ₗ[K] K ⊗[K] Dual K V) ∘ₗ
      (↑(TensorProduct.rid K (Dual K V)) : Dual K V ⊗[K] K →ₗ[K] Dual K V))

Tactic:
apply TensorProduct.ext

Premises used: TensorProduct.ext
-- Module: Mathlib.LinearAlgebra.Coevaluation
Goal:
K : Type u
inst : Field K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
this : DecidableEq (↑(Basis.ofVectorSpaceIndex K V) : Type v) :=
  Classical.decEq (↑(Basis.ofVectorSpaceIndex K V) : Type v)
H :
  ∀ (i : (↑(Basis.ofVectorSpaceIndex K V) : Type v)),
    Eq (α := K →ₗ[K] K ⊗[K] Dual K V)
      ((LinearMap.compr₂ₛₗ (TensorProduct.mk K (Dual K V) K)
              (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
                (↑(LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V))) :
                    Dual K V ⊗[K] (V ⊗[K] Dual K V) →ₗ[K] Dual K V ⊗[K] V ⊗[K] Dual K V) ∘ₗ
                  LinearMap.lTensor (Dual K V) (coevaluation K V)) :
            (a : Dual K V) → K →ₗ[K] K ⊗[K] Dual K V)
          ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
            i) :
        K →ₗ[K] K ⊗[K] Dual K V)
      ((LinearMap.compr₂ₛₗ (TensorProduct.mk K (Dual K V) K)
              ((↑(LinearEquiv.symm (TensorProduct.lid K (Dual K V))) : Dual K V →ₗ[K] K ⊗[K] Dual K V) ∘ₗ
                (↑(TensorProduct.rid K (Dual K V)) : Dual K V ⊗[K] K →ₗ[K] Dual K V)) :
            (a : Dual K V) → K →ₗ[K] K ⊗[K] Dual K V)
          ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
            i) :
        K →ₗ[K] K ⊗[K] Dual K V)
⊢ Eq (α := Dual K V →ₗ[K] K →ₗ[K] K ⊗[K] Dual K V)
    (LinearMap.compr₂ₛₗ (TensorProduct.mk K (Dual K V) K)
      (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V))) :
            Dual K V ⊗[K] (V ⊗[K] Dual K V) →ₗ[K] Dual K V ⊗[K] V ⊗[K] Dual K V) ∘ₗ
          LinearMap.lTensor (Dual K V) (coevaluation K V)))
    (LinearMap.compr₂ₛₗ (TensorProduct.mk K (Dual K V) K)
      ((↑(LinearEquiv.symm (TensorProduct.lid K (Dual K V))) : Dual K V →ₗ[K] K ⊗[K] Dual K V) ∘ₗ
        (↑(TensorProduct.rid K (Dual K V)) : Dual K V ⊗[K] K →ₗ[K] Dual K V)))

Tactic:
apply (Basis.ofVectorSpace K V).dualBasis.ext

Premises used: Module.Basis.ofVectorSpace, Module.Basis.dualBasis, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Coevaluation
Goal:
K : Type u
inst : Field K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
this : DecidableEq (↑(Basis.ofVectorSpaceIndex K V) : Type v) :=
  Classical.decEq (↑(Basis.ofVectorSpaceIndex K V) : Type v)
j : (↑(Basis.ofVectorSpaceIndex K V) : Type v)
H :
  Eq (α := K ⊗[K] Dual K V)
    ((((LinearMap.compr₂ₛₗ (TensorProduct.mk K (Dual K V) K)
                (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
                  (↑(LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V))) :
                      Dual K V ⊗[K] (V ⊗[K] Dual K V) →ₗ[K] Dual K V ⊗[K] V ⊗[K] Dual K V) ∘ₗ
                    LinearMap.lTensor (Dual K V) (coevaluation K V)) :
              (a : Dual K V) → K →ₗ[K] K ⊗[K] Dual K V)
            ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
              j) :
          K →ₗ[K] K ⊗[K] Dual K V) :
        (a : K) → K ⊗[K] Dual K V)
      1)
    ((((LinearMap.compr₂ₛₗ (TensorProduct.mk K (Dual K V) K)
                ((↑(LinearEquiv.symm (TensorProduct.lid K (Dual K V))) : Dual K V →ₗ[K] K ⊗[K] Dual K V) ∘ₗ
                  (↑(TensorProduct.rid K (Dual K V)) : Dual K V ⊗[K] K →ₗ[K] Dual K V)) :
              (a : Dual K V) → K →ₗ[K] K ⊗[K] Dual K V)
            ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
              j) :
          K →ₗ[K] K ⊗[K] Dual K V) :
        (a : K) → K ⊗[K] Dual K V)
      1)
⊢ Eq (α := K →ₗ[K] K ⊗[K] Dual K V)
    ((LinearMap.compr₂ₛₗ (TensorProduct.mk K (Dual K V) K)
            (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
              (↑(LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V))) :
                  Dual K V ⊗[K] (V ⊗[K] Dual K V) →ₗ[K] Dual K V ⊗[K] V ⊗[K] Dual K V) ∘ₗ
                LinearMap.lTensor (Dual K V) (coevaluation K V)) :
          (a : Dual K V) → K →ₗ[K] K ⊗[K] Dual K V)
        ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V) j) :
      K →ₗ[K] K ⊗[K] Dual K V)
    ((LinearMap.compr₂ₛₗ (TensorProduct.mk K (Dual K V) K)
            ((↑(LinearEquiv.symm (TensorProduct.lid K (Dual K V))) : Dual K V →ₗ[K] K ⊗[K] Dual K V) ∘ₗ
              (↑(TensorProduct.rid K (Dual K V)) : Dual K V ⊗[K] K →ₗ[K] Dual K V)) :
          (a : Dual K V) → K →ₗ[K] K ⊗[K] Dual K V)
        ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V) j) :
      K →ₗ[K] K ⊗[K] Dual K V)

Tactic:
apply LinearMap.ext_ring

Premises used: LinearMap.ext_ring
-- Module: Mathlib.LinearAlgebra.Coevaluation
Goal:
K : Type u
inst : Field K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
this : DecidableEq (↑(Basis.ofVectorSpaceIndex K V) : Type v) :=
  Classical.decEq (↑(Basis.ofVectorSpaceIndex K V) : Type v)
j : (↑(Basis.ofVectorSpaceIndex K V) : Type v)
H :
  Eq (α := K ⊗[K] Dual K V)
    ((LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
            (↑(LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V))) :
                Dual K V ⊗[K] (V ⊗[K] Dual K V) →ₗ[K] Dual K V ⊗[K] V ⊗[K] Dual K V) ∘ₗ
              LinearMap.lTensor (Dual K V) (coevaluation K V) :
          (a : Dual K V ⊗[K] K) → K ⊗[K] Dual K V)
        ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
            j ⊗ₜ[K]
          1) :
      K ⊗[K] Dual K V)
    (((↑(LinearEquiv.symm (TensorProduct.lid K (Dual K V))) : Dual K V →ₗ[K] K ⊗[K] Dual K V) ∘ₗ
            (↑(TensorProduct.rid K (Dual K V)) : Dual K V ⊗[K] K →ₗ[K] Dual K V) :
          (a : Dual K V ⊗[K] K) → K ⊗[K] Dual K V)
        ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
            j ⊗ₜ[K]
          1) :
      K ⊗[K] Dual K V)
⊢ Eq (α := K ⊗[K] Dual K V)
    ((((LinearMap.compr₂ₛₗ (TensorProduct.mk K (Dual K V) K)
                (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
                  (↑(LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V))) :
                      Dual K V ⊗[K] (V ⊗[K] Dual K V) →ₗ[K] Dual K V ⊗[K] V ⊗[K] Dual K V) ∘ₗ
                    LinearMap.lTensor (Dual K V) (coevaluation K V)) :
              (a : Dual K V) → K →ₗ[K] K ⊗[K] Dual K V)
            ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
              j) :
          K →ₗ[K] K ⊗[K] Dual K V) :
        (a : K) → K ⊗[K] Dual K V)
      1)
    ((((LinearMap.compr₂ₛₗ (TensorProduct.mk K (Dual K V) K)
                ((↑(LinearEquiv.symm (TensorProduct.lid K (Dual K V))) : Dual K V →ₗ[K] K ⊗[K] Dual K V) ∘ₗ
                  (↑(TensorProduct.rid K (Dual K V)) : Dual K V ⊗[K] K →ₗ[K] Dual K V)) :
              (a : Dual K V) → K →ₗ[K] K ⊗[K] Dual K V)
            ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
              j) :
          K →ₗ[K] K ⊗[K] Dual K V) :
        (a : K) → K ⊗[K] Dual K V)
      1)

Tactic:
rw [LinearMap.compr₂ₛₗ_apply, LinearMap.compr₂ₛₗ_apply, TensorProduct.mk_apply]

Premises used: TensorProduct.mk_apply, LinearMap.compr₂ₛₗ_apply
-- Module: Mathlib.LinearAlgebra.Coevaluation
Goal:
K : Type u
inst : Field K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
this : DecidableEq (↑(Basis.ofVectorSpaceIndex K V) : Type v) :=
  Classical.decEq (↑(Basis.ofVectorSpaceIndex K V) : Type v)
j : (↑(Basis.ofVectorSpaceIndex K V) : Type v)
H :
  Eq (α := K ⊗[K] Dual K V)
    ((LinearMap.rTensor (Dual K V) (contractLeft K V) : (a : Dual K V ⊗[K] V ⊗[K] Dual K V) → K ⊗[K] Dual K V)
        ((LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V)) :
            (a : Dual K V ⊗[K] (V ⊗[K] Dual K V)) → Dual K V ⊗[K] V ⊗[K] Dual K V)
          ((LinearMap.lTensor (Dual K V) (coevaluation K V) : (a : Dual K V ⊗[K] K) → Dual K V ⊗[K] (V ⊗[K] Dual K V))
            ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
                j ⊗ₜ[K]
              1))) :
      K ⊗[K] Dual K V)
    (1 ⊗ₜ[K]
        (Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V) j :
      K ⊗[K] Dual K V)
⊢ Eq (α := K ⊗[K] Dual K V)
    ((LinearMap.rTensor (Dual K V) (contractLeft K V) : (a : Dual K V ⊗[K] V ⊗[K] Dual K V) → K ⊗[K] Dual K V)
        ((LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V)) :
            (a : Dual K V ⊗[K] (V ⊗[K] Dual K V)) → Dual K V ⊗[K] V ⊗[K] Dual K V)
          ((LinearMap.lTensor (Dual K V) (coevaluation K V) : (a : Dual K V ⊗[K] K) → Dual K V ⊗[K] (V ⊗[K] Dual K V))
            ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
                j ⊗ₜ[K]
              1))) :
      K ⊗[K] Dual K V)
    ((LinearEquiv.symm (TensorProduct.lid K (Dual K V)) : (a : Dual K V) → K ⊗[K] Dual K V)
        ((TensorProduct.rid K (Dual K V) : (a : Dual K V ⊗[K] K) → Dual K V)
          ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
              j ⊗ₜ[K]
            1)) :
      K ⊗[K] Dual K V)

Tactic:
rw [rid_tmul, one_smul, lid_symm_apply]

Premises used: TensorProduct.lid_symm_apply, one_smul, TensorProduct.rid_tmul
-- Module: Mathlib.LinearAlgebra.Coevaluation
Goal:
K : Type u
inst : Field K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
this : DecidableEq (↑(Basis.ofVectorSpaceIndex K V) : Type v) :=
  Classical.decEq (↑(Basis.ofVectorSpaceIndex K V) : Type v)
j : (↑(Basis.ofVectorSpaceIndex K V) : Type v)
H :
  Eq (α := K ⊗[K] Dual K V)
    ((LinearMap.rTensor (Dual K V) (contractLeft K V) : (a : Dual K V ⊗[K] V ⊗[K] Dual K V) → K ⊗[K] Dual K V)
        ((LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V)) :
            (a : Dual K V ⊗[K] (V ⊗[K] Dual K V)) → Dual K V ⊗[K] V ⊗[K] Dual K V)
          ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
              j ⊗ₜ[K]
            ∑ i : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
              (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) i ⊗ₜ[K]
                Basis.coord (Basis.ofVectorSpace K V) i)) :
      K ⊗[K] Dual K V)
    (1 ⊗ₜ[K]
        (Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V) j :
      K ⊗[K] Dual K V)
⊢ Eq (α := K ⊗[K] Dual K V)
    ((LinearMap.rTensor (Dual K V) (contractLeft K V) : (a : Dual K V ⊗[K] V ⊗[K] Dual K V) → K ⊗[K] Dual K V)
        ((LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V)) :
            (a : Dual K V ⊗[K] (V ⊗[K] Dual K V)) → Dual K V ⊗[K] V ⊗[K] Dual K V)
          ((LinearMap.lTensor (Dual K V) (coevaluation K V) : (a : Dual K V ⊗[K] K) → Dual K V ⊗[K] (V ⊗[K] Dual K V))
            ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
                j ⊗ₜ[K]
              1))) :
      K ⊗[K] Dual K V)
    (1 ⊗ₜ[K]
        (Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V) j :
      K ⊗[K] Dual K V)

Tactic:
simp only [LinearMap.lTensor_tmul, coevaluation_apply_one]

Premises used: coevaluation_apply_one, LinearMap.lTensor_tmul
-- Module: Mathlib.LinearAlgebra.Coevaluation
Goal:
K : Type u
inst : Field K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
this : DecidableEq (↑(Basis.ofVectorSpaceIndex K V) : Type v) :=
  Classical.decEq (↑(Basis.ofVectorSpaceIndex K V) : Type v)
j : (↑(Basis.ofVectorSpaceIndex K V) : Type v)
H :
  Eq (α := K ⊗[K] Dual K V)
    ((LinearMap.rTensor (Dual K V) (contractLeft K V) : (a : Dual K V ⊗[K] V ⊗[K] Dual K V) → K ⊗[K] Dual K V)
        (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
          (LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V)) :
              (a : Dual K V ⊗[K] (V ⊗[K] Dual K V)) → Dual K V ⊗[K] V ⊗[K] Dual K V)
            ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
                j ⊗ₜ[K]
              ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K]
                Basis.coord (Basis.ofVectorSpace K V) x))) :
      K ⊗[K] Dual K V)
    (1 ⊗ₜ[K]
        (Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V) j :
      K ⊗[K] Dual K V)
⊢ Eq (α := K ⊗[K] Dual K V)
    ((LinearMap.rTensor (Dual K V) (contractLeft K V) : (a : Dual K V ⊗[K] V ⊗[K] Dual K V) → K ⊗[K] Dual K V)
        ((LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V)) :
            (a : Dual K V ⊗[K] (V ⊗[K] Dual K V)) → Dual K V ⊗[K] V ⊗[K] Dual K V)
          ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
              j ⊗ₜ[K]
            ∑ i : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
              (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) i ⊗ₜ[K]
                Basis.coord (Basis.ofVectorSpace K V) i)) :
      K ⊗[K] Dual K V)
    (1 ⊗ₜ[K]
        (Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V) j :
      K ⊗[K] Dual K V)

Tactic:
rw [TensorProduct.tmul_sum, map_sum]

Premises used: map_sum, TensorProduct.tmul_sum
-- Module: Mathlib.LinearAlgebra.Coevaluation
Goal:
K : Type u
inst : Field K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
this : DecidableEq (↑(Basis.ofVectorSpaceIndex K V) : Type v) :=
  Classical.decEq (↑(Basis.ofVectorSpaceIndex K V) : Type v)
j : (↑(Basis.ofVectorSpaceIndex K V) : Type v)
H :
  Eq (α := K ⊗[K] Dual K V)
    ((LinearMap.rTensor (Dual K V) (contractLeft K V) : (a : Dual K V ⊗[K] V ⊗[K] Dual K V) → K ⊗[K] Dual K V)
        (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
          (Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
                j ⊗ₜ[K]
              (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K]
            Basis.coord (Basis.ofVectorSpace K V) x) :
      K ⊗[K] Dual K V)
    (1 ⊗ₜ[K]
        (Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V) j :
      K ⊗[K] Dual K V)
⊢ Eq (α := K ⊗[K] Dual K V)
    ((LinearMap.rTensor (Dual K V) (contractLeft K V) : (a : Dual K V ⊗[K] V ⊗[K] Dual K V) → K ⊗[K] Dual K V)
        (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
          (LinearEquiv.symm (TensorProduct.assoc K (Dual K V) V (Dual K V)) :
              (a : Dual K V ⊗[K] (V ⊗[K] Dual K V)) → Dual K V ⊗[K] V ⊗[K] Dual K V)
            ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
                j ⊗ₜ[K]
              ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K]
                Basis.coord (Basis.ofVectorSpace K V) x))) :
      K ⊗[K] Dual K V)
    (1 ⊗ₜ[K]
        (Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V) j :
      K ⊗[K] Dual K V)

Tactic:
simp only [assoc_symm_tmul]

Premises used: TensorProduct.assoc_symm_tmul
-- Module: Mathlib.LinearAlgebra.Coevaluation
Goal:
K : Type u
inst : Field K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
this : DecidableEq (↑(Basis.ofVectorSpaceIndex K V) : Type v) :=
  Classical.decEq (↑(Basis.ofVectorSpaceIndex K V) : Type v)
j : (↑(Basis.ofVectorSpaceIndex K V) : Type v)
H :
  Eq (α := K ⊗[K] Dual K V)
    (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
        (LinearMap.rTensor (Dual K V) (contractLeft K V) : (a : Dual K V ⊗[K] V ⊗[K] Dual K V) → K ⊗[K] Dual K V)
          ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
                j ⊗ₜ[K]
              (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K]
            Basis.coord (Basis.ofVectorSpace K V) x) :
      K ⊗[K] Dual K V)
    (1 ⊗ₜ[K]
        (Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V) j :
      K ⊗[K] Dual K V)
⊢ Eq (α := K ⊗[K] Dual K V)
    ((LinearMap.rTensor (Dual K V) (contractLeft K V) : (a : Dual K V ⊗[K] V ⊗[K] Dual K V) → K ⊗[K] Dual K V)
        (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
          (Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
                j ⊗ₜ[K]
              (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K]
            Basis.coord (Basis.ofVectorSpace K V) x) :
      K ⊗[K] Dual K V)
    (1 ⊗ₜ[K]
        (Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V) j :
      K ⊗[K] Dual K V)

Tactic:
rw [map_sum]

Premises used: map_sum
-- Module: Mathlib.LinearAlgebra.Coevaluation
Goal:
K : Type u
inst : Field K
V : Type v
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
this : DecidableEq (↑(Basis.ofVectorSpaceIndex K V) : Type v) :=
  Classical.decEq (↑(Basis.ofVectorSpaceIndex K V) : Type v)
j : (↑(Basis.ofVectorSpaceIndex K V) : Type v)
H :
  Eq (α := K ⊗[K] Dual K V)
    (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
        (((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V) j :
                Dual K V) :
              (a : V) → K)
            ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x : V) ⊗ₜ[K]
          Basis.coord (Basis.ofVectorSpace K V) x :
      K ⊗[K] Dual K V)
    (1 ⊗ₜ[K]
        (Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V) j :
      K ⊗[K] Dual K V)
⊢ Eq (α := K ⊗[K] Dual K V)
    (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
        (LinearMap.rTensor (Dual K V) (contractLeft K V) : (a : Dual K V ⊗[K] V ⊗[K] Dual K V) → K ⊗[K] Dual K V)
          ((Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V)
                j ⊗ₜ[K]
              (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K]
            Basis.coord (Basis.ofVectorSpace K V) x) :
      K ⊗[K] Dual K V)
    (1 ⊗ₜ[K]
        (Basis.dualBasis (Basis.ofVectorSpace K V) : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → Dual K V) j :
      K ⊗[K] Dual K V)

Tactic:
simp only [LinearMap.rTensor_tmul, contractLeft_apply]

Premises used: LinearMap.rTensor_tmul, contractLeft_apply