-- Mathlib/Analysis/Convex/Combination.lean
theorem Convex.finsum_mem {ι : Sort*} {w : ι → R} {z : ι → E} {s : Set E} (hs : Convex R s)
    (h₀ : ∀ i, 0 ≤ w i) (h₁ : ∑ᶠ i, w i = 1) (hz : ∀ i, w i ≠ 0 → z i ∈ s) :
    (∑ᶠ i, w i • z i) ∈ s

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : (support (w ∘ PLift.down)).Finite
hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ ↑hfin_w.toFinset
⊢ ∑ i ∈ hfin_w.toFinset, w i.down • z i.down ∈ s

Tactic:
refine hs.sum_mem (fun _ _ => h₀ _) ?_ fun i hi => hz _ ?_

Result:
case refine_1
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : (support (w ∘ PLift.down)).Finite
hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ ↑hfin_w.toFinset
⊢ ∑ i ∈ hfin_w.toFinset, w i.down = 1

case refine_2
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : (support (w ∘ PLift.down)).Finite
hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ ↑hfin_w.toFinset
i : PLift ι
hi : i ∈ hfin_w.toFinset
⊢ w i.down ≠ 0

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
⊢ (support (w ∘ PLift.down)).Finite

Tactic:
by_contra H

Result:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
H : ¬(support (w ∘ PLift.down)).Finite
⊢ False

Proof state:
case refine_1
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : (support (w ∘ PLift.down)).Finite
hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ ↑hfin_w.toFinset
⊢ ∑ i ∈ hfin_w.toFinset, w i.down = 1

Tactic:
rwa [finsum, dif_pos hfin_w] at h₁

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
H : ¬(support (w ∘ PLift.down)).Finite
⊢ False

Tactic:
rw [finsum, dif_neg H] at h₁

Result:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : 0 = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
H : ¬(support (w ∘ PLift.down)).Finite
⊢ False

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
⊢ ∑ᶠ (i : ι), w i • z i ∈ s

Tactic:
have hfin_w : (support (w ∘ PLift.down)).Finite := by
  by_contra H
  rw [finsum, dif_neg H] at h₁
  exact zero_ne_one h₁

Result:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : (support (w ∘ PLift.down)).Finite
⊢ ∑ᶠ (i : ι), w i • z i ∈ s

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : (support (w ∘ PLift.down)).Finite
hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ ↑hfin_w.toFinset
⊢ ∑ᶠ (i : ι), w i • z i ∈ s

Tactic:
rw [finsum_eq_sum_plift_of_support_subset hsub]

Result:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : (support (w ∘ PLift.down)).Finite
hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ ↑hfin_w.toFinset
⊢ ∑ i ∈ hfin_w.toFinset, w i.down • z i.down ∈ s

Proof state:
case refine_2
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : (support (w ∘ PLift.down)).Finite
hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ ↑hfin_w.toFinset
i : PLift ι
hi : i ∈ hfin_w.toFinset
⊢ w i.down ≠ 0

Tactic:
rwa [hfin_w.mem_toFinset] at hi

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : 0 = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
H : ¬(support (w ∘ PLift.down)).Finite
⊢ False

Tactic:
exact zero_ne_one h₁

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : (support (w ∘ PLift.down)).Finite
⊢ ∑ᶠ (i : ι), w i • z i ∈ s

Tactic:
have hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ hfin_w.toFinset :=
  (support_smul_subset_left _ _).trans hfin_w.coe_toFinset.ge

Result:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : ∑ᶠ (i : ι), w i = 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : (support (w ∘ PLift.down)).Finite
hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ ↑hfin_w.toFinset
⊢ ∑ᶠ (i : ι), w i • z i ∈ s