rw [combiInterior_eq hs]
𝕜 : 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
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
⊢ s.centerMass (fun i => Finset.centroidWeights 𝕜 s i) 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
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
⊢ s.centerMass (fun i => Finset.centroidWeights 𝕜 s i) id ∈
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}