K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ ↑(↑(Basis.constr (Basis.singleton Unit K) K) fun x =>
          ∑ x : ↑(Basis.ofVectorSpaceIndex K V),
            ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x)
      1 =
    ∑ x : ↑(Basis.ofVectorSpaceIndex K V), ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ ↑(coevaluation K V) 1 =
    let bV := Basis.ofVectorSpace K V;
    ∑ i : ↑(Basis.ofVectorSpaceIndex K V), ↑bV i ⊗ₜ[K] Basis.coord bV i
simp only [coevaluation, id]
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ ∑ i : Unit,
      ↑(Basis.equivFun (Basis.singleton Unit K)) 1 i •
        ∑ x : ↑(Basis.ofVectorSpaceIndex K V),
          ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x =
    ∑ x : ↑(Basis.ofVectorSpaceIndex K V), ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ ↑(↑(Basis.constr (Basis.singleton Unit K) K) fun x =>
          ∑ x : ↑(Basis.ofVectorSpaceIndex K V),
            ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x)
      1 =
    ∑ x : ↑(Basis.ofVectorSpaceIndex K V), ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x
rw [(Basis.singleton Unit K).constr_apply_fintype K]
no goals
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
⊢ ∑ i : Unit,
      ↑(Basis.equivFun (Basis.singleton Unit K)) 1 i •
        ∑ x : ↑(Basis.ofVectorSpaceIndex K V),
          ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x =
    ∑ x : ↑(Basis.ofVectorSpaceIndex K V), ↑(Basis.ofVectorSpace K V) x ⊗ₜ[K] Basis.coord (Basis.ofVectorSpace K V) x
simp only [Fintype.univ_punit, Finset.sum_const, one_smul, Basis.singleton_repr,
  Basis.equivFun_apply, Basis.coe_ofVectorSpace, one_nsmul, Finset.card_singleton]