no goals
ι : Type u_1
ι' : Type ?u.48727
k : Type u_3
V : Type u_2
P : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i✝ j✝ : ι
e : ι ≃ ι'
i : ι
j : { j // j ≠ i }
⊢ ↑(basisOf b i) j = ↑b ↑j -ᵥ ↑b i
simp [basisOf]