awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
ws : ∀ j ∈ t, w j = 0
wz : Eq.{u_3 + 1} (α := E) (∑ j ∈ t, w j • z j) 0
hpos : 0 < w i
⊢ z i ∈ s

Tactic:
zi
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
ws : ∀ j ∈ t, w j = 0
wz : Eq.{u_3 + 1} (α := E) (∑ j ∈ t, w j • z j) 0
hpos : 0 < w i
⊢ z i ∈ s

Tactic:
exact zi
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
neg : (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z ∈ s
⊢ (insert i t).centerMass w z ∈ s

Tactic:
rw [Finset.centerMass_insert _ _ _ hi hsum_t]

Premises used: Finset.centerMass_insert
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
⊢ (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z ∈ s

Tactic:
convex_iff_div.1 hs zi (ht hs₀ ?_ ?_) ?_ (sum_nonneg hs₀) hpos

Premises used: Finset.sum_nonneg, convex_iff_div, Iff.mp
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
neg : LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i)
neg₁ : ∀ i ∈ t, z i ∈ s
neg₂ : 0 ≤ w i
⊢ (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z ∈ s

Tactic:
refine convex_iff_div.1 hs zi (ht hs₀ ?_ ?_) ?_ (sum_nonneg hs₀) hpos

Premises used: Finset.sum_nonneg, convex_iff_div, Iff.mp
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i)

Tactic:
lt_of_le_of_ne (sum_nonneg hs₀) (Ne.symm hsum_t)

Premises used: Ne.symm, Finset.sum_nonneg, lt_of_le_of_ne
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i)

Tactic:
exact lt_of_le_of_ne (sum_nonneg hs₀) (Ne.symm hsum_t)

Premises used: Ne.symm, Finset.sum_nonneg, lt_of_le_of_ne
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
j : ι
hj : j ∈ t
⊢ z j ∈ s

Tactic:
hmem j (mem_insert_of_mem hj)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
j : ι
hj : j ∈ t
⊢ z j ∈ s

Tactic:
exact hmem j (mem_insert_of_mem hj)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
⊢ 0 ≤ w i

Tactic:
h₀ _ (mem_insert_self _ _)

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
⊢ 0 ≤ w i

Tactic:
exact h₀ _ (mem_insert_self _ _)

Premises used: Finset.mem_insert_self
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
empty :
  (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ w i) →
    LT.lt.{u_1} (α := R) 0 (∑ i ∈ ∅, w i) →
      (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → z i ∈ s) → centerMass ∅ w z ∈ s
insert :
  ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
    (ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s),
    (∀ i_1 ∈ Insert.insert i t, 0 ≤ w i_1) →
      LT.lt.{u_1} (α := R) 0 (∑ i ∈ Insert.insert i t, w i) →
        (∀ i_1 ∈ Insert.insert i t, z i_1 ∈ s) → (Insert.insert i t).centerMass w z ∈ s
⊢ (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s

Tactic:
induction t using Finset.induction with
  | empty => simp
  | insert i t hi ht =>
    intro h₀ hpos hmem
    have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
    have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
    rw [sum_insert hi] at hpos
    by_cases hsum_t : ∑ j ∈ t, w j = 0
    · have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
      have wz : ∑ j ∈ t, w j • z j = 0 := sum_eq_zero fun i hi => by simp [ws i hi]
      simp only [centerMass, sum_insert hi, wz, hsum_t, add_zero]
      simp only [hsum_t, add_zero] at hpos
      rw [← mul_smul, inv_mul_cancel₀ (ne_of_gt hpos), one_smul]
      exact zi
    · rw [Finset.centerMass_insert _ _ _ hi hsum_t]
      refine convex_iff_div.1 hs zi (ht hs₀ ?_ ?_) ?_ (sum_nonneg hs₀) hpos
      · exact lt_of_le_of_ne (sum_nonneg hs₀) (Ne.symm hsum_t)
      · intro j hj
        exact hmem j (mem_insert_of_mem hj)
      · exact h₀ _ (mem_insert_self _ _)

Premises used: Insert.insert, one_smul, Finset.centerMass, add_zero, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
empty :
  (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ w i) →
    LT.lt.{u_1} (α := R) 0 (∑ i ∈ ∅, w i) →
      (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → z i ∈ s) → centerMass ∅ w z ∈ s
insert :
  ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
    (ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s),
    (∀ i_1 ∈ Insert.insert i t, 0 ≤ w i_1) →
      LT.lt.{u_1} (α := R) 0 (∑ i ∈ Insert.insert i t, w i) →
        (∀ i_1 ∈ Insert.insert i t, z i_1 ∈ s) → (Insert.insert i t).centerMass w z ∈ s
⊢ (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s

Tactic:
classical
  induction t using Finset.induction with
  | empty => simp
  | insert i t hi ht =>
    intro h₀ hpos hmem
    have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
    have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
    rw [sum_insert hi] at hpos
    by_cases hsum_t : ∑ j ∈ t, w j = 0
    · have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
      have wz : ∑ j ∈ t, w j • z j = 0 := sum_eq_zero fun i hi => by simp [ws i hi]
      simp only [centerMass, sum_insert hi, wz, hsum_t, add_zero]
      simp only [hsum_t, add_zero] at hpos
      rw [← mul_smul, inv_mul_cancel₀ (ne_of_gt hpos), one_smul]
      exact zi
    · rw [Finset.centerMass_insert _ _ _ hi hsum_t]
      refine convex_iff_div.1 hs zi (ht hs₀ ?_ ?_) ?_ (sum_nonneg hs₀) hpos
      · exact lt_of_le_of_ne (sum_nonneg hs₀) (Ne.symm hsum_t)
      · intro j hj
        exact hmem j (mem_insert_of_mem hj)
      · exact h₀ _ (mem_insert_self _ _)

Premises used: Insert.insert, one_smul, Finset.centerMass, add_zero, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
⊢ ∑ i ∈ t, w i • z i ∈ s

Tactic:
simpa only [h₁, centerMass, inv_one, one_smul] using
    hs.centerMass_mem h₀ (h₁.symm ▸ zero_lt_one) hz

Premises used: Convex.centerMass_mem, inv_one, Eq.rec, one_smul, zero_lt_one, Finset.centerMass, Eq.symm
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
by_contra : ∀ (H : ¬HasFiniteSupport (w ∘ PLift.down)), False
⊢ HasFiniteSupport (w ∘ PLift.down)

Tactic:
by_contra H
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
H : ¬HasFiniteSupport (w ∘ PLift.down)
⊢ Eq.{u_1 + 1} (α := R) 0 1

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

Premises used: finsum, dif_neg
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
H : ¬HasFiniteSupport (w ∘ PLift.down)
h₂ : Eq.{u_1 + 1} (α := R) 0 1
⊢ ∀ (i : ι), w i ≠ 0 → z i ∈ s

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

Premises used: finsum, dif_neg
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
H : ¬HasFiniteSupport (w ∘ PLift.down)
h₂ : Eq.{u_1 + 1} (α := R) 0 1
hz₁ : ∀ (i : ι), w i ≠ 0 → z i ∈ s
⊢ ¬HasFiniteSupport (w ∘ PLift.down)

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

Premises used: finsum, dif_neg
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) 0 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
H : ¬HasFiniteSupport (w ∘ PLift.down)
⊢ False

Tactic:
zero_ne_one h₁

Premises used: zero_ne_one
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) 0 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
H : ¬HasFiniteSupport (w ∘ PLift.down)
⊢ False

