awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (hypothesis)
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
⊢ Sum.elim zx zy i ∈ s
have hi₁ : (∃ a ∈ sx, Sum.inl a = i) ∨ ∃ b ∈ sy, Sum.inr b = i
Tactic: rw [Finset.mem_disjSum] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Sum.elim zx zy i ∈ s
have refine_2 : ∀ (j : ι) (hj : j ∈ sx), Sum.elim zx zy (Sum.inl j) ∈ s
Tactic: rcases hi with (⟨j, hj, rfl⟩ | ⟨j, hj, rfl⟩)
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Sum.elim zx zy i ∈ s
have refine_2₁ : ∀ (j : ι') (hj : j ∈ sy), Sum.elim zx zy (Sum.inr j) ∈ s
Tactic: rcases hi with (⟨j, hj, rfl⟩ | ⟨j, hj, rfl⟩)
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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) x
have rw : Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) (centerMass Finset.univ w z)
Tactic: rw [← hx, ← centerMass_eq_of_sum_1 _ _ hw₁]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ 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
have 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
Tactic: simp only [convexHull_eq, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
have 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
Tactic: refine ⟨t, inferInstance, w ∘ (↑), z ∘ (↑), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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)
have 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}
Tactic: refine Set.Subset.antisymm (convexHull_min ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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}
⊢ 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)
have 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}
Tactic: refine Set.Subset.antisymm (convexHull_min ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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}
⊢ 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)
have 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))
Tactic: refine Set.Subset.antisymm (convexHull_min ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (hypothesis)
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)
⊢ 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
have hx₁ : x ∈ s
Tactic: rw [Finset.mem_coe] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
have refine_1 : ∀ y ∈ s, LE.le.{u_1} (α := R) 0 (if x = y then 1 else 0)
Tactic: refine ⟨_, ?_, ?_, Finset.centerMass_ite_eq _ _ _ hx⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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)
⊢ 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
have refine_1₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, if x = y then 1 else 0) 1
Tactic: refine ⟨_, ?_, ?_, Finset.centerMass_ite_eq _ _ _ hx⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ LE.le.{u_1} (α := R) 0 (if x = y then 1 else 0)
have pos : x = y → LE.le.{u_1} (α := R) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ LE.le.{u_1} (α := R) 0 (if x = y then 1 else 0)
have neg : ¬x = y → LE.le.{u_1} (α := R) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, if x = y then 1 else 0) 1
have refine_1 : Eq.{u_1 + 1} (α := R) (if x ∈ s then 1 else 0) 1
Tactic: rw [Finset.sum_ite_eq, if_pos hx]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, if x = y then 1 else 0) 1
have refine_1₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [Finset.sum_ite_eq, if_pos hx]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wx y) 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wy y) 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 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}
    (a • s.centerMass wx id + b • s.centerMass wy id)
have refine_2 : 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}
  (centerMass.{u_1, u_3, u_3} (R := R) s (fun (i : E) ↦ a * wx i + b * wy i) id)
Tactic: rw [Finset.centerMass_segment _ _ _ _ hwx₁ hwy₁ _ _ hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wx y) 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wy y) 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 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}
    (centerMass.{u_1, u_3, u_3} (R := R) s (fun (i : E) ↦ a * wx i + b * wy i) id)
have refine_2 : ∀ y ∈ s, 0 ≤ a * wx y + b * wy y
Tactic: refine ⟨_, ?_, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wx y) 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wy y) 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_2 : ∀ y ∈ s, 0 ≤ a * wx y + b * wy y
⊢ 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}
    (centerMass.{u_1, u_3, u_3} (R := R) s (fun (i : E) ↦ a * wx i + b * wy i) id)
have refine_2₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, (a * wx y + b * wy y)) 1
Tactic: refine ⟨_, ?_, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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)
have 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}
Tactic: classical
  refine Set.Subset.antisymm (convexHull_min ?_ ?_) ?_
  · intro x hx
    rw [Finset.mem_coe] at hx
    refine ⟨_, ?_, ?_, Finset.centerMass_ite_eq _ _ _ hx⟩
    · intros
      split_ifs
      exacts [zero_le_one, le_refl 0]
    · rw [Finset.sum_ite_eq, if_pos hx]
  · rintro x ⟨wx, hwx₀, hwx₁, rfl⟩ y ⟨wy, hwy₀, hwy₁, rfl⟩ a b ha hb hab
    rw [Finset.centerMass_segment _ _ _ _ hwx₁ hwy₁ _ _ hab]
    refine ⟨_, ?_, ?_, rfl⟩
    · rintro i hi
      apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀]
    · simp only [Finset.sum_add_distrib, ← mul_sum, mul_one, *]
  · rintro _ ⟨w, hw₀, hw₁, rfl⟩
    exact
      s.centerMass_mem_convexHull (fun x hx => hw₀ _ hx) (hw₁.symm ▸ zero_lt_one) fun x hx => hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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}
