intro w hw₀ hw₁ hw₂
𝕜 : 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
𝕜 : 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
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
hw₂ : s.centerMass w id = x
⊢ (∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x) ∧
    ∀ (x_1 : E → 𝕜), (∀ y ∈ s, 0 ≤ x_1 y) → ∑ y ∈ s, x_1 y = 1 → ∀ x_4 ∈ s, x_1 x_4 = 0 → ¬s.centerMass x_1 id = x