K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
⊢ LinearMap.comp (LinearMap.lTensor V (contractLeft K V))
      (LinearMap.comp (↑(TensorProduct.assoc K V (Module.Dual K V) V)) (LinearMap.rTensor V (coevaluation K V))) =
    LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.rid K V)) ↑(TensorProduct.lid K V)
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ LinearMap.comp (LinearMap.lTensor V (contractLeft K V))
      (LinearMap.comp (↑(TensorProduct.assoc K V (Module.Dual K V) V)) (LinearMap.rTensor V (coevaluation K V))) =
    LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.rid K V)) ↑(TensorProduct.lid K V)
letI := Classical.decEq (Basis.ofVectorSpaceIndex K V)
case H
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
⊢ LinearMap.compr₂ (mk K K V)
      (LinearMap.comp (LinearMap.lTensor V (contractLeft K V))
        (LinearMap.comp (↑(TensorProduct.assoc K V (Module.Dual K V) V)) (LinearMap.rTensor V (coevaluation K V)))) =
    LinearMap.compr₂ (mk K K V) (LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.rid K V)) ↑(TensorProduct.lid K V))
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
⊢ LinearMap.comp (LinearMap.lTensor V (contractLeft K V))
      (LinearMap.comp (↑(TensorProduct.assoc K V (Module.Dual K V) V)) (LinearMap.rTensor V (coevaluation K V))) =
    LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.rid K V)) ↑(TensorProduct.lid K V)
apply TensorProduct.ext
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(LinearMap.compr₂ (mk K K V)
          (LinearMap.comp (LinearMap.lTensor V (contractLeft K V))
            (LinearMap.comp (↑(TensorProduct.assoc K V (Module.Dual K V) V)) (LinearMap.rTensor V (coevaluation K V)))))
      1 =
    ↑(LinearMap.compr₂ (mk K K V) (LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.rid K V)) ↑(TensorProduct.lid K V)))
      1
case H
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
⊢ LinearMap.compr₂ (mk K K V)
      (LinearMap.comp (LinearMap.lTensor V (contractLeft K V))
        (LinearMap.comp (↑(TensorProduct.assoc K V (Module.Dual K V) V)) (LinearMap.rTensor V (coevaluation K V)))) =
    LinearMap.compr₂ (mk K K V) (LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.rid K V)) ↑(TensorProduct.lid K V))
apply LinearMap.ext_ring
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
⊢ ∀ (i : ↑(Basis.ofVectorSpaceIndex K V)),
    ↑(↑(LinearMap.compr₂ (mk K K V)
                (LinearMap.comp (LinearMap.lTensor V (contractLeft K V))
                  (LinearMap.comp (↑(TensorProduct.assoc K V (Module.Dual K V) V))
                    (LinearMap.rTensor V (coevaluation K V)))))
            1)
        (↑(Basis.ofVectorSpace K V) i) =
      ↑(↑(LinearMap.compr₂ (mk K K V)
                (LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.rid K V)) ↑(TensorProduct.lid K V)))
            1)
        (↑(Basis.ofVectorSpace K V) i)
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(LinearMap.compr₂ (mk K K V)
          (LinearMap.comp (LinearMap.lTensor V (contractLeft K V))
            (LinearMap.comp (↑(TensorProduct.assoc K V (Module.Dual K V) V)) (LinearMap.rTensor V (coevaluation K V)))))
      1 =
    ↑(LinearMap.compr₂ (mk K K V) (LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.rid K V)) ↑(TensorProduct.lid K V)))
      1
