no goals
ι : Type u_2
ι' : Type ?u.90092
k : Type u_1
V : Type u_4
P : Type u_3
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j : ι
e : ι ≃ ι'
i : ι
⊢ ↑(coord b i) (↑b i) = 1
simp only [coord, Basis.coe_sumCoords, LinearEquiv.map_zero, LinearEquiv.coe_coe, sub_zero,
  AffineMap.coe_mk, Finsupp.sum_zero_index, vsub_self]