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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sx, wx i) 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sy, wy i) 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Membership.mem (γ := Set E)
    {x : E |
      ∃ (ι : Type) (t : Finset ι) (w : ι → R) (z : ι → E),
        (∀ i ∈ t, 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}
    (centerMass.{u_1, u_3, 0} (R := R) (sx.disjSum sy) (Sum.elim (fun (i : ι) ↦ a * wx i) fun (j : ι') ↦ b * wy j)
      (Sum.elim zx zy))

Tactic:
⟨_, _, _, _, ?_, ?_, ?_, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, rfl
-- 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 : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sx, wx i) 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sy, wy i) 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_2 : ∀ i ∈ sx.disjSum sy, LE.le.{u_1} (α := R) 0 (Sum.elim (fun (i : ι) ↦ a * wx i) (fun (j : ι') ↦ b * wy j) i)
refine_2₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sx.disjSum sy, Sum.elim (fun (i : ι) ↦ a * wx i) (fun (j : ι') ↦ b * wy j) i) 1
refine_2₂ : ∀ i ∈ sx.disjSum sy, Sum.elim zx zy i ∈ s
⊢ Membership.mem (γ := Set E)
    {x : E |
      ∃ (ι : Type) (t : Finset ι) (w : ι → R) (z : ι → E),
        (∀ i ∈ t, 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}
    (centerMass.{u_1, u_3, 0} (R := R) (sx.disjSum sy) (Sum.elim (fun (i : ι) ↦ a * wx i) fun (j : ι') ↦ b * wy j)
      (Sum.elim zx zy))

Tactic:
refine ⟨_, _, _, _, ?_, ?_, ?_, rfl⟩
-- 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 : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sx, wx i) 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sy, wy i) 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι ⊕ ι'
hi : i ∈ sx.disjSum sy
⊢ (∃ a ∈ sx, Sum.inl a = i) ∨ ∃ b ∈ sy, Sum.inr b = i

Tactic:
rw [Finset.mem_disjSum] at hi

Premises used: Finset.mem_disjSum
-- 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 : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sx, wx i) 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sy, wy i) 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι ⊕ ι'
hi : (∃ a ∈ sx, Sum.inl a = i) ∨ ∃ b ∈ sy, Sum.inr b = i
refine_2 :
  ∀ (j : ι) (hj : j ∈ sx),
    LE.le.{u_1} (α := R) 0 (Sum.elim (fun (i : ι) ↦ a * wx i) (fun (j : ι') ↦ b * wy j) (Sum.inl j))
refine_2₁ :
  ∀ (j : ι') (hj : j ∈ sy),
    LE.le.{u_1} (α := R) 0 (Sum.elim (fun (i : ι) ↦ a * wx i) (fun (j : ι') ↦ b * wy j) (Sum.inr j))
⊢ LE.le.{u_1} (α := R) 0 (Sum.elim (fun (i : ι) ↦ a * wx i) (fun (j : ι') ↦ b * wy j) i)

Tactic:
rcases hi with (⟨j, hj, rfl⟩ | ⟨j, hj, rfl⟩)

Premises used: rfl
-- 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 : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sx, wx i) 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sy, wy i) 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
j : ι
hj : j ∈ sx
refine_2 : 0 ≤ a * wx j
⊢ LE.le.{u_1} (α := R) 0 (Sum.elim (fun (i : ι) ↦ a * wx i) (fun (j : ι') ↦ b * wy j) (Sum.inl j))

Tactic:
simp only [Sum.elim_inl, Sum.elim_inr]

Premises used: Sum.elim_inr, Sum.elim_inl
-- 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 : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sx, wx i) 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sy, wy i) 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
j : ι'
hj : j ∈ sy
refine_2 : 0 ≤ b * wy j
⊢ LE.le.{u_1} (α := R) 0 (Sum.elim (fun (i : ι) ↦ a * wx i) (fun (j : ι') ↦ b * wy j) (Sum.inr j))

Tactic:
simp only [Sum.elim_inl, Sum.elim_inr]

Premises used: Sum.elim_inr, Sum.elim_inl
-- 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 : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sx, wx i) 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sy, wy i) 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
j : ι
hj : j ∈ sx
⊢ 0 ≤ a * wx j

Tactic:
apply_rules [mul_nonneg, hwx₀, hwy₀]

Premises used: mul_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 : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sx, wx i) 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sy, wy i) 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
j : ι'
hj : j ∈ sy
⊢ 0 ≤ b * wy j

Tactic:
apply_rules [mul_nonneg, hwx₀, hwy₀]

Premises used: mul_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 : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sx, wx i) 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sy, wy i) 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ sx.disjSum sy, Sum.elim (fun (i : ι) ↦ a * wx i) (fun (j : ι') ↦ b * wy j) i) 1

Tactic:
simp [← mul_sum, *]

Premises used: Finset.mul_sum
-- 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 : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sx, wx i) 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sy, wy i) 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι ⊕ ι'
hi : (∃ a ∈ sx, Sum.inl a = i) ∨ ∃ b ∈ sy, Sum.inr b = i
refine_2 : ∀ (j : ι) (hj : j ∈ sx), Sum.elim zx zy (Sum.inl j) ∈ s
refine_2₁ : ∀ (j : ι') (hj : j ∈ sy), Sum.elim zx zy (Sum.inr j) ∈ s
⊢ Sum.elim zx zy i ∈ s

Tactic:
rcases hi with (⟨j, hj, rfl⟩ | ⟨j, hj, rfl⟩)

Premises used: rfl
-- 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 : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sx, wx i) 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sy, wy i) 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
j : ι
hj : j ∈ sx
⊢ Sum.elim zx zy (Sum.inl j) ∈ s

Tactic:
apply_rules [hzx, hzy]
-- 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 : Set E
ι : Type
sx : Finset ι
wx : ι → R
zx : ι → E
hwx₀ : ∀ i ∈ sx, 0 ≤ wx i
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sx, wx i) 1
hzx : ∀ i ∈ sx, zx i ∈ s
ι' : Type
sy : Finset ι'
wy : ι' → R
zy : ι' → E
hwy₀ : ∀ i ∈ sy, 0 ≤ wy i
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ sy, wy i) 1
hzy : ∀ i ∈ sy, zy i ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
j : ι'
hj : j ∈ sy
⊢ Sum.elim zx zy (Sum.inr j) ∈ s

Tactic:
apply_rules [hzx, hzy]
-- 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 : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
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:
t.centerMass_mem_convexHull hw₀ (hw₁.symm ▸ zero_lt_one) hz

Premises used: Eq.rec, Finset.centerMass_mem_convexHull, zero_lt_one, 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
s : Set E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
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 t.centerMass_mem_convexHull hw₀ (hw₁.symm ▸ zero_lt_one) hz

Premises used: Eq.rec, Finset.centerMass_mem_convexHull, zero_lt_one, Eq.symm
-- 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 : Set E
x : E
inst_5 : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
rw : Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) (centerMass Finset.univ w z)
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) x

Tactic:
rw [← hx, ← centerMass_eq_of_sum_1 _ _ hw₁]

Premises used: Finset.centerMass_eq_of_sum_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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Set E
x : E
inst_5 : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
⊢ ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → 0 ≤ w i

Tactic:
simpa using 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 : Set E
x : E
inst_5 : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
⊢ LT.lt.{u_1} (α := R) 0 (∑ i : ι, 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 : Set E
x : E
inst_5 : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
⊢ ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → z i ∈ s

Tactic:
simpa using hz
-- 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 : Set E
x : E
inst_5 : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) (centerMass Finset.univ w z)

Tactic:
exact centerMass_mem_convexHull _ (by simpa using hw₀) (by simp [hw₁]) (by simpa using hz)

Premises used: Finset.centerMass_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 : Set E
x : E
mp :
  Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) x →
    ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E),
      (∀ (i : ι), 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x
mpr :
  (∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E),
      (∀ (i : ι), 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x) →
    Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) x
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) x ↔
    ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E),
      (∀ (i : ι), 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x

Tactic:
constructor
-- 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 : Set E
x : E
mp :
  (∃ (ι : Type) (t : Finset ι) (w : ι → R) (z : ι → E),
      (∀ i ∈ t, 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x) →
    ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E),
      (∀ (i : ι), 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) x →
    ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E),
      (∀ (i : ι), 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x

Tactic:
simp only [convexHull_eq, mem_setOf_eq]

Premises used: Set.mem_setOf_eq, convexHull_eq
-- 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 : Set E
x : E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
h : (∀ i ∈ t, 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x
⊢ ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E),
    (∀ (i : ι), 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x

Tactic:
⟨t, inferInstance, w ∘ (↑), z ∘ (↑), ?_⟩

Premises used: Function.comp, Membership.mem, inferInstance, Subtype, Exists.intro, Subtype.val
-- 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 : Set E
x : E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
h : (∀ i ∈ t, 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x
mp :
  (∀ (i : ↥t), 0 ≤ (w ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ t)) i) ∧
    Eq.{u_1 + 1} (α := R) (∑ i : ↥t, (w ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ t)) i) 1 ∧
      (∀ (i : ↥t), (z ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ t)) i ∈ s) ∧
        ∑ i : ↥t, (w ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ t)) i • (z ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ t)) i = x