apply (Basis.ofVectorSpace K V).ext
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(↑(LinearMap.compr₂ (mk K K V)
              (LinearMap.comp (LinearMap.lTensor V (contractLeft K V))
                (LinearMap.comp (↑(TensorProduct.assoc K V (Module.Dual K V) V))
                  (LinearMap.rTensor V (coevaluation K V)))))
          1)
      (↑(Basis.ofVectorSpace K V) j) =
    ↑(↑(LinearMap.compr₂ (mk K K V)
              (LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.rid K V)) ↑(TensorProduct.lid K V)))
          1)
      (↑(Basis.ofVectorSpace K V) j)
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
⊢ ∀ (i : ↑(Basis.ofVectorSpaceIndex K V)),
    ↑(↑(LinearMap.compr₂ (mk K K V)
                (LinearMap.comp (LinearMap.lTensor V (contractLeft K V))
                  (LinearMap.comp (↑(TensorProduct.assoc K V (Module.Dual K V) V))
                    (LinearMap.rTensor V (coevaluation K V)))))
            1)
        (↑(Basis.ofVectorSpace K V) i) =
      ↑(↑(LinearMap.compr₂ (mk K K V)
                (LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.rid K V)) ↑(TensorProduct.lid K V)))
            1)
        (↑(Basis.ofVectorSpace K V) i)
intro j
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(LinearMap.comp (LinearMap.lTensor V (contractLeft K V))
          (LinearMap.comp (↑(TensorProduct.assoc K V (Module.Dual K V) V)) (LinearMap.rTensor V (coevaluation K V))))
      (1 ⊗ₜ[K] ↑(Basis.ofVectorSpace K V) j) =
    ↑(LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.rid K V)) ↑(TensorProduct.lid K V))
      (1 ⊗ₜ[K] ↑(Basis.ofVectorSpace K V) j)
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(↑(LinearMap.compr₂ (mk K K V)
              (LinearMap.comp (LinearMap.lTensor V (contractLeft K V))
                (LinearMap.comp (↑(TensorProduct.assoc K V (Module.Dual K V) V))
                  (LinearMap.rTensor V (coevaluation K V)))))
          1)
      (↑(Basis.ofVectorSpace K V) j) =
    ↑(↑(LinearMap.compr₂ (mk K K V)
              (LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.rid K V)) ↑(TensorProduct.lid K V)))
          1)
      (↑(Basis.ofVectorSpace K V) j)
rw [LinearMap.compr₂_apply, LinearMap.compr₂_apply, TensorProduct.mk_apply]
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(LinearMap.lTensor V (contractLeft K V))
      (↑(TensorProduct.assoc K V (Module.Dual K V) V)
        (↑(LinearMap.rTensor V (coevaluation K V)) (1 ⊗ₜ[K] ↑(Basis.ofVectorSpace K V) j))) =
    ↑(LinearEquiv.symm (TensorProduct.rid K V)) (↑(TensorProduct.lid K V) (1 ⊗ₜ[K] ↑(Basis.ofVectorSpace K V) j))
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(LinearMap.comp (LinearMap.lTensor V (contractLeft K V))
          (LinearMap.comp (↑(TensorProduct.assoc K V (Module.Dual K V) V)) (LinearMap.rTensor V (coevaluation K V))))
      (1 ⊗ₜ[K] ↑(Basis.ofVectorSpace K V) j) =
    ↑(LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.rid K V)) ↑(TensorProduct.lid K V))
      (1 ⊗ₜ[K] ↑(Basis.ofVectorSpace K V) j)
simp only [LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_toLinearMap]
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(LinearMap.lTensor V (contractLeft K V))
      (↑(TensorProduct.assoc K V (Module.Dual K V) V)
        (↑(LinearMap.rTensor V (coevaluation K V)) (1 ⊗ₜ[K] ↑(Basis.ofVectorSpace K V) j))) =
    ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(LinearMap.lTensor V (contractLeft K V))
      (↑(TensorProduct.assoc K V (Module.Dual K V) V)
        (↑(LinearMap.rTensor V (coevaluation K V)) (1 ⊗ₜ[K] ↑(Basis.ofVectorSpace K V) j))) =
    ↑(LinearEquiv.symm (TensorProduct.rid K V)) (↑(TensorProduct.lid K V) (1 ⊗ₜ[K] ↑(Basis.ofVectorSpace K V) j))
