no goals
ι : Type u_1
ι' : Type ?u.94243
k : Type u_2
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 : ι ≃ ι'
h : i ≠ j
⊢ ↑(coord b i) (↑b j) = 0
rw [coord, AffineMap.coe_mk, ← @Subtype.coe_mk _ (fun j => j ≠ i) j h.symm, ← b.basisOf_apply,
  Basis.sumCoords_self_apply, sub_self]