⊢ ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E),
    (∀ (i : ι), 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x

Tactic:
refine ⟨t, inferInstance, w ∘ (↑), z ∘ (↑), ?_⟩
-- 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 : Set E
x : E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
h : (∀ i ∈ t, 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x
⊢ (∀ (i : ↥t), 0 ≤ (w ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ t)) i) ∧
    Eq.{u_1 + 1} (α := R) (∑ i : ↥t, (w ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ t)) i) 1 ∧
      (∀ (i : ↥t), (z ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ t)) i ∈ s) ∧
        ∑ i : ↥t, (w ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ t)) i • (z ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ t)) i = x

Tactic:
simpa [← sum_attach t, centerMass_eq_of_sum_1 _ _ h.2.1] using h

Premises used: Finset.sum_attach, And.right, And.left, Finset.centerMass_eq_of_sum_1
-- 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 : Set E
x : E
ι : Type
w_1 : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) x

Tactic:
mem_convexHull_of_exists_fintype w z hw₀ hw₁ hz hx

Premises used: mem_convexHull_of_exists_fintype
-- 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 : Set E
x : E
ι : Type
w_1 : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) x

Tactic:
exact mem_convexHull_of_exists_fintype w z hw₀ hw₁ hz hx

Premises used: mem_convexHull_of_exists_fintype
-- 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
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E)
    ({x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x} :
      Set E)

