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
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
rw :
  Eq.{u_3 + 1} (α := E) (∑ x ∈ t, HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ x ∈ t', w x)⁻¹ (w x • z x))
    (∑ x ∈ t', HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ i ∈ t', w i)⁻¹ (w x • z x))
⊢ t.centerMass w z = t'.centerMass w z

Tactic:
rw [centerMass, sum_subset ht h, smul_sum, centerMass, smul_sum]

Premises used: Finset.sum_subset, Finset.smul_sum, Finset.centerMass
-- 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
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
apply : ∀ x ∈ t', x ∉ t → HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ x ∈ t', w x)⁻¹ (w x • z x) = 0
⊢ Eq.{u_3 + 1} (α := E) (∑ x ∈ t, HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ x ∈ t', w x)⁻¹ (w x • z x))
    (∑ x ∈ t', HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ i ∈ t', w i)⁻¹ (w x • z x))

Tactic:
apply sum_subset ht

Premises used: Finset.sum_subset
-- 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
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
i : ι
hit' : i ∈ t'
hit : i ∉ t
rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ x ∈ t', w x)⁻¹ (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 (z i)) = 0
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ x ∈ t', w x)⁻¹ 0 = 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := E) 0 0
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ x ∈ t', w x)⁻¹ (w i • z i) = 0

Tactic:
rw [h i hit' hit, zero_smul, smul_zero]

Premises used: smul_zero, zero_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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : (i : ι) → Decidable (w i ≠ 0)
i : ι
hit : i ∈ t
hit' : i ∉ {i ∈ t | w i ≠ 0}
⊢ w i = 0

Tactic:
simpa only [hit, mem_filter, true_and, Ne, Classical.not_not] using hit'

Premises used: Classical.not_not, Ne, Finset.mem_filter, true_and
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
ι : Type u_5
ι' : Type u_6
α : Type u_7
inst : Field R
inst_1 : Field R'
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : AddCommGroup α
inst_5 : LinearOrder α
inst_6 : Module R E
inst_7 : Module R F
inst_8 : Module R α
s : Set E
i j : ι
c : R
t : Finset ι
w_1 : ι → R
z : ι → E
inst_9 : LinearOrder R
inst_10 : IsOrderedAddMonoid α
inst_11 : PosSMulMono R α
f : ι → α
w : ι → R
hw₀ : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := R) 0 (∑ i ∈ ∅, w i)
⊢ False

