awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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),
      if x = j then 1 ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x else 0)
    (1 ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) j)
have 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)
Tactic: rw [Finset.sum_ite_eq']
-- 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 (α := 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))
have 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)))
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 (α := 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)))
have 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)
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)
⊢ 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)
have 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)
Tactic: apply (Basis.ofVectorSpace K V).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 (α := 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)
have 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)
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 (α := 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)
have 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)
Tactic: simp only [LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_toLinearMap]
-- 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 (α := 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)
have 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)
Tactic: rw [lid_tmul, one_smul, rid_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 (α := 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)
have 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)
Tactic: simp only [LinearMap.rTensor_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 (α := 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)
have 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)
Tactic: rw [TensorProduct.sum_tmul, 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 (α := 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)
have 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)
Tactic: simp only [assoc_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 (α := 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)
have 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)
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 (α := 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)
have 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)
Tactic: simp only [LinearMap.lTensor_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 (α := 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)
have 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)
Tactic: simp only [Basis.coord_apply, Basis.repr_self_apply, TensorProduct.tmul_ite]
-- 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 (α := 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)
have 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)
Tactic: rw [Finset.sum_ite_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Determinant (goal)
Goal:
⊢ Eq (α := ℝ) ((LinearMap.det : (a : ℂ →ₗ[ℝ] ℂ) → ℝ) (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) : ℝ) (-1 : ℝ)
have rw : HMul.hMul (α := ℝ) 1 (-1) - HMul.hMul (α := ℝ) 0 0 = -1
Tactic: rw [← LinearMap.det_toMatrix basisOneI, toMatrix_conjAe, Matrix.det_fin_two_of]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.FiniteDimensional (goal)
Goal:
⊢ finrank ℝ ℂ = 2
have rw : Fintype.card (Fin 2) = 2
Tactic: rw [finrank_eq_card_basis basisOneI, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.FiniteDimensional (goal)
Goal:
rw : Fintype.card (Fin 2) = 2
⊢ finrank ℝ ℂ = 2
have rw₁ : Eq (α := ℕ) 2 2
Tactic: rw [finrank_eq_card_basis basisOneI, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.FiniteDimensional (goal)
Goal:
⊢ Cardinal.lift.{u, 0} (Module.rank ℝ ℂ) = 2
have rw : Cardinal.lift.{u, 0} (↑(finrank ℝ ℂ) : Cardinal.{0}) = 2
Tactic: rw [← finrank_eq_rank, finrank_real_complex, Cardinal.lift_natCast, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.FiniteDimensional (goal)
Goal:
rw : Cardinal.lift.{u, 0} (↑(finrank ℝ ℂ) : Cardinal.{0}) = 2
⊢ Cardinal.lift.{u, 0} (Module.rank ℝ ℂ) = 2
have rw₁ : Cardinal.lift.{u, 0} (↑2 : Cardinal.{0}) = 2
Tactic: rw [← finrank_eq_rank, finrank_real_complex, Cardinal.lift_natCast, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.FiniteDimensional (goal)
Goal:
rw : Cardinal.lift.{u, 0} (↑(finrank ℝ ℂ) : Cardinal.{0}) = 2
rw₁ : Cardinal.lift.{u, 0} (↑2 : Cardinal.{0}) = 2
⊢ Cardinal.lift.{u, 0} (Module.rank ℝ ℂ) = 2
have rw₂ : Eq.{u + 2} (α := Cardinal.{u}) (↑2 : Cardinal.{u}) 2
Tactic: rw [← finrank_eq_rank, finrank_real_complex, Cardinal.lift_natCast, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.FiniteDimensional (goal)
Goal:
rw : Cardinal.lift.{u, 0} (↑(finrank ℝ ℂ) : Cardinal.{0}) = 2
rw₁ : Cardinal.lift.{u, 0} (↑2 : Cardinal.{0}) = 2
rw₂ : Eq.{u + 2} (α := Cardinal.{u}) (↑2 : Cardinal.{u}) 2
⊢ Cardinal.lift.{u, 0} (Module.rank ℝ ℂ) = 2
have rw₃ : Eq.{u + 2} (α := Cardinal.{u}) 2 2
Tactic: rw [← finrank_eq_rank, finrank_real_complex, Cardinal.lift_natCast, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.FiniteDimensional (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℂ E
⊢ Cardinal.lift.{0, u_1} (Module.rank ℝ E) = Cardinal.lift.{0, u_1} (2 * Module.rank ℂ E)
have rw : 2 * Cardinal.lift.{0, u_1} (Module.rank ℂ E) = Cardinal.lift.{0, u_1} (2 * Module.rank ℂ E)
Tactic: rw [← lift_rank_mul_lift_rank ℝ ℂ E, Complex.rank_real_complex']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.FiniteDimensional (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℂ E
⊢ finrank ℝ E = 2 * finrank ℂ E
have rw : finrank ℝ ℂ * finrank ℂ E = 2 * finrank ℂ E
Tactic: rw [← Module.finrank_mul_finrank ℝ ℂ E, Complex.finrank_real_complex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.FiniteDimensional (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℂ E
rw : finrank ℝ ℂ * finrank ℂ E = 2 * finrank ℂ E
⊢ finrank ℝ E = 2 * finrank ℂ E
have rw₁ : 2 * finrank ℂ E = 2 * finrank ℂ E
Tactic: rw [← Module.finrank_mul_finrank ℝ ℂ E, Complex.finrank_real_complex]