rw [lid_tmul, one_smul, rid_symm_apply]
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(LinearMap.lTensor V (contractLeft K V))
      (↑(TensorProduct.assoc K V (Module.Dual K V) V)
        ((∑ x : ↑(Basis.ofVectorSpaceIndex K V),
            ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x) ⊗ₜ[K]
          ↑(Basis.ofVectorSpace K V) j)) =
    ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(LinearMap.lTensor V (contractLeft K V))
      (↑(TensorProduct.assoc K V (Module.Dual K V) V)
        (↑(LinearMap.rTensor V (coevaluation K V)) (1 ⊗ₜ[K] ↑(Basis.ofVectorSpace K V) j))) =
    ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
simp only [LinearEquiv.coe_toLinearMap, LinearMap.rTensor_tmul, coevaluation_apply_one]
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(LinearMap.lTensor V (contractLeft K V))
      (∑ i : ↑(Basis.ofVectorSpaceIndex K V),
        ↑(TensorProduct.assoc K V (Module.Dual K V) V)
          ((↑(Basis.ofVectorSpace K V) i ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) i) ⊗ₜ[K]
            ↑(Basis.ofVectorSpace K V) j)) =
    ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(LinearMap.lTensor V (contractLeft K V))
      (↑(TensorProduct.assoc K V (Module.Dual K V) V)
        ((∑ x : ↑(Basis.ofVectorSpaceIndex K V),
            ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x) ⊗ₜ[K]
          ↑(Basis.ofVectorSpace K V) j)) =
    ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
rw [TensorProduct.sum_tmul, LinearEquiv.map_sum]
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(LinearMap.lTensor V (contractLeft K V))
      (∑ x : ↑(Basis.ofVectorSpaceIndex K V),
        ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x ⊗ₜ[K] ↑(Basis.ofVectorSpace K V) j) =
    ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(LinearMap.lTensor V (contractLeft K V))
      (∑ i : ↑(Basis.ofVectorSpaceIndex K V),
        ↑(TensorProduct.assoc K V (Module.Dual K V) V)
          ((↑(Basis.ofVectorSpace K V) i ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) i) ⊗ₜ[K]
            ↑(Basis.ofVectorSpace K V) j)) =
    ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
simp only [assoc_tmul]
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ∑ i : ↑(Basis.ofVectorSpaceIndex K V),
      ↑(LinearMap.lTensor V (contractLeft K V))
        (↑(Basis.ofVectorSpace K V) i ⊗ₜ[K]
          Basis.coord (Basis.ofVectorSpace K V) i ⊗ₜ[K] ↑(Basis.ofVectorSpace K V) j) =
    ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(LinearMap.lTensor V (contractLeft K V))
      (∑ x : ↑(Basis.ofVectorSpaceIndex K V),
        ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x ⊗ₜ[K] ↑(Basis.ofVectorSpace K V) j) =
    ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
rw [LinearMap.map_sum]
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ∑ x : ↑(Basis.ofVectorSpaceIndex K V),
      ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] ↑(Basis.coord (Basis.ofVectorSpace K V) x) (↑(Basis.ofVectorSpace K V) j) =
    ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ∑ i : ↑(Basis.ofVectorSpaceIndex K V),
      ↑(LinearMap.lTensor V (contractLeft K V))
        (↑(Basis.ofVectorSpace K V) i ⊗ₜ[K]
          Basis.coord (Basis.ofVectorSpace K V) i ⊗ₜ[K] ↑(Basis.ofVectorSpace K V) j) =
    ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
simp only [LinearMap.lTensor_tmul, contractLeft_apply]
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (∑ x : ↑(Basis.ofVectorSpaceIndex K V), if j = x then ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] 1 else 0) =
    ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ∑ x : ↑(Basis.ofVectorSpaceIndex K V),
      ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] ↑(Basis.coord (Basis.ofVectorSpace K V) x) (↑(Basis.ofVectorSpace K V) j) =
    ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
simp only [Basis.coord_apply, Basis.repr_self_apply, TensorProduct.tmul_ite]
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (if j ∈ Finset.univ then ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1 else 0) = ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (∑ x : ↑(Basis.ofVectorSpaceIndex K V), if j = x then ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] 1 else 0) =
    ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
rw [Finset.sum_ite_eq]
no goals
case H.h
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (if j ∈ Finset.univ then ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1 else 0) = ↑(Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
simp only [Finset.mem_univ, if_true]