R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
⊢ (∀ (t : Finset E) (w : E → R),
      (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s) →
    Convex R s
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
⊢ Convex R s ↔
    ∀ (t : Finset E) (w : E → R),
      (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
refine' ⟨fun hs t w hw₀ hw₁ hts => hs.sum_mem hw₀ hw₁ hts, _⟩
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
⊢ (∀ (t : Finset E) (w : E → R),
      (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s) →
    Convex R s
intro h x hx y hy a b ha hb hab
case pos
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : x = y
⊢ a • x + b • y ∈ s

case neg
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ a • x + b • y ∈ s
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s
by_cases h_cases : x = y
case pos
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : x = y
⊢ y ∈ s
case pos
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : x = y
⊢ a • x + b • y ∈ s
rw [h_cases, ← add_smul, hab, one_smul]
no goals
case pos
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : x = y
⊢ y ∈ s
exact hy
case h.e'_4
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ a • x + b • y = ∑ x in {x, y}, (if x = y then b else a) • x

case neg.convert_1
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ ∀ (i : E), i ∈ {x, y} → 0 ≤ (fun z => if z = y then b else a) i

case neg.convert_2
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ ∑ i in {x, y}, (fun z => if z = y then b else a) i = 1

case neg.convert_3
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ ∀ (x_1 : E), x_1 ∈ {x, y} → x_1 ∈ s
case neg
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ a • x + b • y ∈ s
convert h {x, y} (fun z => if z = y then b else a) _ _ _
no goals
case h.e'_4
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ a • x + b • y = ∑ x in {x, y}, (if x = y then b else a) • x
simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial]
case neg.convert_1
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
a✝ : i ∈ {x, y}
⊢ 0 ≤ (fun z => if z = y then b else a) i
case neg.convert_1
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ ∀ (i : E), i ∈ {x, y} → 0 ≤ (fun z => if z = y then b else a) i
intro i _
case neg.convert_1
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
a✝ : i ∈ {x, y}
⊢ 0 ≤ if i = y then b else a
case neg.convert_1
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
a✝ : i ∈ {x, y}
⊢ 0 ≤ (fun z => if z = y then b else a) i
simp only
no goals
case neg.convert_1
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
a✝ : i ∈ {x, y}
⊢ 0 ≤ if i = y then b else a
split_ifs <;> assumption
no goals
case neg.convert_2
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ ∑ i in {x, y}, (fun z => if z = y then b else a) i = 1
simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial, hab]
case neg.convert_3
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
hi : i ∈ {x, y}
⊢ i ∈ s
case neg.convert_3
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ ∀ (x_1 : E), x_1 ∈ {x, y} → x_1 ∈ s
intro i hi
case neg.convert_3
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
hi : i = x ∨ i = y
⊢ i ∈ s
case neg.convert_3
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
hi : i ∈ {x, y}
⊢ i ∈ s
simp only [Finset.mem_singleton, Finset.mem_insert] at hi
no goals
case neg.convert_3
R : Type u_1
E : Type u_2
F : Type ?u.108718
ι : Type ?u.108721
ι' : Type ?u.108724
α : Type ?u.108727
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
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ (i : E), i ∈ t → 0 ≤ w i) → ∑ i in t, w i = 1 → (∀ (x : E), x ∈ t → x ∈ s) → ∑ x in t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
hi : i = x ∨ i = y
⊢ i ∈ s
cases hi <;> subst i <;> assumption