case refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
⊢ ↑s ⊆ {x | ∃ w x_1 x_2, centerMass s w id = x}

case refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
⊢ Convex R {x | ∃ w x_1 x_2, centerMass s w id = x}

case refine'_3
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
⊢ {x | ∃ w x_1 x_2, centerMass s w id = x} ⊆ ↑(convexHull R).toOrderHom ↑s
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
⊢ ↑(convexHull R).toOrderHom ↑s = {x | ∃ w x_1 x_2, centerMass s w id = x}
refine' Set.Subset.antisymm (convexHull_min _ _) _
case refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
x : E
hx : x ∈ ↑s
⊢ x ∈ {x | ∃ w x_1 x_2, centerMass s w id = x}
case refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
⊢ ↑s ⊆ {x | ∃ w x_1 x_2, centerMass s w id = x}
intro x hx
case refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
x : E
hx : x ∈ s
⊢ x ∈ {x | ∃ w x_1 x_2, centerMass s w id = x}
case refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
x : E
hx : x ∈ ↑s
⊢ x ∈ {x | ∃ w x_1 x_2, centerMass s w id = x}
rw [Finset.mem_coe] at hx
case refine'_1.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
x : E
hx : x ∈ s
⊢ ∀ (y : E), y ∈ s → 0 ≤ if x = y then 1 else 0

case refine'_1.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
x : E
hx : x ∈ s
⊢ (∑ y in s, if x = y then 1 else 0) = 1
case refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
x : E
hx : x ∈ s
⊢ x ∈ {x | ∃ w x_1 x_2, centerMass s w id = x}
refine' ⟨_, _, _, Finset.centerMass_ite_eq _ _ _ hx⟩
case refine'_1.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
x : E
hx : x ∈ s
y✝ : E
a✝ : y✝ ∈ s
⊢ 0 ≤ if x = y✝ then 1 else 0
case refine'_1.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
x : E
hx : x ∈ s
⊢ ∀ (y : E), y ∈ s → 0 ≤ if x = y then 1 else 0
intros
case refine'_1.refine'_1.inl
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
x : E
hx : x ∈ s
y✝ : E
a✝ : y✝ ∈ s
h✝ : x = y✝
⊢ 0 ≤ 1

case refine'_1.refine'_1.inr
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
x : E
hx : x ∈ s
y✝ : E
a✝ : y✝ ∈ s
h✝ : ¬x = y✝
⊢ 0 ≤ 0
case refine'_1.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
x : E
hx : x ∈ s
y✝ : E
a✝ : y✝ ∈ s
⊢ 0 ≤ if x = y✝ then 1 else 0
split_ifs
no goals
case refine'_1.refine'_1.inl
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
x : E
hx : x ∈ s
y✝ : E
a✝ : y✝ ∈ s
h✝ : x = y✝
⊢ 0 ≤ 1

case refine'_1.refine'_1.inr
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
x : E
hx : x ∈ s
y✝ : E
a✝ : y✝ ∈ s
h✝ : ¬x = y✝
⊢ 0 ≤ 0
exacts [zero_le_one, le_refl 0]
no goals
case refine'_1.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
x : E
hx : x ∈ s
⊢ (∑ y in s, if x = y then 1 else 0) = 1
rw [Finset.sum_ite_eq, if_pos hx]
case refine'_2.intro.intro.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
wx : E → R
hwx₀ : ∀ (y : E), y ∈ s → 0 ≤ wx y
hwx₁ : ∑ y in s, wx y = 1
wy : E → R
hwy₀ : ∀ (y : E), y ∈ s → 0 ≤ wy y
hwy₁ : ∑ y in s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • centerMass s wx id + b • centerMass s wy id ∈ {x | ∃ w x_1 x_2, centerMass s w id = x}
case refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
⊢ Convex R {x | ∃ w x_1 x_2, centerMass s w id = x}
rintro x ⟨wx, hwx₀, hwx₁, rfl⟩ y ⟨wy, hwy₀, hwy₁, rfl⟩ a b ha hb hab
case refine'_2.intro.intro.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
wx : E → R
hwx₀ : ∀ (y : E), y ∈ s → 0 ≤ wx y
hwx₁ : ∑ y in s, wx y = 1
wy : E → R
hwy₀ : ∀ (y : E), y ∈ s → 0 ≤ wy y
hwy₁ : ∑ y in s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ centerMass s (fun i => a * wx i + b * wy i) id ∈ {x | ∃ w x_1 x_2, centerMass s w id = x}
case refine'_2.intro.intro.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
wx : E → R
hwx₀ : ∀ (y : E), y ∈ s → 0 ≤ wx y
hwx₁ : ∑ y in s, wx y = 1
wy : E → R
hwy₀ : ∀ (y : E), y ∈ s → 0 ≤ wy y
hwy₁ : ∑ y in s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • centerMass s wx id + b • centerMass s wy id ∈ {x | ∃ w x_1 x_2, centerMass s w id = x}
rw [Finset.centerMass_segment _ _ _ _ hwx₁ hwy₁ _ _ hab]
case refine'_2.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
wx : E → R
hwx₀ : ∀ (y : E), y ∈ s → 0 ≤ wx y
hwx₁ : ∑ y in s, wx y = 1
wy : E → R
hwy₀ : ∀ (y : E), y ∈ s → 0 ≤ wy y
hwy₁ : ∑ y in s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∀ (y : E), y ∈ s → 0 ≤ a * wx y + b * wy y

