simp only [mul_boole, Finset.centroidWeights_apply]
case a.refine'_2.refine'_1
𝕜 : 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 : ℕ
⊢ ∀ y ∈ s, 0 < (↑n + 2)⁻¹ * Finset.centroidWeights ℝ s y + (1 - (↑n + 2)⁻¹) * if x = y then 1 else 0
case a.refine'_2.refine'_1
𝕜 : 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 : ℕ
⊢ ∀ y ∈ s, 0 < (↑n + 2)⁻¹ * (↑s.card)⁻¹ + if x = y then 1 - (↑n + 2)⁻¹ else 0