Tactic:
simp at hw₁
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
ι : Type u_5
α : Type u_7
inst : Field R
inst_1 : AddCommGroup α
inst_2 : LinearOrder α
inst_3 : Module R α
inst_4 : LinearOrder R
inst_5 : IsOrderedAddMonoid α
inst_6 : PosSMulMono R α
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := R) 0 (∑ i ∈ s, w i)
rw : LE.le.{u_7} (α := α) (∑ i ∈ s, w i • f i) (∑ i ∈ s, w i • s.sup' ⋯ f)
⊢ s.centerMass w f ≤ s.sup' ⋯ f

Tactic:
rw [centerMass, inv_smul_le_iff_of_pos hw₁, sum_smul]

Premises used: Finset.sum_smul, inv_smul_le_iff_of_pos, Finset.centerMass
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
ι : Type u_5
α : Type u_7
inst : Field R
inst_1 : AddCommGroup α
inst_2 : LinearOrder α
inst_3 : Module R α
inst_4 : LinearOrder R
inst_5 : IsOrderedAddMonoid α
inst_6 : PosSMulMono R α
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := R) 0 (∑ i ∈ s, w i)
⊢ LE.le.{u_7} (α := α) (∑ i ∈ s, w i • f i) (∑ i ∈ s, w i • s.sup' ⋯ f)

Tactic:
sum_le_sum fun i hi => smul_le_smul_of_nonneg_left (le_sup' _ hi) <| hw₀ i hi

Premises used: Finset.sum_le_sum, Finset.le_sup', smul_le_smul_of_nonneg_left
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
ι : Type u_5
α : Type u_7
inst : Field R
inst_1 : AddCommGroup α
inst_2 : LinearOrder α
inst_3 : Module R α
inst_4 : LinearOrder R
inst_5 : IsOrderedAddMonoid α
inst_6 : PosSMulMono R α
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := R) 0 (∑ i ∈ s, w i)
⊢ LE.le.{u_7} (α := α) (∑ i ∈ s, w i • f i) (∑ i ∈ s, w i • s.sup' ⋯ f)

Tactic:
exact sum_le_sum fun i hi => smul_le_smul_of_nonneg_left (le_sup' _ hi) <| hw₀ i hi

Premises used: Finset.sum_le_sum, smul_le_smul_of_nonneg_left
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
ι : Type u_5
α : Type u_7
inst : Field R
inst_1 : AddCommGroup α
inst_2 : LinearOrder α
inst_3 : Module R α
inst_4 : LinearOrder R
inst_5 : IsOrderedAddMonoid α
inst_6 : PosSMulMono R α
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := R) 0 (∑ i ∈ s, w i)
⊢ s.inf' ⋯ f ≤ s.centerMass w f

Tactic:
centerMass_le_sup (α := αᵒᵈ) hw₀ hw₁

Premises used: Finset.inf', WithTop.some, WithTop.untop, Finset.centerMass_le_sup, OrderDual, Finset.inf, WithTop
-- 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
t : Finset ι
w : ι → R
hw : Ne.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
c : E
⊢ t.centerMass w (const ι c) = c

Tactic:
simp [centerMass, ← sum_smul, hw]

Premises used: Finset.sum_smul, Finset.centerMass
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
rw :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i • z' i)
⊢ t.centerMass w z = t'.centerMass w' z'

Tactic:
rw [← centerMass_filter_ne_zero, centerMass, ← centerMass_filter_ne_zero, centerMass]

Premises used: Finset.centerMass_filter_ne_zero, Finset.centerMass
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
e_a : Eq.{u_1 + 1} (α := R) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹
e_a₁ : Eq.{u_3 + 1} (α := E) (∑ i ∈ t with w i ≠ 0, w i • z i) (∑ i ∈ t' with w' i ≠ 0, w' i • z' i)
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i • z' i)

Tactic:
congr 1
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
e_a : Eq.{u_1 + 1} (α := R) (∑ i ∈ t with w i ≠ 0, w i) (∑ i ∈ t' with w' i ≠ 0, w' i)
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹

Tactic:
congr 1
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ {i ∈ t | w i ≠ 0} = {i ∈ t' | w' i ≠ 0}

Tactic:
grind
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ ∀ x ∈ {i ∈ t' | w' i ≠ 0}, w x = w' x

Tactic:
grind
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ t with w i ≠ 0, w i) (∑ i ∈ t' with w' i ≠ 0, w' i)

Tactic:
exact sum_congr (by grind) (by grind)

Premises used: Finset.sum_congr
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ ∀ x ∈ {i ∈ t' | w' i ≠ 0}, w x • z x = w' x • z' x

Tactic:
grind
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ Eq.{u_3 + 1} (α := E) (∑ i ∈ t with w i ≠ 0, w i • z i) (∑ i ∈ t' with w' i ≠ 0, w' i • z' i)

Tactic:
exact sum_congr (by grind) (by grind)

Premises used: Finset.sum_congr
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
rw : {i ∈ t | w i ≠ 0}.centerMass w z = t'.centerMass w' z'
rw₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    t'.centerMass w' z'
rw₂ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    {i ∈ t' | w' i ≠ 0}.centerMass w' z'
rw₃ rw₄ rw₅ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i • z' i)
e_a : Eq.{u_1 + 1} (α := R) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹
e_a₁ e_a₂ : Eq.{u_3 + 1} (α := E) (∑ i ∈ t with w i ≠ 0, w i • z i) (∑ i ∈ t' with w' i ≠ 0, w' i • z' i)
⊢ t.centerMass w z = t'.centerMass w' z'

Tactic:
classical
  rw [← centerMass_filter_ne_zero, centerMass, ← centerMass_filter_ne_zero, centerMass]
  congr 1
  · congr 1
    exact sum_congr (by grind) (by grind)
  · exact sum_congr (by grind) (by grind)

Premises used: Finset.centerMass_filter_ne_zero, Finset.centerMass, Finset.sum_congr
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
h : ∀ i ∈ t ∪ t', w i ≠ 0 → i ∈ t ∩ t'
⊢ ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w i ≠ 0 → i ∈ t ∩ t' ∧ w i = w i ∧ z i = z i

Tactic:
grind
-- 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
t : Finset ι
w : ι → R
z : ι → E
w' : ι → R
h : ∀ i ∈ t, w i = w' i
⊢ ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t ∧ w' i ≠ 0 → i ∈ t ∩ t ∧ w i = w' i ∧ z i = z i

Tactic:
grind
-- 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
t : Finset ι
w : ι → R
z : ι → E
w' : ι → R
h : ∀ i ∈ t, w i = w' i
⊢ t.centerMass w z = t.centerMass w' z

Tactic:
exact centerMass_congr (by grind)

Premises used: Finset.centerMass_congr
-- 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
t : Finset ι
w : ι → R
z : ι → E
w' : ι → R
h : ∀ i ∈ t, w i = w' i
⊢ t.centerMass w z = t.centerMass w' z

Tactic:
classical
  exact centerMass_congr (by grind)

Premises used: Finset.centerMass_congr
-- 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
t : Finset ι
w : ι → R
z z' : ι → E
h : ∀ i ∈ t, w i ≠ 0 → z i = z' i
⊢ ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t ∧ w i ≠ 0 → i ∈ t ∩ t ∧ w i = w i ∧ z i = z' i

Tactic:
grind
-- 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
t : Finset ι
w : ι → R
z z' : ι → E
h : ∀ i ∈ t, w i ≠ 0 → z i = z' i
⊢ t.centerMass w z = t.centerMass w z'

Tactic:
exact centerMass_congr (by grind)

Premises used: Finset.centerMass_congr
-- 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
t : Finset ι
w : ι → R
z z' : ι → E
h : ∀ i ∈ t, w i ≠ 0 → z i = z' i
⊢ t.centerMass w z = t.centerMass w z'

Tactic:
classical
  exact centerMass_congr (by grind)

Premises used: Finset.centerMass_congr
-- 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
w : ι → R
z : ι → E
s t : Finset ι
hw : HAdd.hAdd (α := R) (∑ i ∈ s, w i) (∑ i ∈ t, w i) = 0
hz : HAdd.hAdd (α := E) (∑ i ∈ s, w i • z i) (∑ i ∈ t, w i • z i) = 0
⊢ s.centerMass w z = t.centerMass w z

Tactic:
simp [centerMass, eq_neg_of_add_eq_zero_right hw, eq_neg_of_add_eq_zero_left hz]

Premises used: eq_neg_of_add_eq_zero_left, Finset.centerMass, eq_neg_of_add_eq_zero_right
-- 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
⊢ (∀ (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

Tactic:
simp
-- 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 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ insert i t, w i)
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
⊢ z i ∈ s

Tactic:
have zi : z i ∈ s := hmem _ (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 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ insert i t, w i)
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
⊢ ∀ j ∈ t, 0 ≤ w j

Tactic:
have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
-- 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 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ insert i t, w i)
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
⊢ 0 < w i + ∑ x ∈ t, w x

Tactic:
rw [sum_insert hi] at hpos

Premises used: Finset.sum_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 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ insert i t, w i)
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hpos₁ : 0 < w i + ∑ x ∈ t, w x
⊢ ∀ i_1 ∈ insert i t, z i_1 ∈ s

Tactic:
rw [sum_insert hi] at hpos

Premises used: Finset.sum_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 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ insert i t, w i)
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hpos₁ : 0 < w i + ∑ x ∈ t, w x
hmem₁ : ∀ i_1 ∈ insert i t, z i_1 ∈ s
⊢ z i ∈ s

Tactic:
rw [sum_insert hi] at hpos

Premises used: Finset.sum_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 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ insert i t, w i)
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hpos₁ : 0 < w i + ∑ x ∈ t, w x
hmem₁ : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi₁ : z i ∈ s
⊢ ∀ j ∈ t, 0 ≤ w j

