awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ y ∈ s

Tactic:
hy
-- 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
⊢ y ∈ s

Tactic:
exact hy
-- 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
⊢ ∑ x ∈ {x, y}, (if x = y then b else a) • x ∈ s

Tactic:
h { x, y } (fun z => if z = y then b else a) _ _ _

Premises used: Insert.insert, Singleton.singleton, Eq, ite
-- 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
h₁ : a • x + b • y = ∑ x ∈ {x, y}, (if x = y then b else a) • x
neg :
  ∀ (i : E), Membership.mem (γ := Finset E) {x, y} i → LE.le.{u_1} (α := R) 0 ((fun (z : E) ↦ if z = y then b else a) i)
neg₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ {x, y}, (fun (z : E) ↦ if z = y then b else a) i) 1
neg₂ : ∀ (x_1 : E), Membership.mem (γ := Finset E) {x, y} x_1 → x_1 ∈ s
⊢ a • x + b • y ∈ s

Tactic:
convert! h { x, y } (fun z => if z = y then b else a) _ _ _

Premises used: Insert.insert, Singleton.singleton, Eq, ite
-- 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
⊢ a • x + b • y = ∑ x ∈ {x, y}, (if x = y then b else a) • x

Tactic:
simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial]

Premises used: trivial, Finset.sum_pair, if_pos, if_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
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
⊢ ∀ (i : E), Membership.mem (γ := Finset E) {x, y} i → LE.le.{u_1} (α := R) 0 ((fun (z : E) ↦ if z = y then b else a) i)

Tactic:
grind
-- 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
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ {x, y}, (fun (z : E) ↦ if z = y then b else a) i) 1

Tactic:
simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial, hab]

Premises used: trivial, Finset.sum_pair, if_pos, if_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
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
i : E
hi : Membership.mem (γ := Finset E) {x, y} i
⊢ i = x ∨ i = y

Tactic:
simp only [Finset.mem_singleton, Finset.mem_insert] at hi

Premises used: Finset.mem_singleton, Finset.mem_insert
-- 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
i : E
hi : i = x ∨ i = y
neg : i = x → i ∈ s
neg₁ : i = y → i ∈ s
⊢ i ∈ s

Tactic:
cases hi
-- 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
i : E
h_1 : i = x
neg : x ∈ s
⊢ i ∈ s

Tactic:
subst i
-- 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
i : E
h_1 : i = y
neg : y ∈ s
⊢ i ∈ s

Tactic:
subst i
-- 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
⊢ x ∈ s

Tactic:
assumption
-- 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
⊢ y ∈ s

Tactic:
assumption
-- 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
refine₁ :
  ∀
    (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), a • x + b • y ∈ s
pos :
  ∀
    (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),
    a • x + b • y ∈ s
neg neg₁ :
  ∀
    (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),
    a • x + b • y ∈ 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:
classical
  refine ⟨fun hs t w hw₀ hw₁ hts => hs.sum_mem hw₀ hw₁ hts, ?_⟩
  intro h x hx y hy a b ha hb hab
  by_cases h_cases : x = y
  · rw [h_cases, ← add_smul, hab, one_smul]
    exact hy
  · convert! h { x, y } (fun z => if z = y then b else a) _ _ _
    · simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial]
    · grind
    · simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial, hab]
    · intro i hi
      simp only [Finset.mem_singleton, Finset.mem_insert] at hi
      cases hi <;> subst i <;> assumption

Premises used: Finset.mem_singleton, trivial, Finset.mem_insert, if_pos, one_smul, add_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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
t : Finset ι
w : ι → R
hw₀ : ∀ i ∈ t, 0 ≤ w i
hws : LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i)
z : ι → E
hz : ∀ i ∈ t, z i ∈ s
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) (t.centerMass w z)

Tactic:
(convex_convexHull R s).centerMass_mem hw₀ hws fun i hi => subset_convexHull R s <| hz i hi

Premises used: Convex.centerMass_mem, subset_convexHull, convex_convexHull
-- 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
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
t : Finset ι
hw₀ : ∀ i ∈ t, w i ≤ 0
hws : LT.lt.{u_1} (α := R) (∑ i ∈ t, w i) 0
hz : ∀ i ∈ t, z i ∈ s
rw : Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) (t.centerMass (-w) z)
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) (t.centerMass w z)

Tactic:
rw [← centerMass_neg_left]

Premises used: Finset.centerMass_neg_left
-- 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
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
t : Finset ι
hw₀ : ∀ i ∈ t, w i ≤ 0
hws : LT.lt.{u_1} (α := R) (∑ i ∈ t, w i) 0
hz : ∀ i ∈ t, z i ∈ s
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, -w i)

