[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]


[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
⊢ Set.Nonempty (extremePoints ℝ s)
[PROOFSTEP]
let S : Set (Set E) := {t | t.Nonempty ∧ IsClosed t ∧ IsExtreme ℝ s t}
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
⊢ Set.Nonempty (extremePoints ℝ s)
[PROOFSTEP]
rsuffices ⟨t, ⟨⟨x, hxt⟩, htclos, hst⟩, hBmin⟩ : ∃ t ∈ S, ∀ u ∈ S, u ⊆ t → u = t
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
⊢ Set.Nonempty (extremePoints ℝ s)
[PROOFSTEP]
refine' ⟨x, mem_extremePoints_iff_extreme_singleton.2 _⟩
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
⊢ IsExtreme ℝ s {x}
[PROOFSTEP]
rwa [← eq_singleton_iff_unique_mem.2 ⟨hxt, fun y hyB => ?_⟩]
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
⊢ y = x
[PROOFSTEP]
by_contra hyx
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
⊢ False
[PROOFSTEP]
obtain ⟨l, hl⟩ := geometric_hahn_banach_point_point hyx
[GOAL]
case intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
l : E →L[ℝ] ℝ
hl : ↑l y < ↑l x
⊢ False
[PROOFSTEP]
obtain ⟨z, hzt, hz⟩ :=
  (isCompact_of_isClosed_subset hscomp htclos hst.1).exists_forall_ge ⟨x, hxt⟩ l.continuous.continuousOn
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
l : E →L[ℝ] ℝ
hl : ↑l y < ↑l x
z : E
hzt : z ∈ t
hz : ∀ (y : E), y ∈ t → ↑l y ≤ ↑l z
⊢ False
[PROOFSTEP]
have h : IsExposed ℝ t ({z ∈ t | ∀ w ∈ t, l w ≤ l z}) := fun _ => ⟨l, rfl⟩
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyB : y ∈ t
hyx : ¬y = x
l : E →L[ℝ] ℝ
hl : ↑l y < ↑l x
z : E
hzt : z ∈ t
hz : ∀ (y : E), y ∈ t → ↑l y ≤ ↑l z
h : IsExposed ℝ t {z | z ∈ t ∧ ∀ (w : E), w ∈ t → ↑l w ≤ ↑l z}
⊢ False
[PROOFSTEP]
rw [← hBmin ({z ∈ t | ∀ w ∈ t, l w ≤ l z}) ⟨⟨z, hzt, hz⟩, h.isClosed htclos, hst.trans h.isExtreme⟩ (t.sep_subset _)] at
  hyB
[GOAL]
case intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
t : Set E
hBmin : ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
x : E
hxt : x ∈ t
htclos : IsClosed t
hst : IsExtreme ℝ s t
y : E
hyx : ¬y = x
l : E →L[ℝ] ℝ
hyB : y ∈ {z | z ∈ t ∧ ∀ (w : E), w ∈ t → ↑l w ≤ ↑l z}
hl : ↑l y < ↑l x
z : E
hzt : z ∈ t
hz : ∀ (y : E), y ∈ t → ↑l y ≤ ↑l z
h : IsExposed ℝ t {z | z ∈ t ∧ ∀ (w : E), w ∈ t → ↑l w ≤ ↑l z}
⊢ False
[PROOFSTEP]
exact hl.not_le (hyB.2 x hxt)
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
⊢ ∃ t, t ∈ S ∧ ∀ (u : Set E), u ∈ S → u ⊆ t → u = t
[PROOFSTEP]
refine' zorn_superset _ fun F hFS hF => _
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
⊢ ∃ lb, lb ∈ S ∧ ∀ (s : Set E), s ∈ F → lb ⊆ s
[PROOFSTEP]
obtain rfl | hFnemp := F.eq_empty_or_nonempty
[GOAL]
case inl
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
hFS : ∅ ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) ∅
⊢ ∃ lb, lb ∈ S ∧ ∀ (s : Set E), s ∈ ∅ → lb ⊆ s
[PROOFSTEP]
exact ⟨s, ⟨hsnemp, hscomp.isClosed, IsExtreme.rfl⟩, fun _ => False.elim⟩
[GOAL]
case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
hFnemp : Set.Nonempty F
⊢ ∃ lb, lb ∈ S ∧ ∀ (s : Set E), s ∈ F → lb ⊆ s
[PROOFSTEP]
refine'
  ⟨⋂₀ F, ⟨_, isClosed_sInter fun t ht => (hFS ht).2.1, isExtreme_sInter hFnemp fun t ht => (hFS ht).2.2⟩, fun t ht =>
    sInter_subset_of_mem ht⟩