Tactic:
exact zero_ne_one h₁

Premises used: zero_ne_one
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
⊢ HasFiniteSupport (w ∘ PLift.down)

Tactic:
have hfin_w : HasFiniteSupport (w ∘ PLift.down) := by
    by_contra H
    rw [finsum, dif_neg H] at h₁
    exact zero_ne_one h₁
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
⊢ support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))

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
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub :
  support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))
rw : ∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down • z i.down ∈ s
⊢ ∑ᶠ (i : ι), w i • z i ∈ s

Tactic:
rw [finsum_eq_sum_plift_of_support_subset hsub]

Premises used: finsum_eq_sum_plift_of_support_subset
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub :
  support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))
⊢ ∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down • z i.down ∈ s

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

Premises used: PLift.down, Convex.sum_mem
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub :
  support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))
refine_1 : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down) 1
refine_2 : ∀ (i : PLift ι) (hi : i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w), w i.down ≠ 0
⊢ ∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down • z i.down ∈ s

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

Premises used: Convex.sum_mem
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub :
  support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))
refine_1 :
  ∀
    (h₁ :
      Eq.{u_1 + 1} (α := R)
        (if h : HasFiniteSupport.{u_8, u_1} (α := PLift ι) (M := R) ((fun (i : ι) ↦ w i) ∘ PLift.down) then
          ∑ i ∈ Finite.toFinset (s := support.{u_8, u_1} (M := R) ((fun (i : ι) ↦ w i) ∘ PLift.down)) h, w i.down
        else 0)
        1)
    (hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s) (hfin_w : HasFiniteSupport (w ∘ PLift.down))
    (hsub :
      support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
        (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))),
    Eq.{u_1 + 1} (α := R) (∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down) 1
refine_1₁ refine_1₂ refine_1₃ refine_1₄ :
  ∀ (hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s) (hfin_w : HasFiniteSupport (w ∘ PLift.down))
    (h₁ :
      Eq.{u_1 + 1} (α := R)
        (∑ i ∈ Finite.toFinset (s := support.{u_8, u_1} (M := R) ((fun (i : ι) ↦ w i) ∘ PLift.down)) hfin_w, w i.down)
        1)
    (hsub :
      support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
        (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))),
    Eq.{u_1 + 1} (α := R) (∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down) 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down) 1

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

Premises used: finsum, dif_pos
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub :
  support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))
i : PLift ι
hi : i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w
refine_2 refine_2₁ refine_2₂ refine_2₃ : ∀ (hi : i ∈ support (w ∘ PLift.down)), w i.down ≠ 0
⊢ w i.down ≠ 0

Tactic:
rwa [hfin_w.mem_toFinset] at hi

Premises used: Set.Finite.mem_toFinset
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
⊢ Convex R s ↔
    ∀ (t : Finset E) (w : E → R),
      (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s

Tactic:
⟨fun hs t w hw₀ hw₁ hts => hs.sum_mem hw₀ hw₁ hts, ?_⟩

Premises used: Iff.intro, Convex.sum_mem
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
refine :
  (∀ (t : Finset E) (w : E → R),
      (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s) →
    Convex R s
⊢ Convex R s ↔
    ∀ (t : Finset E) (w : E → R),
      (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s

Tactic:
refine ⟨fun hs t w hw₀ hw₁ hts => hs.sum_mem hw₀ hw₁ hts, ?_⟩
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ 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
pos : ∀ (h_cases : x = y), a • x + b • y ∈ s
neg : ∀ (h_cases : ¬x = y), a • x + b • y ∈ s
⊢ a • x + b • y ∈ s

Tactic:
by_cases h_cases : x = y
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ 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
pos : y ∈ s
⊢ a • x + b • y ∈ s

Tactic:
rw [h_cases, ← add_smul, hab, one_smul]

Premises used: one_smul, add_smul