Tactic:
simpa
-- 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
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
t : Finset ι
hw₀ : ∀ i ∈ t, w i ≤ 0
hws : LT.lt.{u_1} (α := R) (∑ i ∈ t, w i) 0
hz : ∀ i ∈ t, z i ∈ s
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) (t.centerMass (-w) z)

Tactic:
exact Finset.centerMass_mem_convexHull _ (fun _i hi ↦ neg_nonneg.2 <| hw₀ _ hi) (by simpa) hz

Premises used: Iff.mpr, Finset.centerMass_mem_convexHull, neg_nonneg
-- 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
t : Finset E
w : E → R
hw₀ : ∀ i ∈ t, 0 ≤ w i
hws : LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i)
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E) (t.centerMass w id)

Tactic:
t.centerMass_mem_convexHull hw₀ hws fun _ => mem_coe.2

Premises used: Iff.mpr, Finset.centerMass_mem_convexHull, Finset.mem_coe
-- 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
t : Finset E
w : E → R
hw₀ : ∀ i ∈ t, w i ≤ 0
hws : LT.lt.{u_1} (α := R) (∑ i ∈ t, w i) 0
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E) (t.centerMass w id)

Tactic:
t.centerMass_mem_convexHull_of_nonpos hw₀ hws fun _ ↦ mem_coe.2

Premises used: Iff.mpr, Finset.mem_coe, Finset.centerMass_mem_convexHull_of_nonpos
-- 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
ι : Type u_8
t : Finset ι
p : ι → E
w : ι → R
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
rw : Eq.{u_3 + 1} (α := E) (∑ i ∈ t, w i • (p i -ᵥ 0)) (∑ i ∈ t, w i • p i)
⊢ (affineCombination R t p : (a : ι → R) → E) w = t.centerMass w p

Tactic:
rw [affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ w _ hw₂ (0 : E),
    Finset.weightedVSubOfPoint_apply, vadd_eq_add, add_zero, t.centerMass_eq_of_sum_1 _ hw₂]

Premises used: Finset.weightedVSubOfPoint_apply, Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, vadd_eq_add, Finset.centerMass_eq_of_sum_1, add_zero, OfNat.ofNat
-- 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
ι : Type u_8
t : Finset ι
p : ι → E
w : ι → R
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
simp_rw : Eq.{u_3 + 1} (α := E) (∑ x ∈ t, w x • (p x - 0)) (∑ i ∈ t, w i • p i)
⊢ Eq.{u_3 + 1} (α := E) (∑ i ∈ t, w i • (p i -ᵥ 0)) (∑ i ∈ t, w i • p i)

Tactic:
simp_rw [vsub_eq_sub, sub_zero]

Premises used: sub_zero, vsub_eq_sub
-- 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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
rw : Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (Set.range v) : Set E) (s.centerMass w v)
⊢ Membership.mem (α := E) (γ := Set E) ((convexHull R : (a : Set E) → Set E) (Set.range v) : Set E)
    ((affineCombination R s v : (a : ι → R) → E) w : E)

Tactic:
rw [affineCombination_eq_centerMass hw₁]

Premises used: affineCombination_eq_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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
hws : LT.lt.{u_1} (α := R) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, v i ∈ Set.range v
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (Set.range v) : Set E) (s.centerMass w v)

Tactic:
apply s.centerMass_mem_convexHull hw₀

Premises used: Finset.centerMass_mem_convexHull
-- 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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ s, w i)

Tactic:
simp [hw₁]
-- 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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ ∀ i ∈ s, v i ∈ Set.range v

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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Finset ι
hs : s.Nonempty
p : ι → E
⊢ centroid R s p = s.centerMass (centroidWeights R s) p

Tactic:
affineCombination_eq_centerMass (s.sum_centroidWeights_eq_one_of_nonempty R hs)

Premises used: Finset.sum_centroidWeights_eq_one_of_nonempty, Finset.centroid, affineCombination_eq_centerMass
-- 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
s : Finset E
hs : s.Nonempty
rw :
  Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E)
    (s.centerMass (centroidWeights R s) id)
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E) (centroid R s id)

Tactic:
rw [s.centroid_eq_centerMass hs]

Premises used: Finset.centroid_eq_centerMass
-- 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
s : Finset E
hs : s.Nonempty
hw₀ : ∀ i ∈ s, 0 ≤ centroidWeights R s i
hws : LT.lt.{u_1} (α := R) 0 (∑ i ∈ s, centroidWeights R s i)
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E)
    (s.centerMass (centroidWeights R s) id)

Tactic:
apply s.centerMass_id_mem_convexHull

Premises used: Finset.centerMass_id_mem_convexHull
-- 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
s : Finset E
hs : s.Nonempty
⊢ ∀ i ∈ s, 0 ≤ centroidWeights R s i