⊢ 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)
have 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}
Tactic: classical
  refine Set.Subset.antisymm (convexHull_min ?_ ?_) ?_
  · intro x hx
    rw [Finset.mem_coe] at hx
    refine ⟨_, ?_, ?_, Finset.centerMass_ite_eq _ _ _ hx⟩
    · intros
      split_ifs
      exacts [zero_le_one, le_refl 0]
    · rw [Finset.sum_ite_eq, if_pos hx]
  · rintro x ⟨wx, hwx₀, hwx₁, rfl⟩ y ⟨wy, hwy₀, hwy₁, rfl⟩ a b ha hb hab
    rw [Finset.centerMass_segment _ _ _ _ hwx₁ hwy₁ _ _ hab]
    refine ⟨_, ?_, ?_, rfl⟩
    · rintro i hi
      apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀]
    · simp only [Finset.sum_add_distrib, ← mul_sum, mul_one, *]
  · rintro _ ⟨w, hw₀, hw₁, rfl⟩
    exact
      s.centerMass_mem_convexHull (fun x hx => hw₀ _ hx) (hw₁.symm ▸ zero_lt_one) fun x hx => hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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}
⊢ 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)
have 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))
Tactic: classical
  refine Set.Subset.antisymm (convexHull_min ?_ ?_) ?_
  · intro x hx
    rw [Finset.mem_coe] at hx
    refine ⟨_, ?_, ?_, Finset.centerMass_ite_eq _ _ _ hx⟩
    · intros
      split_ifs
      exacts [zero_le_one, le_refl 0]
    · rw [Finset.sum_ite_eq, if_pos hx]
  · rintro x ⟨wx, hwx₀, hwx₁, rfl⟩ y ⟨wy, hwy₀, hwy₁, rfl⟩ a b ha hb hab
    rw [Finset.centerMass_segment _ _ _ _ hwx₁ hwy₁ _ _ hab]
    refine ⟨_, ?_, ?_, rfl⟩
    · rintro i hi
      apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀]
    · simp only [Finset.sum_add_distrib, ← mul_sum, mul_one, *]
  · rintro _ ⟨w, hw₀, hw₁, rfl⟩
    exact
      s.centerMass_mem_convexHull (fun x hx => hw₀ _ hx) (hw₁.symm ▸ zero_lt_one) fun x hx => hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E) x ↔
    ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x
have rw : 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 ↔
  ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x
Tactic: rw [Finset.convexHull_eq, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
rw :
  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 ↔
    ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E) x ↔
    ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x
have rw₁ : (∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x) ↔
  ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x
Tactic: rw [Finset.convexHull_eq, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E) x ↔
    ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ ∑ y ∈ s, w y • y = x
have rw : (∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x) ↔
  ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ ∑ y ∈ s, w y • y = x
Tactic: rw [mem_convexHull]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ (∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x) ↔
    ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ ∑ y ∈ s, w y • y = x
have refine : ∀ (w : E → R) (hw : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1), s.centerMass w id = x ↔ ∑ y ∈ s, w y • y = x
Tactic: refine exists_congr fun w ↦ and_congr_right' <| and_congr_right fun hw ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
w : E → R
hw : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1
⊢ s.centerMass w id = x ↔ ∑ y ∈ s, w y • y = x
have simp_rw : ∑ i ∈ s, w i • id i = x ↔ ∑ y ∈ s, w y • y = x
Tactic: simp_rw [centerMass_eq_of_sum_1 _ _ hw, id_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)
have refine_1 : Subset (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
  (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)
Tactic: refine Subset.antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
refine_1 :
  Subset (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)
have refine_2 : Subset.{u_3} (α := Set E)
  (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E))
  ((convexHull R : (a : Set E) → Set E) s)
Tactic: refine Subset.antisymm ?_ ?_