[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
h : ¬AffineIndependent 𝕜 Subtype.val
x : E
m : x ∈ ↑(convexHull 𝕜) ↑t
⊢ ∃ y, x ∈ ↑(convexHull 𝕜) ↑(erase t ↑y)
[PROOFSTEP]
simp only [Finset.convexHull_eq, mem_setOf_eq] at m ⊢
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
h : ¬AffineIndependent 𝕜 Subtype.val
x : E
m : ∃ w x_1 x_2, centerMass t w id = x
⊢ ∃ y w x_1 x_2, centerMass (erase t ↑y) w id = x
[PROOFSTEP]
obtain ⟨f, fpos, fsum, rfl⟩ := m
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
h : ¬AffineIndependent 𝕜 Subtype.val
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
⊢ ∃ y w x x, centerMass (erase t ↑y) w id = centerMass t f id
[PROOFSTEP]
obtain ⟨g, gcombo, gsum, gpos⟩ := exists_nontrivial_relation_sum_zero_of_not_affine_ind h
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
h : ¬AffineIndependent 𝕜 Subtype.val
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ x, x ∈ t ∧ g x ≠ 0
⊢ ∃ y w x x, centerMass (erase t ↑y) w id = centerMass t f id
[PROOFSTEP]
replace gpos := exists_pos_of_sum_zero_of_exists_nonzero g gsum gpos
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
h : ¬AffineIndependent 𝕜 Subtype.val
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
⊢ ∃ y w x x, centerMass (erase t ↑y) w id = centerMass t f id
[PROOFSTEP]
clear h
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
⊢ ∃ y w x x, centerMass (erase t ↑y) w id = centerMass t f id
[PROOFSTEP]
let s := @Finset.filter _ (fun z => 0 < g z) (fun _ => LinearOrder.decidableLT _ _) t
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
⊢ ∃ y w x x, centerMass (erase t ↑y) w id = centerMass t f id
[PROOFSTEP]
obtain ⟨i₀, mem, w⟩ : ∃ i₀ ∈ s, ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i :=
  by
  apply s.exists_min_image fun z => f z / g z
  obtain ⟨x, hx, hgx⟩ : ∃ x ∈ t, 0 < g x := gpos
  exact ⟨x, mem_filter.mpr ⟨hx, hgx⟩⟩
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
⊢ ∃ i₀, i₀ ∈ s ∧ ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
[PROOFSTEP]
apply s.exists_min_image fun z => f z / g z
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
⊢ Finset.Nonempty s
[PROOFSTEP]
obtain ⟨x, hx, hgx⟩ : ∃ x ∈ t, 0 < g x := gpos
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
s : Finset E := filter (fun z => 0 < g z) t
x : E
hx : x ∈ t
hgx : 0 < g x
⊢ Finset.Nonempty s
[PROOFSTEP]
exact ⟨x, mem_filter.mpr ⟨hx, hgx⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
⊢ ∃ y w x x, centerMass (erase t ↑y) w id = centerMass t f id
[PROOFSTEP]
have hg : 0 < g i₀ := by
  rw [mem_filter] at mem 
  exact mem.2
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
⊢ 0 < g i₀
[PROOFSTEP]
rw [mem_filter] at mem 
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ t ∧ 0 < g i₀
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
⊢ 0 < g i₀
[PROOFSTEP]
exact mem.2
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
⊢ ∃ y w x x, centerMass (erase t ↑y) w id = centerMass t f id
[PROOFSTEP]
have hi₀ : i₀ ∈ t := filter_subset _ _ mem
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
⊢ ∃ y w x x, centerMass (erase t ↑y) w id = centerMass t f id
[PROOFSTEP]
let k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
⊢ ∃ y w x x, centerMass (erase t ↑y) w id = centerMass t f id
[PROOFSTEP]
have hk : k i₀ = 0 := by field_simp [ne_of_gt hg]
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
⊢ k i₀ = 0
[PROOFSTEP]
field_simp [ne_of_gt hg]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
⊢ ∃ y w x x, centerMass (erase t ↑y) w id = centerMass t f id
[PROOFSTEP]
have ksum : ∑ e in t.erase i₀, k e = 1 := by
  calc
    ∑ e in t.erase i₀, k e = ∑ e in t, k e := by
      conv_rhs => rw [← insert_erase hi₀, sum_insert (not_mem_erase i₀ t), hk, zero_add]
    _ = ∑ e in t, (f e - f i₀ / g i₀ * g e) := rfl
    _ = 1 := by rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
⊢ ∑ e in erase t i₀, k e = 1
[PROOFSTEP]
calc
  ∑ e in t.erase i₀, k e = ∑ e in t, k e := by
    conv_rhs => rw [← insert_erase hi₀, sum_insert (not_mem_erase i₀ t), hk, zero_add]
  _ = ∑ e in t, (f e - f i₀ / g i₀ * g e) := rfl
  _ = 1 := by rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
⊢ ∑ e in erase t i₀, k e = ∑ e in t, k e
[PROOFSTEP]
conv_rhs => rw [← insert_erase hi₀, sum_insert (not_mem_erase i₀ t), hk, zero_add]
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
| ∑ e in t, k e
[PROOFSTEP]
rw [← insert_erase hi₀, sum_insert (not_mem_erase i₀ t), hk, zero_add]
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
| ∑ e in t, k e
[PROOFSTEP]
rw [← insert_erase hi₀, sum_insert (not_mem_erase i₀ t), hk, zero_add]
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
| ∑ e in t, k e
[PROOFSTEP]
rw [← insert_erase hi₀, sum_insert (not_mem_erase i₀ t), hk, zero_add]
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
⊢ ∑ e in t, (f e - f i₀ / g i₀ * g e) = 1
[PROOFSTEP]
rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
⊢ ∃ y w x x, centerMass (erase t ↑y) w id = centerMass t f id
[PROOFSTEP]
refine' ⟨⟨i₀, hi₀⟩, k, _, by convert ksum, _⟩
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
⊢ ∑ y in erase t ↑{ val := i₀, property := hi₀ }, k y = 1
[PROOFSTEP]
convert ksum
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
⊢ ∀ (y : E), y ∈ erase t ↑{ val := i₀, property := hi₀ } → 0 ≤ k y
[PROOFSTEP]
simp only [and_imp, sub_nonneg, mem_erase, Ne.def, Subtype.coe_mk]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
⊢ ∀ (y : E), ¬y = i₀ → y ∈ t → f i₀ / g i₀ * g y ≤ f y
[PROOFSTEP]
intro e _ het
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
⊢ f i₀ / g i₀ * g e ≤ f e
[PROOFSTEP]
by_cases hes : e ∈ s
[GOAL]
case pos
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∈ s
⊢ f i₀ / g i₀ * g e ≤ f e
[PROOFSTEP]
have hge : 0 < g e := by
  rw [mem_filter] at hes 
  exact hes.2
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∈ s
⊢ 0 < g e
[PROOFSTEP]
rw [mem_filter] at hes 
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∈ t ∧ 0 < g e
⊢ 0 < g e
[PROOFSTEP]
exact hes.2
[GOAL]
case pos
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∈ s
hge : 0 < g e
⊢ f i₀ / g i₀ * g e ≤ f e
[PROOFSTEP]
rw [← le_div_iff hge]
[GOAL]
case pos
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : e ∈ s
hge : 0 < g e
⊢ f i₀ / g i₀ ≤ f e / g e
[PROOFSTEP]
exact w _ hes
[GOAL]
case neg
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : ¬e ∈ s
⊢ f i₀ / g i₀ * g e ≤ f e
[PROOFSTEP]
calc
  _ ≤ 0 := by
    apply mul_nonpos_of_nonneg_of_nonpos
    · apply div_nonneg (fpos i₀ (mem_of_subset (filter_subset _ t) mem)) (le_of_lt hg)
    · simpa only [mem_filter, het, true_and_iff, not_lt] using hes
  _ ≤ f e := fpos e het
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : ¬e ∈ s
⊢ f i₀ / g i₀ * g e ≤ 0
[PROOFSTEP]
apply mul_nonpos_of_nonneg_of_nonpos
[GOAL]
case ha
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : ¬e ∈ s
⊢ 0 ≤ f i₀ / g i₀
[PROOFSTEP]
apply div_nonneg (fpos i₀ (mem_of_subset (filter_subset _ t) mem)) (le_of_lt hg)
[GOAL]
case hb
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
e : E
a✝ : ¬e = i₀
het : e ∈ t
hes : ¬e ∈ s
⊢ g e ≤ 0
[PROOFSTEP]
simpa only [mem_filter, het, true_and_iff, not_lt] using hes
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
⊢ centerMass (erase t ↑{ val := i₀, property := hi₀ }) k id = centerMass t f id
[PROOFSTEP]
rw [Subtype.coe_mk, centerMass_eq_of_sum_1 _ id ksum]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
⊢ ∑ i in erase t i₀, k i • id i = centerMass t f id
[PROOFSTEP]
calc
  ∑ e in t.erase i₀, k e • e = ∑ e in t, k e • e := sum_erase _ (by rw [hk, zero_smul])
  _ = ∑ e in t, (f e - f i₀ / g i₀ * g e) • e := rfl
  _ = t.centerMass f id := by
    simp only [sub_smul, mul_smul, sum_sub_distrib, ← smul_sum, gcombo, smul_zero, sub_zero, centerMass, fsum, inv_one,
      one_smul, id.def]
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
⊢ k i₀ • i₀ = 0
[PROOFSTEP]
rw [hk, zero_smul]
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ (y : E), y ∈ t → 0 ≤ f y
fsum : ∑ y in t, f y = 1
g : E → 𝕜
gcombo : ∑ e in t, g e • e = 0
gsum : ∑ e in t, g e = 0
gpos : ∃ i, i ∈ t ∧ 0 < g i
s : Finset E := filter (fun z => 0 < g z) t
i₀ : E
mem : i₀ ∈ s
w : ∀ (i : E), i ∈ s → f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun z => f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : ∑ e in erase t i₀, k e = 1
⊢ ∑ e in t, (f e - f i₀ / g i₀ * g e) • e = centerMass t f id
[PROOFSTEP]
simp only [sub_smul, mul_smul, sum_sub_distrib, ← smul_sum, gcombo, smul_zero, sub_zero, centerMass, fsum, inv_one,
  one_smul, id.def]
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
⊢ Set.Nonempty {t | ↑t ⊆ s ∧ x ∈ ↑(convexHull 𝕜) ↑t}
[PROOFSTEP]
simpa only [convexHull_eq_union_convexHull_finite_subsets s, exists_prop, mem_iUnion] using hx
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
⊢ Finset.Nonempty (minCardFinsetOfMemConvexHull hx)
[PROOFSTEP]
rw [← Finset.coe_nonempty, ← @convexHull_nonempty_iff 𝕜]
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
⊢ Set.Nonempty (↑(convexHull 𝕜) ↑(minCardFinsetOfMemConvexHull hx))
[PROOFSTEP]
exact ⟨x, mem_minCardFinsetOfMemConvexHull hx⟩
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : x ∈ ↑(convexHull 𝕜) ↑t
⊢ t ∈ {t | ↑t ⊆ s ∧ x ∈ ↑(convexHull 𝕜) ↑t}
[PROOFSTEP]
exact ⟨ht₁, ht₂⟩
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
⊢ AffineIndependent 𝕜 Subtype.val
[PROOFSTEP]
let k := (minCardFinsetOfMemConvexHull hx).card - 1
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
⊢ AffineIndependent 𝕜 Subtype.val
[PROOFSTEP]
have hk : (minCardFinsetOfMemConvexHull hx).card = k + 1 :=
  (Nat.succ_pred_eq_of_pos (Finset.card_pos.mpr (minCardFinsetOfMemConvexHull_nonempty hx))).symm
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
⊢ AffineIndependent 𝕜 Subtype.val
[PROOFSTEP]
classical
by_contra h
obtain ⟨p, hp⟩ := mem_convexHull_erase h (mem_minCardFinsetOfMemConvexHull hx)
have contra :=
  minCardFinsetOfMemConvexHull_card_le_card hx
    (Set.Subset.trans (Finset.erase_subset (p : E) (minCardFinsetOfMemConvexHull hx))
      (minCardFinsetOfMemConvexHull_subseteq hx))
    hp
rw [← not_lt] at contra 
apply contra
erw [card_erase_of_mem p.2, hk]
exact lt_add_one _
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
⊢ AffineIndependent 𝕜 Subtype.val
[PROOFSTEP]
by_contra h
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
⊢ False
[PROOFSTEP]
obtain ⟨p, hp⟩ := mem_convexHull_erase h (mem_minCardFinsetOfMemConvexHull hx)
[GOAL]
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜) ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
⊢ False
[PROOFSTEP]
have contra :=
  minCardFinsetOfMemConvexHull_card_le_card hx
    (Set.Subset.trans (Finset.erase_subset (p : E) (minCardFinsetOfMemConvexHull hx))
      (minCardFinsetOfMemConvexHull_subseteq hx))
    hp
