simp only [not_exists, and_imp, not_and, mem_setOf_eq, mem_diff, exists_imp]
𝕜 : 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
x : E
⊢ x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} →
    x ∈
      {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} \
        {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x}
𝕜 : 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
x : E
⊢ ∀ (x_1 : E → 𝕜),
    (∀ y ∈ s, 0 < x_1 y) →
      ∑ y ∈ s, x_1 y = 1 →
        s.centerMass x_1 id = x →
          (∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x) ∧
            ∀ (x_4 : E → 𝕜),
              (∀ y ∈ s, 0 ≤ x_4 y) → ∑ y ∈ s, x_4 y = 1 → ∀ x_7 ∈ s, x_4 x_7 = 0 → ¬s.centerMass x_4 id = x