rw [Finset.centerMass_segment]
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (↑n + 2)⁻¹ • s.centerMass (Finset.centroidWeights ℝ s) id +
      (1 - (↑n + 2)⁻¹) • s.centerMass (fun j => if x = j then 1 else 0) id ∈
    combiInterior ℝ s
case a.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ s.centerMass (fun i => (↑n + 2)⁻¹ * Finset.centroidWeights ℝ s i + (1 - (↑n + 2)⁻¹) * if x = i then 1 else 0) id ∈
    combiInterior ℝ s

case a.refine'_2.hw₁
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1

case a.refine'_2.hw₂
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (∑ i ∈ s, if x = i then 1 else 0) = 1

case a.refine'_2.hab
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ (↑n + 2)⁻¹ + (1 - (↑n + 2)⁻¹) = 1