no goals
ι : Type u_2
ι' : Type ?u.181001
k : Type u_1
V : Type u_3
P : Type u_4
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : DivisionRing k
inst✝¹ : Module k V
inst✝ : CharZero k
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
⊢ ↑(coord b i) (Finset.centroid k s ↑b) = (↑(Finset.card s))⁻¹
rw [Finset.centroid,
  b.coord_apply_combination_of_mem hi (s.sum_centroidWeights_eq_one_of_nonempty _ ⟨i, hi⟩),
  Finset.centroidWeights, Function.const_apply]