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
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),
      if x = j then 1 ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x else 0)
    (1 ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) j)
⊢ 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)

Tactic:
simp only [Basis.coe_dualBasis, Basis.coord_apply, Basis.repr_self_apply, TensorProduct.ite_tmul]

Premises used: Module.Basis.coe_dualBasis, Module.Basis.repr_self_apply, TensorProduct.ite_tmul, Module.Basis.coord_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)
    (if Membership.mem (γ := Finset (↑(Basis.ofVectorSpaceIndex K V) : Type v)) Finset.univ j then
      1 ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) j
    else 0)
    (1 ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) j)
⊢ Eq (α := K ⊗[K] Dual K V)
    (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
      if x = j then 1 ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x else 0)
    (1 ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) j)

Tactic:
rw [Finset.sum_ite_eq']

Premises used: Finset.sum_ite_eq'
-- 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)
⊢ Eq (α := K ⊗[K] Dual K V)
    (if Membership.mem (γ := Finset (↑(Basis.ofVectorSpaceIndex K V) : Type v)) Finset.univ j then
      1 ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) j
    else 0)
    (1 ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) j)

Tactic:
simp only [Finset.mem_univ, if_true]

Premises used: Finset.mem_univ, if_true
-- 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 (α := K →ₗ[K] V →ₗ[K] V ⊗[K] K)
    (LinearMap.compr₂ₛₗ (TensorProduct.mk K K V)
      (LinearMap.lTensor V (contractLeft K V) ∘ₗ
        (↑(TensorProduct.assoc K V (Dual K V) V) : V ⊗[K] Dual K V ⊗[K] V →ₗ[K] V ⊗[K] (Dual K V ⊗[K] V)) ∘ₗ
          LinearMap.rTensor V (coevaluation K V)))
    (LinearMap.compr₂ₛₗ (TensorProduct.mk K K V)
      ((↑(LinearEquiv.symm (TensorProduct.rid K V)) : V →ₗ[K] V ⊗[K] K) ∘ₗ
        (↑(TensorProduct.lid K V) : K ⊗[K] V →ₗ[K] V)))