[GOAL]
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜) ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
contra : card (minCardFinsetOfMemConvexHull hx) ≤ card (erase (minCardFinsetOfMemConvexHull hx) ↑p)
⊢ False
[PROOFSTEP]
rw [← not_lt] at contra 
[GOAL]
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜) ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
contra : ¬card (erase (minCardFinsetOfMemConvexHull hx) ↑p) < card (minCardFinsetOfMemConvexHull hx)
⊢ False
[PROOFSTEP]
apply contra
[GOAL]
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜) ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
contra : ¬card (erase (minCardFinsetOfMemConvexHull hx) ↑p) < card (minCardFinsetOfMemConvexHull hx)
⊢ card (erase (minCardFinsetOfMemConvexHull hx) ↑p) < card (minCardFinsetOfMemConvexHull hx)
[PROOFSTEP]
erw [card_erase_of_mem p.2, hk]
[GOAL]
case intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
k : ℕ := card (minCardFinsetOfMemConvexHull hx) - 1
hk : card (minCardFinsetOfMemConvexHull hx) = k + 1
h : ¬AffineIndependent 𝕜 Subtype.val
p : ↑↑(minCardFinsetOfMemConvexHull hx)
hp : x ∈ ↑(convexHull 𝕜) ↑(erase (minCardFinsetOfMemConvexHull hx) ↑p)
contra : ¬card (erase (minCardFinsetOfMemConvexHull hx) ↑p) < card (minCardFinsetOfMemConvexHull hx)
⊢ k + 1 - 1 < k + 1
[PROOFSTEP]
exact lt_add_one _
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ↑(convexHull 𝕜) s = ⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜) ↑t
[PROOFSTEP]
apply Set.Subset.antisymm
[GOAL]
case h₁
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ↑(convexHull 𝕜) s ⊆ ⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜) ↑t
[PROOFSTEP]
intro x hx
[GOAL]
case h₁
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
⊢ x ∈ ⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜) ↑t
[PROOFSTEP]
simp only [exists_prop, Set.mem_iUnion]
[GOAL]
case h₁
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
⊢ ∃ i, ↑i ⊆ s ∧ AffineIndependent 𝕜 Subtype.val ∧ x ∈ ↑(convexHull 𝕜) ↑i
[PROOFSTEP]
exact
  ⟨Caratheodory.minCardFinsetOfMemConvexHull hx, Caratheodory.minCardFinsetOfMemConvexHull_subseteq hx,
    Caratheodory.affineIndependent_minCardFinsetOfMemConvexHull hx, Caratheodory.mem_minCardFinsetOfMemConvexHull hx⟩