Tactic:
rw [sum_insert hi] at hpos

Premises used: Finset.sum_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
pos : ∀ (hsum_t : Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0), (insert i t).centerMass w z ∈ s
neg : ∀ (hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0), (insert i t).centerMass w z ∈ s
⊢ (insert i t).centerMass w z ∈ s

Tactic:
by_cases hsum_t : ∑ j ∈ t, w j = 0
-- 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 ∈ t, w j = 0

Tactic:
have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
-- 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_1 : ι
t : Finset ι
hi_1 : i_1 ∉ 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 ∈ insert i_1 t, 0 ≤ w i
hpos : 0 < w i_1 + ∑ x ∈ t, w x
hmem : ∀ i ∈ insert i_1 t, z i ∈ s
zi : z i_1 ∈ 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
i : ι
hi : i ∈ t
⊢ w i • z i = 0

Tactic:
simp [ws i hi]
-- 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
ws : ∀ j ∈ t, w j = 0
⊢ Eq.{u_3 + 1} (α := E) (∑ j ∈ t, w j • z j) 0

Tactic:
have wz : ∑ j ∈ t, w j • z j = 0 := sum_eq_zero fun i hi => by simp [ws i hi]
-- 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
ws : ∀ j ∈ t, w j = 0
wz : Eq.{u_3 + 1} (α := E) (∑ j ∈ t, w j • z j) 0
pos : (w i)⁻¹ • w i • z i ∈ s
⊢ (insert i t).centerMass w z ∈ s

Tactic:
simp only [centerMass, sum_insert hi, wz, hsum_t, add_zero]

Premises used: Finset.centerMass, Finset.sum_insert, add_zero
-- 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
ws : ∀ j ∈ t, w j = 0
wz : Eq.{u_3 + 1} (α := E) (∑ j ∈ t, w j • z j) 0
⊢ 0 < w i

Tactic:
simp only [hsum_t, add_zero] at hpos

Premises used: add_zero
-- 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
pos : z i ∈ s
⊢ (w i)⁻¹ • w i • z i ∈ s

Tactic:
rw [← mul_smul, inv_mul_cancel₀ (ne_of_gt hpos), one_smul]

Premises used: ne_of_gt, one_smul, inv_mul_cancel₀, SemigroupAction.mul_smul