awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Star (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
r : R
rw :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((involute : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
rw₁ :
  Eq (α := CliffordAlgebra Q)
    ((reverse : (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) :
      CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
⊢ Eq (α := CliffordAlgebra Q)
    (star ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r) : CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
have rw₂ : Eq (α := CliffordAlgebra Q) ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
  ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
Tactic: rw [star_def, involute.commutes, reverse.commutes]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Coevaluation (goal)
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)
    (((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)
have 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)
Tactic: rw [(Basis.singleton Unit K).constr_apply_fintype K]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Coevaluation (goal)
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)
⊢ 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))
have 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)))
Tactic: apply TensorProduct.ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Coevaluation (goal)
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)
⊢ 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)))
have 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)
Tactic: apply (Basis.ofVectorSpace K V).dualBasis.ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Coevaluation (goal)
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] 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)
have 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)
Tactic: apply LinearMap.ext_ring
-- Lean 4 proof step from Mathlib.LinearAlgebra.Coevaluation (goal)
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)
    ((((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)
have 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)
Tactic: rw [LinearMap.compr₂ₛₗ_apply, LinearMap.compr₂ₛₗ_apply, TensorProduct.mk_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Coevaluation (goal)
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)
    ((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)
have 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)
Tactic: rw [rid_tmul, one_smul, lid_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Coevaluation (goal)
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)
    ((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)
have 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)
Tactic: simp only [LinearMap.lTensor_tmul, coevaluation_apply_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Coevaluation (goal)
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)
    ((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)
have 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)
Tactic: rw [TensorProduct.tmul_sum, map_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Coevaluation (goal)
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)
    ((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)
have 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)
Tactic: simp only [assoc_symm_tmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Coevaluation (goal)
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)
    ((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)
have 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)
Tactic: rw [map_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Coevaluation (goal)
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)
    (∑ 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)
have 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)
Tactic: simp only [LinearMap.rTensor_tmul, contractLeft_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Coevaluation (goal)
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)
    (∑ 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)
have 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)
Tactic: simp only [Basis.coe_dualBasis, Basis.coord_apply, Basis.repr_self_apply, TensorProduct.ite_tmul]