Tactic:
simp only [inv_nonneg, imp_true_iff, Nat.cast_nonneg, Finset.centroidWeights_apply]

Premises used: Nat.cast_nonneg, Finset.centroidWeights_apply, imp_true_iff, inv_nonneg
-- 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
s : Finset E
hs : s.Nonempty
⊢ Ne.{u_1 + 1} (α := R) (↑(#s) : R) 0

Tactic:
simp [Finset.nonempty_iff_ne_empty.mp hs]

Premises used: Finset.nonempty_iff_ne_empty, Iff.mp
-- 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
s : Finset E
hs : s.Nonempty
⊢ Ne.{u_1 + 1} (α := R) (↑(#s) : R) 0

Tactic:
have hs_card : (#s : R) ≠ 0 := by simp [Finset.nonempty_iff_ne_empty.mp hs]
-- 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
s : Finset E
hs : s.Nonempty
hs_card : Ne.{u_1 + 1} (α := R) (↑(#s) : R) 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ s, centroidWeights R s i)

Tactic:
simp only [hs_card, Finset.sum_const, nsmul_eq_mul, mul_inv_cancel₀, Ne, not_false_iff,
      Finset.centroidWeights_apply, zero_lt_one]

Premises used: mul_inv_cancel₀, Ne, Finset.centroidWeights_apply, zero_lt_one, nsmul_eq_mul, not_false_iff, Finset.sum_const
-- 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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) (Set.range v) : Set E)
    ({x : E |
        ∃ (s : Finset ι) (w : ι → R),
          (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v : (a : ι → R) → E) w = x} :
      Set E)

Tactic:
Subset.antisymm (convexHull_min ?_ ?_) ?_

Premises used: Set.Subset.antisymm, convexHull_min
-- 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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
refine_1 :
  Set.range v ⊆
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v : (a : ι → R) → E) w = x}
refine_2 :
  Convex.{u_1, u_3} R (E := E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v : (a : ι → R) → E) w = x}
refine_3 :
  Subset.{u_3} (α := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v : (a : ι → R) → E) w = x}
    ((convexHull R : (a : Set E) → Set E) (Set.range v))
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) (Set.range v) : Set E)
    ({x : E |
        ∃ (s : Finset ι) (w : ι → R),
          (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v : (a : ι → R) → E) w = x} :
      Set E)

Tactic:
refine Subset.antisymm (convexHull_min ?_ ?_) ?_
-- 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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
x : E
hx : x ∈ Set.range v
refine_1 :
  ∀ (i : ι) (hi : v i = x),
    Membership.mem (γ := Set E)
      {x : E |
        ∃ (s : Finset ι) (w : ι → R),
          (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v : (a : ι → R) → E) w = x}
      x
⊢ Membership.mem (γ := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v : (a : ι → R) → E) w = x}
    x

Tactic:
obtain ⟨i, hi⟩ := Set.mem_range.mp hx

Premises used: Set.mem_range, 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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
x : E
hx : x ∈ Set.range v
i : ι
hi : v i = x
⊢ ∀ (i_1 : ι), Membership.mem (γ := Finset ι) {i} i_1 → LE.le.{u_1} (α := R) 0 (const ι 1 i_1)

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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
x : E
hx : x ∈ Set.range v
i : ι
hi : v i = x
⊢ Eq.{u_1 + 1} (α := R) (Finset.sum {i} (const ι 1)) 1

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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
x : E
hx : x ∈ Set.range v
i : ι
hi : v i = x
⊢ (affineCombination R {i} v : (a : ι → R) → E) (const ι 1) = x

Tactic:
simp [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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
x : E
hx : x ∈ Set.range v
i : ι
hi : v i = x
⊢ Membership.mem (γ := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v : (a : ι → R) → E) w = x}
    x

Tactic:
exact ⟨{i}, Function.const ι (1 : R), by simp, by simp, by simp [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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
h : ∀ x ∈ s', x ∈ s'
h₁ : ∀ x ∈ s, x ∈ s
rw : ∀ x ∈ s ∪ s', x ∉ s' → (if x ∈ s' then b * w' x else 0) = 0
rw₁ : ∀ x ∈ s ∪ s', x ∉ s → (if x ∈ s then a * w x else 0) = 0
⊢ (s ∪ s').sum W = 1

Tactic:
rw [sum_add_distrib, ← sum_subset subset_union_left,
        ← sum_subset subset_union_right, sum_ite_of_true,
        sum_ite_of_true, ← mul_sum, ← mul_sum, hw₁, hw₁', ← add_mul, hab,
        mul_one]

Premises used: add_mul, Finset.mul_sum, Finset.sum_add_distrib, Finset.subset_union_left, Finset.sum_subset, Finset.sum_ite_of_true, mul_one, Finset.subset_union_right