Tactic:
Set.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
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Finset E
refine_1 :
  (↑s : Set E) ⊆
    {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x}
refine_2 :
  Convex.{u_1, u_3} R (E := E)
    {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x}
refine_3 :
  Subset.{u_3} (α := Set E)
    {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x}
    ((convexHull R : (a : Set E) → Set E) (↑s : Set E))
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E)
    ({x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x} :
      Set E)

Tactic:
refine Set.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
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Finset E
x : E
hx : x ∈ (↑s : Set E)
⊢ x ∈ s

Tactic:
rw [Finset.mem_coe] at hx

Premises used: 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
s : Finset E
x : E
hx : x ∈ s
⊢ Membership.mem (γ := Set E)
    {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x} x

Tactic:
⟨_, ?_, ?_, Finset.centerMass_ite_eq _ _ _ hx⟩

Premises used: Set.Mem, setOf, Finset.centerMass_ite_eq, And.intro, Exists.intro
-- 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
x : E
hx : x ∈ s
refine_1 : ∀ y ∈ s, LE.le.{u_1} (α := R) 0 (if x = y then 1 else 0)
refine_1₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, if x = y then 1 else 0) 1
⊢ Membership.mem (γ := Set E)
    {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x} x

Tactic:
refine ⟨_, ?_, ?_, Finset.centerMass_ite_eq _ _ _ hx⟩
-- 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
x : E
hx : x ∈ s
y : E
h : y ∈ s
pos : x = y → LE.le.{u_1} (α := R) 0 1
neg : ¬x = y → LE.le.{u_1} (α := R) 0 0
⊢ LE.le.{u_1} (α := R) 0 (if x = y then 1 else 0)

Tactic:
split_ifs
-- 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
x : E
hx : x ∈ s
y : E
h : y ∈ s
h_1 : x = y
⊢ LE.le.{u_1} (α := R) 0 1

Tactic:
zero_le_one

Premises used: zero_le_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
s : Finset E
x : E
hx : x ∈ s
y : E
h : y ∈ s
h_1 : ¬x = y
⊢ LE.le.{u_1} (α := R) 0 0

Tactic:
le_refl 0

Premises used: le_refl, 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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Finset E
x : E
hx : x ∈ s
y : E
h : y ∈ s
h_1 : x = y
⊢ LE.le.{u_1} (α := R) 0 1

Tactic:
exacts [zero_le_one, le_refl 0]

Premises used: le_refl, zero_le_one, 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
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : Finset E
x : E
hx : x ∈ s
refine_1 : Eq.{u_1 + 1} (α := R) (if x ∈ s then 1 else 0) 1
refine_1₁ refine_1₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, if x = y then 1 else 0) 1

Tactic:
rw [Finset.sum_ite_eq, if_pos hx]

Premises used: if_pos, Finset.sum_ite_eq