rw [Finset.centroid_def]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
⊢ Finset.centroid 𝕜 s id ∈ combiInterior 𝕜 s
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
⊢ (Finset.affineCombination 𝕜 s id) (Finset.centroidWeights 𝕜 s) ∈ combiInterior 𝕜 s