awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
hW₁ : (s ∪ s').sum W = 1
⊢ (affineCombination R (s ∪ s') v : (a : ι → R) → E) W =
    HSMul.hSMul (β := E) a ((affineCombination R s v : (a : ι → R) → E) w : E) +
      HSMul.hSMul (β := E) b ((affineCombination R s' v : (a : ι → R) → E) w' : E)
have refine_2 : HAdd.hAdd (α := E) (∑ x ∈ s ∪ s', (if x ∈ s then a * w x else 0) • v x)
    (∑ x ∈ s ∪ s', (if x ∈ s' then b * w' x else 0) • v x) =
  HSMul.hSMul (β := E) a (∑ i ∈ s, w i • v i) + HSMul.hSMul (β := E) b (∑ i ∈ s', w' i • v i)
Tactic: simp_rw [W, affineCombination_eq_linear_combination (s ∪ s') v _ hW₁,
        affineCombination_eq_linear_combination s v w hw₁,
        affineCombination_eq_linear_combination s' v w' hw₁', add_smul, sum_add_distrib]
-- 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
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
hW₁ : (s ∪ s').sum W = 1
⊢ HAdd.hAdd (α := E) (∑ x ∈ s ∪ s', (if x ∈ s then a * w x else 0) • v x)
      (∑ x ∈ s ∪ s', (if x ∈ s' then b * w' x else 0) • v x) =
    HSMul.hSMul (β := E) a (∑ i ∈ s, w i • v i) + HSMul.hSMul (β := E) b (∑ i ∈ s', w' i • v i)
have refine_2 : HAdd.hAdd (α := E) (∑ x ∈ s, (if x ∈ s then a * w x else 0) • v x) (∑ x ∈ s', (if x ∈ s' then b * w' x else 0) • v x) =
  HSMul.hSMul (β := E) a (∑ i ∈ s, w i • v i) + HSMul.hSMul (β := E) b (∑ i ∈ s', w' i • v i)
Tactic: rw [← sum_subset subset_union_left, ← sum_subset subset_union_right]
-- 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
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
hW₁ : (s ∪ s').sum W = 1
refine_2 :
  HAdd.hAdd (α := E) (∑ x ∈ s, (if x ∈ s then a * w x else 0) • v x)
      (∑ x ∈ s', (if x ∈ s' then b * w' x else 0) • v x) =
    HSMul.hSMul (β := E) a (∑ i ∈ s, w i • v i) + HSMul.hSMul (β := E) b (∑ i ∈ s', w' i • v i)
⊢ HAdd.hAdd (α := E) (∑ x ∈ s ∪ s', (if x ∈ s then a * w x else 0) • v x)
      (∑ x ∈ s ∪ s', (if x ∈ s' then b * w' x else 0) • v x) =
    HSMul.hSMul (β := E) a (∑ i ∈ s, w i • v i) + HSMul.hSMul (β := E) b (∑ i ∈ s', w' i • v i)
have refine_2₁ : ∀ x ∈ s ∪ s', x ∉ s' → (if x ∈ s' then b * w' x else 0) • v x = 0
Tactic: rw [← sum_subset subset_union_left, ← sum_subset subset_union_right]
-- 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
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
hW₁ : (s ∪ s').sum W = 1
refine_2 :
  HAdd.hAdd (α := E) (∑ x ∈ s, (if x ∈ s then a * w x else 0) • v x)
      (∑ x ∈ s', (if x ∈ s' then b * w' x else 0) • v x) =
    HSMul.hSMul (β := E) a (∑ i ∈ s, w i • v i) + HSMul.hSMul (β := E) b (∑ i ∈ s', w' i • v i)
refine_2₁ : ∀ x ∈ s ∪ s', x ∉ s' → (if x ∈ s' then b * w' x else 0) • v x = 0
⊢ HAdd.hAdd (α := E) (∑ x ∈ s ∪ s', (if x ∈ s then a * w x else 0) • v x)
      (∑ x ∈ s ∪ s', (if x ∈ s' then b * w' x else 0) • v x) =
    HSMul.hSMul (β := E) a (∑ i ∈ s, w i • v i) + HSMul.hSMul (β := E) b (∑ i ∈ s', w' i • v i)
have refine_2₂ : ∀ x ∈ s ∪ s', x ∉ s → (if x ∈ s then a * w x else 0) • v x = 0
Tactic: rw [← sum_subset subset_union_left, ← sum_subset subset_union_right]
-- 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
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)
have 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}
Tactic: classical
  refine Subset.antisymm (convexHull_min ?_ ?_) ?_
  · intro x hx
    obtain ⟨i, hi⟩ := Set.mem_range.mp hx
    exact ⟨{i}, Function.const ι (1 : R), by simp, by simp, by simp [hi]⟩
  · rintro x ⟨s, w, hw₀, hw₁, rfl⟩ y ⟨s', w', hw₀', hw₁', rfl⟩ a b ha hb hab
    let W : ι → R := fun i => (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
    have hW₁ : (s ∪ s').sum W = 1 := by
      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] <;> intros <;> simp_all
    refine ⟨s ∪ s', W, ?_, hW₁, ?_⟩
    · rintro i -
      by_cases hi : i ∈ s <;> by_cases hi' : i ∈ s' <;>
        simp [W, hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]
    · simp_rw [W, affineCombination_eq_linear_combination (s ∪ s') v _ hW₁,
        affineCombination_eq_linear_combination s v w hw₁,
        affineCombination_eq_linear_combination s' v w' hw₁', add_smul, sum_add_distrib]
      rw [← sum_subset subset_union_left, ← sum_subset subset_union_right]
      · simp only [ite_smul, sum_ite_of_true fun _ hi => hi, mul_smul, ← smul_sum]
      · intro i _ hi'
        simp [hi']
      · intro i _ hi'
        simp [hi']
  · rintro x ⟨s, w, hw₀, hw₁, rfl⟩
    exact affineCombination_mem_convexHull hw₀ hw₁
-- 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
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}
⊢ 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)
have 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}
Tactic: classical
  refine Subset.antisymm (convexHull_min ?_ ?_) ?_
  · intro x hx
    obtain ⟨i, hi⟩ := Set.mem_range.mp hx
    exact ⟨{i}, Function.const ι (1 : R), by simp, by simp, by simp [hi]⟩
  · rintro x ⟨s, w, hw₀, hw₁, rfl⟩ y ⟨s', w', hw₀', hw₁', rfl⟩ a b ha hb hab
    let W : ι → R := fun i => (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
    have hW₁ : (s ∪ s').sum W = 1 := by
      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] <;> intros <;> simp_all
    refine ⟨s ∪ s', W, ?_, hW₁, ?_⟩
    · rintro i -
      by_cases hi : i ∈ s <;> by_cases hi' : i ∈ s' <;>
        simp [W, hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]
    · simp_rw [W, affineCombination_eq_linear_combination (s ∪ s') v _ hW₁,
        affineCombination_eq_linear_combination s v w hw₁,
        affineCombination_eq_linear_combination s' v w' hw₁', add_smul, sum_add_distrib]
      rw [← sum_subset subset_union_left, ← sum_subset subset_union_right]
      · simp only [ite_smul, sum_ite_of_true fun _ hi => hi, mul_smul, ← smul_sum]
      · intro i _ hi'
        simp [hi']
      · intro i _ hi'
        simp [hi']
  · rintro x ⟨s, w, hw₀, hw₁, rfl⟩
    exact affineCombination_mem_convexHull hw₀ hw₁
-- 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
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}
⊢ 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)
have 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))
Tactic: classical
  refine Subset.antisymm (convexHull_min ?_ ?_) ?_
  · intro x hx
    obtain ⟨i, hi⟩ := Set.mem_range.mp hx
    exact ⟨{i}, Function.const ι (1 : R), by simp, by simp, by simp [hi]⟩
  · rintro x ⟨s, w, hw₀, hw₁, rfl⟩ y ⟨s', w', hw₀', hw₁', rfl⟩ a b ha hb hab
    let W : ι → R := fun i => (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
    have hW₁ : (s ∪ s').sum W = 1 := by
      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] <;> intros <;> simp_all
    refine ⟨s ∪ s', W, ?_, hW₁, ?_⟩
    · rintro i -
      by_cases hi : i ∈ s <;> by_cases hi' : i ∈ s' <;>
        simp [W, hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]
    · simp_rw [W, affineCombination_eq_linear_combination (s ∪ s') v _ hW₁,
        affineCombination_eq_linear_combination s v w hw₁,
        affineCombination_eq_linear_combination s' v w' hw₁', add_smul, sum_add_distrib]
      rw [← sum_subset subset_union_left, ← sum_subset subset_union_right]
      · simp only [ite_smul, sum_ite_of_true fun _ hi => hi, mul_smul, ← smul_sum]
      · intro i _ hi'
        simp [hi']
      · intro i _ hi'
        simp [hi']
  · rintro x ⟨s, w, hw₀, hw₁, rfl⟩
    exact affineCombination_mem_convexHull hw₀ 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
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) s : 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} :
      Set E)
have refine_1 : s ⊆
  {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}
Tactic: refine 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 : Set E
refine_1 :
  s ⊆
    {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}
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) s : 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} :
      Set E)
have refine_2 : Convex.{u_1, u_3} R (E := 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}
Tactic: refine 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 : Set E
refine_1 :
  s ⊆
    {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}
refine_2 :
  Convex.{u_1, u_3} R (E := 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}
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) s : 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} :
      Set E)
have refine_3 : Subset.{u_3} (α := 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}
  ((convexHull R : (a : Set E) → Set E) s)
Tactic: refine 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 : Set E
x : E
hx : x ∈ 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}
    x
have right : (centerMass.{u_1, u_3, 0} (R := R) {PUnit.unit} (fun (x : PUnit.{1}) ↦ 1) fun (x_1 : PUnit.{1}) ↦ x) = x
Tactic: use PUnit, {PUnit.unit}, fun _ => 1, fun _ => x, fun _ _ => zero_le_one, sum_singleton _ _,
      fun _ _ => 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 : 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}
    (a • sx.centerMass wx zx + b • sy.centerMass wy zy)
have refine_2 : 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: 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 : 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))
have 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)
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 : 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)
⊢ 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))
have 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
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 : 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
⊢ 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))
have refine_2₂ : ∀ i ∈ sx.disjSum sy, Sum.elim zx zy i ∈ s
Tactic: refine ⟨_, _, _, _, ?_, ?_, ?_, rfl⟩
-- 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
⊢ LE.le.{u_1} (α := R) 0 (Sum.elim (fun (i : ι) ↦ a * wx i) (fun (j : ι') ↦ b * wy j) i)
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
⊢ LE.le.{u_1} (α := R) 0 (Sum.elim (fun (i : ι) ↦ a * wx i) (fun (j : ι') ↦ b * wy j) i)
have 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))
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),
    LE.le.{u_1} (α := R) 0 (Sum.elim (fun (i : ι) ↦ a * wx i) (fun (j : ι') ↦ b * wy j) (Sum.inl j))
⊢ LE.le.{u_1} (α := R) 0 (Sum.elim (fun (i : ι) ↦ a * wx i) (fun (j : ι') ↦ b * wy j) i)
have 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))
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
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))
have refine_2 : 0 ≤ a * wx j
Tactic: simp only [Sum.elim_inl, Sum.elim_inr]
-- 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
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))
have refine_2 : 0 ≤ b * wy j
Tactic: simp only [Sum.elim_inl, Sum.elim_inr]