rw [add_sub_assoc, sub_smul, sub_right_comm, one_smul, sub_self, zero_sub, ← smul_neg, ←
  smul_add, norm_smul_of_nonneg, ← sub_eq_add_neg]
case h.e'_3.h
𝕜 : 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)⁻¹ • Finset.centroid ℝ s id + (1 - (↑n + 2)⁻¹) • x - x‖ = (↑n + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖
case h.e'_3.h.ht
𝕜 : 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 : ℕ
⊢ 0 ≤ (↑n + 2)⁻¹