no goals
k : Type u_2
V : Type u_3
P : Type u_1
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type ?u.480542
s₂ : Finset ι₂
p : ι → P
i : ι
⊢ centroid k {i} p = p i
simp [centroid_def, affineCombination_apply]