case refine'_2.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
wx : E → R
hwx₀ : ∀ (y : E), y ∈ s → 0 ≤ wx y
hwx₁ : ∑ y in s, wx y = 1
wy : E → R
hwy₀ : ∀ (y : E), y ∈ s → 0 ≤ wy y
hwy₁ : ∑ y in s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ y in s, (a * wx y + b * wy y) = 1
case refine'_2.intro.intro.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
wx : E → R
hwx₀ : ∀ (y : E), y ∈ s → 0 ≤ wx y
hwx₁ : ∑ y in s, wx y = 1
wy : E → R
hwy₀ : ∀ (y : E), y ∈ s → 0 ≤ wy y
hwy₁ : ∑ y in s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ centerMass s (fun i => a * wx i + b * wy i) id ∈ {x | ∃ w x_1 x_2, centerMass s w id = x}
refine' ⟨_, _, _, rfl⟩
case refine'_2.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
wx : E → R
hwx₀ : ∀ (y : E), y ∈ s → 0 ≤ wx y
hwx₁ : ∑ y in s, wx y = 1
wy : E → R
hwy₀ : ∀ (y : E), y ∈ s → 0 ≤ wy y
hwy₁ : ∑ y in s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : E
hi : i ∈ s
⊢ 0 ≤ a * wx i + b * wy i
case refine'_2.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
wx : E → R
hwx₀ : ∀ (y : E), y ∈ s → 0 ≤ wx y
hwx₁ : ∑ y in s, wx y = 1
wy : E → R
hwy₀ : ∀ (y : E), y ∈ s → 0 ≤ wy y
hwy₁ : ∑ y in s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∀ (y : E), y ∈ s → 0 ≤ a * wx y + b * wy y
rintro i hi
no goals
case refine'_2.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
wx : E → R
hwx₀ : ∀ (y : E), y ∈ s → 0 ≤ wx y
hwx₁ : ∑ y in s, wx y = 1
wy : E → R
hwy₀ : ∀ (y : E), y ∈ s → 0 ≤ wy y
hwy₁ : ∑ y in s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : E
hi : i ∈ s
⊢ 0 ≤ a * wx i + b * wy i
apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀]
no goals
case refine'_2.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
wx : E → R
hwx₀ : ∀ (y : E), y ∈ s → 0 ≤ wx y
hwx₁ : ∑ y in s, wx y = 1
wy : E → R
hwy₀ : ∀ (y : E), y ∈ s → 0 ≤ wy y
hwy₁ : ∑ y in s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ y in s, (a * wx y + b * wy y) = 1
simp only [Finset.sum_add_distrib, Finset.mul_sum.symm, mul_one, *]
case refine'_3.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
w : E → R
hw₀ : ∀ (y : E), y ∈ s → 0 ≤ w y
hw₁ : ∑ y in s, w y = 1
⊢ centerMass s w id ∈ ↑(convexHull R).toOrderHom ↑s
case refine'_3
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
⊢ {x | ∃ w x_1 x_2, centerMass s w id = x} ⊆ ↑(convexHull R).toOrderHom ↑s
rintro _ ⟨w, hw₀, hw₁, rfl⟩
no goals
case refine'_3.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.221124
ι : Type ?u.221127
ι' : Type ?u.221130
α : Type ?u.221133
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 : Finset E
w : E → R
hw₀ : ∀ (y : E), y ∈ s → 0 ≤ w y
hw₁ : ∑ y in s, w y = 1
⊢ centerMass s w id ∈ ↑(convexHull R).toOrderHom ↑s
exact
  s.centerMass_mem_convexHull (fun x hx => hw₀ _ hx) (hw₁.symm ▸ zero_lt_one) fun x hx => hx