[GOAL]
case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
hFnemp : Set.Nonempty F
⊢ Set.Nonempty (⋂₀ F)
[PROOFSTEP]
haveI : Nonempty (↥F) := hFnemp.to_subtype
[GOAL]
case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
hFnemp : Set.Nonempty F
this : Nonempty ↑F
⊢ Set.Nonempty (⋂₀ F)
[PROOFSTEP]
rw [sInter_eq_iInter]
[GOAL]
case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
hFnemp : Set.Nonempty F
this : Nonempty ↑F
⊢ Set.Nonempty (⋂ (i : ↑F), ↑i)
[PROOFSTEP]
refine'
  IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed _ (fun t u => _) (fun t => (hFS t.mem).1)
    (fun t => isCompact_of_isClosed_subset hscomp (hFS t.mem).2.1 (hFS t.mem).2.2.1) fun t => (hFS t.mem).2.1
[GOAL]
case inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
hFnemp : Set.Nonempty F
this : Nonempty ↑F
t u : ↑F
⊢ ∃ z, (fun x x_1 => x ⊇ x_1) ↑t ↑z ∧ (fun x x_1 => x ⊇ x_1) ↑u ↑z
[PROOFSTEP]
obtain htu | hut := hF.total t.mem u.mem
[GOAL]
case inr.inl
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
hFnemp : Set.Nonempty F
this : Nonempty ↑F
t u : ↑F
htu : ↑t ⊆ ↑u
⊢ ∃ z, (fun x x_1 => x ⊇ x_1) ↑t ↑z ∧ (fun x x_1 => x ⊇ x_1) ↑u ↑z
case inr.inr
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hsnemp : Set.Nonempty s
S : Set (Set E) := {t | Set.Nonempty t ∧ IsClosed t ∧ IsExtreme ℝ s t}
F : Set (Set E)
hFS : F ⊆ S
hF : IsChain (fun x x_1 => x ⊆ x_1) F
hFnemp : Set.Nonempty F
this : Nonempty ↑F
t u : ↑F
hut : ↑u ⊆ ↑t
⊢ ∃ z, (fun x x_1 => x ⊇ x_1) ↑t ↑z ∧ (fun x x_1 => x ⊇ x_1) ↑u ↑z
[PROOFSTEP]
exacts [⟨t, Subset.rfl, htu⟩, ⟨u, hut, Subset.rfl⟩]
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
⊢ closure (↑(convexHull ℝ) (extremePoints ℝ s)) = s
[PROOFSTEP]
apply (closure_minimal (convexHull_min extremePoints_subset hAconv) hscomp.isClosed).antisymm
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
⊢ s ⊆ closure (↑(convexHull ℝ) (extremePoints ℝ s))
[PROOFSTEP]
by_contra hs
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ) (extremePoints ℝ s))
⊢ False
[PROOFSTEP]
obtain ⟨x, hxA, hxt⟩ := not_subset.1 hs
[GOAL]
case intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s))
⊢ False
[PROOFSTEP]
obtain ⟨l, r, hlr, hrx⟩ := geometric_hahn_banach_closed_point (convex_convexHull _ _).closure isClosed_closure hxt
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
⊢ False
[PROOFSTEP]
have h : IsExposed ℝ s ({y ∈ s | ∀ z ∈ s, l z ≤ l y}) := fun _ => ⟨l, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
⊢ False
[PROOFSTEP]
obtain ⟨z, hzA, hz⟩ := hscomp.exists_forall_ge ⟨x, hxA⟩ l.continuous.continuousOn
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
z : E
hzA : z ∈ s
hz : ∀ (y : E), y ∈ s → ↑l y ≤ ↑l z
⊢ False
[PROOFSTEP]
obtain ⟨y, hy⟩ := (h.isCompact hscomp).has_extreme_point ⟨z, hzA, hz⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : TopologicalSpace E
inst✝³ : T2Space E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hscomp : IsCompact s
hAconv : Convex ℝ s
hs : ¬s ⊆ closure (↑(convexHull ℝ) (extremePoints ℝ s))
x : E
hxA : x ∈ s
hxt : ¬x ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s))
l : E →L[ℝ] ℝ
r : ℝ
hlr : ∀ (a : E), a ∈ closure (↑(convexHull ℝ) (extremePoints ℝ s)) → ↑l a < r
hrx : r < ↑l x
h : IsExposed ℝ s {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
z : E
hzA : z ∈ s
hz : ∀ (y : E), y ∈ s → ↑l y ≤ ↑l z
y : E
hy : y ∈ extremePoints ℝ {y | y ∈ s ∧ ∀ (z : E), z ∈ s → ↑l z ≤ ↑l y}
⊢ False
[PROOFSTEP]
linarith [hlr _ (subset_closure <| subset_convexHull _ _ <| h.isExtreme.extremePoints_subset_extremePoints hy),
  hy.1.2 x hxA]