[GOAL]
case h₂
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜) ↑t ⊆ ↑(convexHull 𝕜) s
[PROOFSTEP]
iterate 3 convert Set.iUnion_subset _; intro
[GOAL]
case h₂
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜) ↑t ⊆ ↑(convexHull 𝕜) s
[PROOFSTEP]
convert Set.iUnion_subset _
[GOAL]
case h₂.convert_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ∀ (i : Finset E), ⋃ (_ : ↑i ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜) ↑i ⊆ ↑(convexHull 𝕜) s
[PROOFSTEP]
intro
[GOAL]
case h₂.convert_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝ : Finset E
⊢ ⋃ (_ : ↑i✝ ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜) ↑i✝ ⊆ ↑(convexHull 𝕜) s
[PROOFSTEP]
convert Set.iUnion_subset _
[GOAL]
case h₂.convert_5.convert_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝ : Finset E
⊢ ↑i✝ ⊆ s → ⋃ (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜) ↑i✝ ⊆ ↑(convexHull 𝕜) s
[PROOFSTEP]
intro
[GOAL]
case h₂.convert_5.convert_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝¹ : Finset E
i✝ : ↑i✝¹ ⊆ s
⊢ ⋃ (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜) ↑i✝¹ ⊆ ↑(convexHull 𝕜) s
[PROOFSTEP]
convert Set.iUnion_subset _
[GOAL]
case h₂.convert_5.convert_5.convert_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝¹ : Finset E
i✝ : ↑i✝¹ ⊆ s
⊢ AffineIndependent 𝕜 Subtype.val → ↑(convexHull 𝕜) ↑i✝¹ ⊆ ↑(convexHull 𝕜) s
[PROOFSTEP]
intro
[GOAL]
case h₂.convert_5.convert_5.convert_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝² : Finset E
i✝¹ : ↑i✝² ⊆ s
i✝ : AffineIndependent 𝕜 Subtype.val
⊢ ↑(convexHull 𝕜) ↑i✝² ⊆ ↑(convexHull 𝕜) s
[PROOFSTEP]
exact convexHull_mono ‹_›
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜) s
⊢ ∃ ι x_1 z w x_2 x_3 x_4, ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x
[PROOFSTEP]
rw [convexHull_eq_union] at hx 
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜) ↑t
⊢ ∃ ι x_1 z w x_2 x_3 x_4, ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x
[PROOFSTEP]
simp only [exists_prop, Set.mem_iUnion] at hx 
[GOAL]
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : ∃ i, ↑i ⊆ s ∧ AffineIndependent 𝕜 Subtype.val ∧ x ∈ ↑(convexHull 𝕜) ↑i
⊢ ∃ ι x_1 z w x_2 x_3 x_4, ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x
[PROOFSTEP]
obtain ⟨t, ht₁, ht₂, ht₃⟩ := hx
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
ht₃ : x ∈ ↑(convexHull 𝕜) ↑t
⊢ ∃ ι x_1 z w x_2 x_3 x_4, ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x
[PROOFSTEP]
simp only [t.convexHull_eq, exists_prop, Set.mem_setOf_eq] at ht₃ 
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
ht₃ : ∃ w, (∀ (y : E), y ∈ t → 0 ≤ w y) ∧ ∑ y in t, w y = 1 ∧ centerMass t w id = x
⊢ ∃ ι x_1 z w x_2 x_3 x_4, ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x
[PROOFSTEP]
obtain ⟨w, hw₁, hw₂, hw₃⟩ := ht₃
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ (y : E), y ∈ t → 0 ≤ w y
hw₂ : ∑ y in t, w y = 1
hw₃ : centerMass t w id = x
⊢ ∃ ι x_1 z w x_2 x_3 x_4, ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x
[PROOFSTEP]
let t' := t.filter fun i => w i ≠ 0
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ (y : E), y ∈ t → 0 ≤ w y
hw₂ : ∑ y in t, w y = 1
hw₃ : centerMass t w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∃ ι x_1 z w x_2 x_3 x_4, ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x
[PROOFSTEP]
refine' ⟨t', t'.fintypeCoeSort, ((↑) : t' → E), w ∘ ((↑) : t' → E), _, _, _, _, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ (y : E), y ∈ t → 0 ≤ w y
hw₂ : ∑ y in t, w y = 1
hw₃ : centerMass t w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ Set.range Subtype.val ⊆ s
[PROOFSTEP]
rw [Subtype.range_coe_subtype]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ (y : E), y ∈ t → 0 ≤ w y
hw₂ : ∑ y in t, w y = 1
hw₃ : centerMass t w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ {x | x ∈ t'} ⊆ s
[PROOFSTEP]
exact Subset.trans (Finset.filter_subset _ t) ht₁
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ (y : E), y ∈ t → 0 ≤ w y
hw₂ : ∑ y in t, w y = 1
hw₃ : centerMass t w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ AffineIndependent 𝕜 Subtype.val
[PROOFSTEP]
exact ht₂.comp_embedding ⟨_, inclusion_injective (Finset.filter_subset (fun i => w i ≠ 0) t)⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ (y : E), y ∈ t → 0 ≤ w y
hw₂ : ∑ y in t, w y = 1
hw₃ : centerMass t w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∀ (i : { x // x ∈ t' }), 0 < (w ∘ Subtype.val) i
[PROOFSTEP]
exact fun i => (hw₁ _ (Finset.mem_filter.mp i.2).1).lt_of_ne (Finset.mem_filter.mp i.property).2.symm
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_4
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ (y : E), y ∈ t → 0 ≤ w y
hw₂ : ∑ y in t, w y = 1
hw₃ : centerMass t w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∑ i : { x // x ∈ t' }, (w ∘ Subtype.val) i = 1
[PROOFSTEP]
erw [Finset.sum_attach, Finset.sum_filter_ne_zero, hw₂]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ (y : E), y ∈ t → 0 ≤ w y
hw₂ : ∑ y in t, w y = 1
hw₃ : centerMass t w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∑ i : { x // x ∈ t' }, (w ∘ Subtype.val) i • ↑i = x
[PROOFSTEP]
change (∑ i : t' in t'.attach, (fun e => w e • e) ↑i) = x
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ (y : E), y ∈ t → 0 ≤ w y
hw₂ : ∑ y in t, w y = 1
hw₃ : centerMass t w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∑ i in attach t', (fun e => w e • e) ↑i = x
[PROOFSTEP]
erw [Finset.sum_attach (f := fun e => w e • e), Finset.sum_filter_of_ne]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ (y : E), y ∈ t → 0 ≤ w y
hw₂ : ∑ y in t, w y = 1
hw₃ : centerMass t w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∑ x in t, w x • x = x
[PROOFSTEP]
rw [t.centerMass_eq_of_sum_1 id hw₂] at hw₃ 
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ (y : E), y ∈ t → 0 ≤ w y
hw₂ : ∑ y in t, w y = 1
hw₃ : ∑ i in t, w i • id i = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∑ x in t, w x • x = x
[PROOFSTEP]
exact hw₃
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ (y : E), y ∈ t → 0 ≤ w y
hw₂ : ∑ y in t, w y = 1
hw₃ : centerMass t w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∀ (x : E), x ∈ t → w x • x ≠ 0 → w x ≠ 0
[PROOFSTEP]
intro e _ hwe contra
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ (y : E), y ∈ t → 0 ≤ w y
hw₂ : ∑ y in t, w y = 1
hw₃ : centerMass t w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
e : E
a✝ : e ∈ t
hwe : w e • e ≠ 0
contra : w e = 0
⊢ False
[PROOFSTEP]
apply hwe
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ (y : E), y ∈ t → 0 ≤ w y
hw₂ : ∑ y in t, w y = 1
hw₃ : centerMass t w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
e : E
a✝ : e ∈ t
hwe : w e • e ≠ 0
contra : w e = 0
⊢ w e • e = 0
[PROOFSTEP]
rw [contra, zero_smul]
