case refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
s : Set E
⊢ ↑(convexHull R).toOrderHom s ⊆ ⋃ (t : Finset E) (_ : ↑t ⊆ s), ↑(convexHull R).toOrderHom ↑t

case refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
s : Set E
⊢ (⋃ (t : Finset E) (_ : ↑t ⊆ s), ↑(convexHull R).toOrderHom ↑t) ⊆ ↑(convexHull R).toOrderHom s
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
s : Set E
⊢ ↑(convexHull R).toOrderHom s = ⋃ (t : Finset E) (_ : ↑t ⊆ s), ↑(convexHull R).toOrderHom ↑t
refine' Subset.antisymm _ _
case refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
s : Set E
⊢ {x | ∃ ι t w z x_1 x_2 x_3, centerMass t w z = x} ⊆ ⋃ (t : Finset E) (_ : ↑t ⊆ s), ↑(convexHull R).toOrderHom ↑t
case refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
s : Set E
⊢ ↑(convexHull R).toOrderHom s ⊆ ⋃ (t : Finset E) (_ : ↑t ⊆ s), ↑(convexHull R).toOrderHom ↑t
rw [_root_.convexHull_eq]
case refine'_1.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι✝ : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι✝
c : R
t✝ : Finset ι✝
w✝ : ι✝ → R
z✝ : ι✝ → E
s : Set E
ι : Type u_1
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hz : ∀ (i : ι), i ∈ t → z i ∈ s
⊢ centerMass t w z ∈ ⋃ (t : Finset E) (_ : ↑t ⊆ s), ↑(convexHull R).toOrderHom ↑t
case refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
s : Set E
⊢ {x | ∃ ι t w z x_1 x_2 x_3, centerMass t w z = x} ⊆ ⋃ (t : Finset E) (_ : ↑t ⊆ s), ↑(convexHull R).toOrderHom ↑t
rintro x ⟨ι : Type u_1, t, w, z, hw₀, hw₁, hz, rfl⟩
case refine'_1.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι✝ : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι✝
c : R
t✝ : Finset ι✝
w✝ : ι✝ → R
z✝ : ι✝ → E
s : Set E
ι : Type u_1
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hz : ∀ (i : ι), i ∈ t → z i ∈ s
⊢ ∃ i i_1, centerMass t w z ∈ ↑(convexHull R).toOrderHom ↑i
case refine'_1.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι✝ : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι✝
c : R
t✝ : Finset ι✝
w✝ : ι✝ → R
z✝ : ι✝ → E
s : Set E
ι : Type u_1
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hz : ∀ (i : ι), i ∈ t → z i ∈ s
⊢ centerMass t w z ∈ ⋃ (t : Finset E) (_ : ↑t ⊆ s), ↑(convexHull R).toOrderHom ↑t
simp only [mem_iUnion]
case refine'_1.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι✝ : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι✝
c : R
t✝ : Finset ι✝
w✝ : ι✝ → R
z✝ : ι✝ → E
s : Set E
ι : Type u_1
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hz : ∀ (i : ι), i ∈ t → z i ∈ s
⊢ ↑(Finset.image z t) ⊆ s

case refine'_1.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι✝ : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι✝
c : R
t✝ : Finset ι✝
w✝ : ι✝ → R
z✝ : ι✝ → E
s : Set E
ι : Type u_1
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hz : ∀ (i : ι), i ∈ t → z i ∈ s
⊢ centerMass t w z ∈ ↑(convexHull R).toOrderHom ↑(Finset.image z t)
case refine'_1.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι✝ : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι✝
c : R
t✝ : Finset ι✝
w✝ : ι✝ → R
z✝ : ι✝ → E
s : Set E
ι : Type u_1
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hz : ∀ (i : ι), i ∈ t → z i ∈ s
⊢ ∃ i i_1, centerMass t w z ∈ ↑(convexHull R).toOrderHom ↑i
refine' ⟨t.image z, _, _⟩
case refine'_1.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι✝ : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι✝
c : R
t✝ : Finset ι✝
w✝ : ι✝ → R
z✝ : ι✝ → E
s : Set E
ι : Type u_1
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hz : ∀ (i : ι), i ∈ t → z i ∈ s
⊢ ↑t ⊆ z ⁻¹' s
case refine'_1.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι✝ : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι✝
c : R
t✝ : Finset ι✝
w✝ : ι✝ → R
z✝ : ι✝ → E
s : Set E
ι : Type u_1
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hz : ∀ (i : ι), i ∈ t → z i ∈ s
⊢ ↑(Finset.image z t) ⊆ s
rw [coe_image, Set.image_subset_iff]
no goals
case refine'_1.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι✝ : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι✝
c : R
t✝ : Finset ι✝
w✝ : ι✝ → R
z✝ : ι✝ → E
s : Set E
ι : Type u_1
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hz : ∀ (i : ι), i ∈ t → z i ∈ s
⊢ ↑t ⊆ z ⁻¹' s
exact hz
case refine'_1.intro.intro.intro.intro.intro.intro.intro.refine'_2.hws
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι✝ : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι✝
c : R
t✝ : Finset ι✝
w✝ : ι✝ → R
z✝ : ι✝ → E
s : Set E
ι : Type u_1
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hz : ∀ (i : ι), i ∈ t → z i ∈ s
⊢ 0 < ∑ i in t, w i

case refine'_1.intro.intro.intro.intro.intro.intro.intro.refine'_2.hz
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι✝ : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι✝
c : R
t✝ : Finset ι✝
w✝ : ι✝ → R
z✝ : ι✝ → E
s : Set E
ι : Type u_1
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hz : ∀ (i : ι), i ∈ t → z i ∈ s
⊢ ∀ (i : ι), i ∈ t → z i ∈ ↑(Finset.image z t)
case refine'_1.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι✝ : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι✝
c : R
t✝ : Finset ι✝
w✝ : ι✝ → R
z✝ : ι✝ → E
s : Set E
ι : Type u_1
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hz : ∀ (i : ι), i ∈ t → z i ∈ s
⊢ centerMass t w z ∈ ↑(convexHull R).toOrderHom ↑(Finset.image z t)
apply t.centerMass_mem_convexHull hw₀
no goals
case refine'_1.intro.intro.intro.intro.intro.intro.intro.refine'_2.hws
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι✝ : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι✝
c : R
t✝ : Finset ι✝
w✝ : ι✝ → R
z✝ : ι✝ → E
s : Set E
ι : Type u_1
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hz : ∀ (i : ι), i ∈ t → z i ∈ s
⊢ 0 < ∑ i in t, w i
simp only [hw₁, zero_lt_one]
no goals
case refine'_1.intro.intro.intro.intro.intro.intro.intro.refine'_2.hz
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι✝ : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι✝
c : R
t✝ : Finset ι✝
w✝ : ι✝ → R
z✝ : ι✝ → E
s : Set E
ι : Type u_1
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), i ∈ t → 0 ≤ w i
hw₁ : ∑ i in t, w i = 1
hz : ∀ (i : ι), i ∈ t → z i ∈ s
⊢ ∀ (i : ι), i ∈ t → z i ∈ ↑(Finset.image z t)
exact fun i hi => Finset.mem_coe.2 (Finset.mem_image_of_mem _ hi)
no goals
case refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.239379
ι : Type ?u.239382
ι' : Type ?u.239385
α : Type ?u.239388
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
s : Set E
⊢ (⋃ (t : Finset E) (_ : ↑t ⊆ s), ↑(convexHull R).toOrderHom ↑t) ⊆ ↑(convexHull R).toOrderHom s
exact iUnion_subset fun i => iUnion_subset convexHull_mono