⊢ Eq (α := K ⊗[K] V →ₗ[K] V ⊗[K] K)
    (LinearMap.lTensor V (contractLeft K V) ∘ₗ
      (↑(TensorProduct.assoc K V (Dual K V) V) : V ⊗[K] Dual K V ⊗[K] V →ₗ[K] V ⊗[K] (Dual K V ⊗[K] V)) ∘ₗ
        LinearMap.rTensor V (coevaluation K V))
    ((↑(LinearEquiv.symm (TensorProduct.rid K V)) : V →ₗ[K] V ⊗[K] K) ∘ₗ (↑(TensorProduct.lid K V) : K ⊗[K] V →ₗ[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 :
  Eq (α := V →ₗ[K] V ⊗[K] K)
    ((LinearMap.compr₂ₛₗ (TensorProduct.mk K K V)
          (LinearMap.lTensor V (contractLeft K V) ∘ₗ
            (↑(TensorProduct.assoc K V (Dual K V) V) : V ⊗[K] Dual K V ⊗[K] V →ₗ[K] V ⊗[K] (Dual K V ⊗[K] V)) ∘ₗ
              LinearMap.rTensor V (coevaluation K V)) :
        (a : K) → V →ₗ[K] V ⊗[K] K)
      1)
    ((LinearMap.compr₂ₛₗ (TensorProduct.mk K K V)
          ((↑(LinearEquiv.symm (TensorProduct.rid K V)) : V →ₗ[K] V ⊗[K] K) ∘ₗ
            (↑(TensorProduct.lid K V) : K ⊗[K] V →ₗ[K] V)) :
        (a : K) → V →ₗ[K] V ⊗[K] K)
      1)
⊢ Eq (α := K →ₗ[K] V →ₗ[K] V ⊗[K] K)
    (LinearMap.compr₂ₛₗ (TensorProduct.mk K K V)
      (LinearMap.lTensor V (contractLeft K V) ∘ₗ
        (↑(TensorProduct.assoc K V (Dual K V) V) : V ⊗[K] Dual K V ⊗[K] V →ₗ[K] V ⊗[K] (Dual K V ⊗[K] V)) ∘ₗ
          LinearMap.rTensor V (coevaluation K V)))
    (LinearMap.compr₂ₛₗ (TensorProduct.mk K K V)
      ((↑(LinearEquiv.symm (TensorProduct.rid K V)) : V →ₗ[K] V ⊗[K] K) ∘ₗ
        (↑(TensorProduct.lid K V) : K ⊗[K] V →ₗ[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)
H :
  ∀ (i : (↑(Basis.ofVectorSpaceIndex K V) : Type v)),
    Eq (α := V ⊗[K] K)
      (((LinearMap.compr₂ₛₗ (TensorProduct.mk K K V)
                  (LinearMap.lTensor V (contractLeft K V) ∘ₗ
                    (↑(TensorProduct.assoc K V (Dual K V) V) : V ⊗[K] Dual K V ⊗[K] V →ₗ[K] V ⊗[K] (Dual K V ⊗[K] V)) ∘ₗ
                      LinearMap.rTensor V (coevaluation K V)) :
                (a : K) → V →ₗ[K] V ⊗[K] K)
              1 :
            (a : V) → V ⊗[K] K)
          ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) i) :
        V ⊗[K] K)
      (((LinearMap.compr₂ₛₗ (TensorProduct.mk K K V)
                  ((↑(LinearEquiv.symm (TensorProduct.rid K V)) : V →ₗ[K] V ⊗[K] K) ∘ₗ
                    (↑(TensorProduct.lid K V) : K ⊗[K] V →ₗ[K] V)) :
                (a : K) → V →ₗ[K] V ⊗[K] K)
              1 :
            (a : V) → V ⊗[K] K)
          ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) i) :
        V ⊗[K] K)
⊢ Eq (α := V →ₗ[K] V ⊗[K] K)
    ((LinearMap.compr₂ₛₗ (TensorProduct.mk K K V)
          (LinearMap.lTensor V (contractLeft K V) ∘ₗ
            (↑(TensorProduct.assoc K V (Dual K V) V) : V ⊗[K] Dual K V ⊗[K] V →ₗ[K] V ⊗[K] (Dual K V ⊗[K] V)) ∘ₗ
              LinearMap.rTensor V (coevaluation K V)) :
        (a : K) → V →ₗ[K] V ⊗[K] K)
      1)
    ((LinearMap.compr₂ₛₗ (TensorProduct.mk K K V)
          ((↑(LinearEquiv.symm (TensorProduct.rid K V)) : V →ₗ[K] V ⊗[K] K) ∘ₗ
            (↑(TensorProduct.lid K V) : K ⊗[K] V →ₗ[K] V)) :
        (a : K) → V →ₗ[K] V ⊗[K] K)
      1)

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

Premises used: Module.Basis.ofVectorSpace, 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 (α := V ⊗[K] K)
    ((LinearMap.lTensor V (contractLeft K V) ∘ₗ
            (↑(TensorProduct.assoc K V (Dual K V) V) : V ⊗[K] Dual K V ⊗[K] V →ₗ[K] V ⊗[K] (Dual K V ⊗[K] V)) ∘ₗ
              LinearMap.rTensor V (coevaluation K V) :
          (a : K ⊗[K] V) → V ⊗[K] K)
        (1 ⊗ₜ[K] (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j) :
      V ⊗[K] K)
    (((↑(LinearEquiv.symm (TensorProduct.rid K V)) : V →ₗ[K] V ⊗[K] K) ∘ₗ
            (↑(TensorProduct.lid K V) : K ⊗[K] V →ₗ[K] V) :
          (a : K ⊗[K] V) → V ⊗[K] K)
        (1 ⊗ₜ[K] (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j) :
      V ⊗[K] K)
⊢ Eq (α := V ⊗[K] K)
    (((LinearMap.compr₂ₛₗ (TensorProduct.mk K K V)
                (LinearMap.lTensor V (contractLeft K V) ∘ₗ
                  (↑(TensorProduct.assoc K V (Dual K V) V) : V ⊗[K] Dual K V ⊗[K] V →ₗ[K] V ⊗[K] (Dual K V ⊗[K] V)) ∘ₗ
                    LinearMap.rTensor V (coevaluation K V)) :
              (a : K) → V →ₗ[K] V ⊗[K] K)
            1 :
          (a : V) → V ⊗[K] K)
        ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j) :
      V ⊗[K] K)
    (((LinearMap.compr₂ₛₗ (TensorProduct.mk K K V)
                ((↑(LinearEquiv.symm (TensorProduct.rid K V)) : V →ₗ[K] V ⊗[K] K) ∘ₗ
                  (↑(TensorProduct.lid K V) : K ⊗[K] V →ₗ[K] V)) :
              (a : K) → V →ₗ[K] V ⊗[K] K)
            1 :
          (a : V) → V ⊗[K] K)
        ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j) :
      V ⊗[K] K)

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 (α := V ⊗[K] K)
    ((LinearMap.lTensor V (contractLeft K V) : (a : V ⊗[K] (Dual K V ⊗[K] V)) → V ⊗[K] K)
        ((TensorProduct.assoc K V (Dual K V) V : (a : V ⊗[K] Dual K V ⊗[K] V) → V ⊗[K] (Dual K V ⊗[K] V))
          ((LinearMap.rTensor V (coevaluation K V) : (a : K ⊗[K] V) → V ⊗[K] Dual K V ⊗[K] V)
            (1 ⊗ₜ[K] (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j))) :
      V ⊗[K] K)
    ((LinearEquiv.symm (TensorProduct.rid K V) : (a : V) → V ⊗[K] K)
        ((TensorProduct.lid K V : (a : K ⊗[K] V) → V)
          (1 ⊗ₜ[K] (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j : K ⊗[K] V)) :
      V ⊗[K] K)
⊢ Eq (α := V ⊗[K] K)
    ((LinearMap.lTensor V (contractLeft K V) ∘ₗ
            (↑(TensorProduct.assoc K V (Dual K V) V) : V ⊗[K] Dual K V ⊗[K] V →ₗ[K] V ⊗[K] (Dual K V ⊗[K] V)) ∘ₗ
              LinearMap.rTensor V (coevaluation K V) :
          (a : K ⊗[K] V) → V ⊗[K] K)
        (1 ⊗ₜ[K] (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j) :
      V ⊗[K] K)
    (((↑(LinearEquiv.symm (TensorProduct.rid K V)) : V →ₗ[K] V ⊗[K] K) ∘ₗ
            (↑(TensorProduct.lid K V) : K ⊗[K] V →ₗ[K] V) :
          (a : K ⊗[K] V) → V ⊗[K] K)
        (1 ⊗ₜ[K] (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j) :
      V ⊗[K] K)

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

Premises used: LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_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 (α := V ⊗[K] K)
    ((LinearMap.lTensor V (contractLeft K V) : (a : V ⊗[K] (Dual K V ⊗[K] V)) → V ⊗[K] K)
        ((TensorProduct.assoc K V (Dual K V) V : (a : V ⊗[K] Dual K V ⊗[K] V) → V ⊗[K] (Dual K V ⊗[K] V))
          ((LinearMap.rTensor V (coevaluation K V) : (a : K ⊗[K] V) → V ⊗[K] Dual K V ⊗[K] V)
            (1 ⊗ₜ[K] (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j))) :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)
⊢ Eq (α := V ⊗[K] K)
    ((LinearMap.lTensor V (contractLeft K V) : (a : V ⊗[K] (Dual K V ⊗[K] V)) → V ⊗[K] K)
        ((TensorProduct.assoc K V (Dual K V) V : (a : V ⊗[K] Dual K V ⊗[K] V) → V ⊗[K] (Dual K V ⊗[K] V))
          ((LinearMap.rTensor V (coevaluation K V) : (a : K ⊗[K] V) → V ⊗[K] Dual K V ⊗[K] V)
            (1 ⊗ₜ[K] (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j))) :
      V ⊗[K] K)
    ((LinearEquiv.symm (TensorProduct.rid K V) : (a : V) → V ⊗[K] K)
        ((TensorProduct.lid K V : (a : K ⊗[K] V) → V)
          (1 ⊗ₜ[K] (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j : K ⊗[K] V)) :
      V ⊗[K] K)

Tactic:
rw [lid_tmul, one_smul, rid_symm_apply]

Premises used: TensorProduct.lid_tmul, one_smul, TensorProduct.rid_symm_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 (α := V ⊗[K] K)
    ((LinearMap.lTensor V (contractLeft K V) : (a : V ⊗[K] (Dual K V ⊗[K] V)) → V ⊗[K] K)
        ((TensorProduct.assoc K V (Dual K V) V : (a : V ⊗[K] Dual K V ⊗[K] V) → V ⊗[K] (Dual K V ⊗[K] V))
          ((∑ 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]
            (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j)) :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)
⊢ Eq (α := V ⊗[K] K)
    ((LinearMap.lTensor V (contractLeft K V) : (a : V ⊗[K] (Dual K V ⊗[K] V)) → V ⊗[K] K)
        ((TensorProduct.assoc K V (Dual K V) V : (a : V ⊗[K] Dual K V ⊗[K] V) → V ⊗[K] (Dual K V ⊗[K] V))
          ((LinearMap.rTensor V (coevaluation K V) : (a : K ⊗[K] V) → V ⊗[K] Dual K V ⊗[K] V)
            (1 ⊗ₜ[K] (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j))) :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)

Tactic:
simp only [LinearMap.rTensor_tmul, coevaluation_apply_one]

Premises used: LinearMap.rTensor_tmul, coevaluation_apply_one
-- 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 (α := V ⊗[K] K)
    ((LinearMap.lTensor V (contractLeft K V) : (a : V ⊗[K] (Dual K V ⊗[K] V)) → V ⊗[K] K)
        (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
          (TensorProduct.assoc K V (Dual K V) V : (a : V ⊗[K] Dual K V ⊗[K] V) → V ⊗[K] (Dual K V ⊗[K] V))
            ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K]
                Basis.coord (Basis.ofVectorSpace K V) x ⊗ₜ[K]
              (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j)) :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)
⊢ Eq (α := V ⊗[K] K)
    ((LinearMap.lTensor V (contractLeft K V) : (a : V ⊗[K] (Dual K V ⊗[K] V)) → V ⊗[K] K)
        ((TensorProduct.assoc K V (Dual K V) V : (a : V ⊗[K] Dual K V ⊗[K] V) → V ⊗[K] (Dual K V ⊗[K] V))
          ((∑ 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]
            (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j)) :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)

Tactic:
rw [TensorProduct.sum_tmul, map_sum]

Premises used: map_sum, TensorProduct.sum_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 (α := V ⊗[K] K)
    ((LinearMap.lTensor V (contractLeft K V) : (a : V ⊗[K] (Dual K V ⊗[K] V)) → V ⊗[K] K)
        (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
          (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K]
            (Basis.coord (Basis.ofVectorSpace K V) x ⊗ₜ[K]
              (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j)) :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)
⊢ Eq (α := V ⊗[K] K)
    ((LinearMap.lTensor V (contractLeft K V) : (a : V ⊗[K] (Dual K V ⊗[K] V)) → V ⊗[K] K)
        (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
          (TensorProduct.assoc K V (Dual K V) V : (a : V ⊗[K] Dual K V ⊗[K] V) → V ⊗[K] (Dual K V ⊗[K] V))
            ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K]
                Basis.coord (Basis.ofVectorSpace K V) x ⊗ₜ[K]
              (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j)) :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)

Tactic:
simp only [assoc_tmul]

Premises used: TensorProduct.assoc_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 (α := V ⊗[K] K)
    (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
        (LinearMap.lTensor V (contractLeft K V) : (a : V ⊗[K] (Dual K V ⊗[K] V)) → V ⊗[K] K)
          ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K]
            (Basis.coord (Basis.ofVectorSpace K V) x ⊗ₜ[K]
              (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j)) :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)
⊢ Eq (α := V ⊗[K] K)
    ((LinearMap.lTensor V (contractLeft K V) : (a : V ⊗[K] (Dual K V ⊗[K] V)) → V ⊗[K] K)
        (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
          (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K]
            (Basis.coord (Basis.ofVectorSpace K V) x ⊗ₜ[K]
              (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j)) :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)

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 (α := V ⊗[K] K)
    (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
        (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K]
          (Basis.coord (Basis.ofVectorSpace K V) x : (a : V) → K)
            ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j : V) :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)
⊢ Eq (α := V ⊗[K] K)
    (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
        (LinearMap.lTensor V (contractLeft K V) : (a : V ⊗[K] (Dual K V ⊗[K] V)) → V ⊗[K] K)
          ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K]
            (Basis.coord (Basis.ofVectorSpace K V) x ⊗ₜ[K]
              (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j)) :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)

Tactic:
simp only [LinearMap.lTensor_tmul, contractLeft_apply]

Premises used: contractLeft_apply, 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 (α := V ⊗[K] K)
    (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
        if j = x then (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K] 1
        else 0 :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)
⊢ Eq (α := V ⊗[K] K)
    (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
        (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K]
          (Basis.coord (Basis.ofVectorSpace K V) x : (a : V) → K)
            ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j : V) :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)

Tactic:
simp only [Basis.coord_apply, Basis.repr_self_apply, TensorProduct.tmul_ite]

Premises used: Module.Basis.repr_self_apply, TensorProduct.tmul_ite, Module.Basis.coord_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 (α := V ⊗[K] K)
    (if Membership.mem (γ := Finset (↑(Basis.ofVectorSpaceIndex K V) : Type v)) Finset.univ j then
        (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1
      else 0 :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)
⊢ Eq (α := V ⊗[K] K)
    (∑ x : (↑(Basis.ofVectorSpaceIndex K V) : Type v),
        if j = x then (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) x ⊗ₜ[K] 1
        else 0 :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)

Tactic:
rw [Finset.sum_ite_eq]

Premises used: Finset.sum_ite_eq
-- 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)
⊢ Eq (α := V ⊗[K] K)
    (if Membership.mem (γ := Finset (↑(Basis.ofVectorSpaceIndex K V) : Type v)) Finset.univ j then
        (Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1
      else 0 :
      V ⊗[K] K)
    ((Basis.ofVectorSpace K V : (a : (↑(Basis.ofVectorSpaceIndex K V) : Type v)) → V) j ⊗ₜ[K] 1 : V ⊗[K] K)

Tactic:
simp only [Finset.mem_univ, if_true]

Premises used: Finset.mem_univ, if_true