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
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
⊢ 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
have 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
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
-- 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
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
⊢ 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
have 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
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
-- 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
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
⊢ 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
have 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
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
-- 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
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)
have rw : Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) (t.centerMass (-w) z)
Tactic: rw [← centerMass_neg_left]
-- 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
ι : Type u_8
t : Finset ι
p : ι → E
w : ι → R
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
⊢ (affineCombination R t p : (a : ι → R) → E) w = t.centerMass w p
have rw : Eq.{u_3 + 1} (α := E) (∑ i ∈ t, w i • (p i -ᵥ 0)) (∑ i ∈ t, w i • p i)
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₂]
-- 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
ι : Type u_8
t : Finset ι
p : ι → E
w : ι → R
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
⊢ Eq.{u_3 + 1} (α := E) (∑ i ∈ t, w i • (p i -ᵥ 0)) (∑ i ∈ t, w i • p i)
have simp_rw : Eq.{u_3 + 1} (α := E) (∑ x ∈ t, w x • (p x - 0)) (∑ i ∈ t, w i • p i)
Tactic: simp_rw [vsub_eq_sub, sub_zero]
-- 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 : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ 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)
have rw : Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (Set.range v) : Set E) (s.centerMass w v)
Tactic: rw [affineCombination_eq_centerMass 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
s : Finset ι
v : ι → E
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (Set.range v) : Set E) (s.centerMass w v)
have hws : LT.lt.{u_1} (α := R) 0 (∑ i ∈ s, w i)
Tactic: apply s.centerMass_mem_convexHull 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
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)
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (Set.range v) : Set E) (s.centerMass w v)
have hz : ∀ i ∈ s, v i ∈ Set.range v
Tactic: apply s.centerMass_mem_convexHull 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
hs : s.Nonempty
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E) (centroid R s id)
have rw : Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E)
  (s.centerMass (centroidWeights R s) id)
Tactic: rw [s.centroid_eq_centerMass hs]
-- 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
hs : s.Nonempty
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E)
    (s.centerMass (centroidWeights R s) id)
have hw₀ : ∀ i ∈ s, 0 ≤ centroidWeights R s i
Tactic: apply s.centerMass_id_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
hs : s.Nonempty
hw₀ : ∀ i ∈ s, 0 ≤ 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)
have hws : LT.lt.{u_1} (α := R) 0 (∑ i ∈ s, centroidWeights R s i)
Tactic: apply s.centerMass_id_mem_convexHull
-- 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
hs : s.Nonempty
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ s, centroidWeights R s i)
have hs_card : Ne.{u_1 + 1} (α := R) (↑(#s) : R) 0
Tactic: have hs_card : (#s : R) ≠ 0 := by simp [Finset.nonempty_iff_ne_empty.mp hs]
-- 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: refine Subset.antisymm (convexHull_min ?_ ?_) ?_
-- 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: refine Subset.antisymm (convexHull_min ?_ ?_) ?_
-- 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: refine Subset.antisymm (convexHull_min ?_ ?_) ?_
-- 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
x : E
hx : x ∈ Set.range v
⊢ 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
have 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
Tactic: obtain ⟨i, hi⟩ := Set.mem_range.mp hx
-- 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
⊢ (s ∪ s').sum W = 1
have h : ∀ x ∈ s', x ∈ s'
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]
-- 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
h : ∀ x ∈ s', x ∈ s'
⊢ (s ∪ s').sum W = 1
have h₁ : ∀ x ∈ s, x ∈ s
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]
-- 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
h : ∀ x ∈ s', x ∈ s'
h₁ : ∀ x ∈ s, x ∈ s
⊢ (s ∪ s').sum W = 1
have rw : ∀ x ∈ s ∪ s', x ∉ s' → (if x ∈ s' then b * w' x else 0) = 0
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]
-- 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
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
⊢ (s ∪ s').sum W = 1
have rw₁ : ∀ x ∈ s ∪ s', x ∉ s → (if x ∈ s then a * w x else 0) = 0
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (hypothesis)
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
⊢ 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}
    (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 hW₁ : (s ∪ s').sum W = 1
Tactic: 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
-- 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
⊢ 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}
    (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 : ∀ i ∈ s ∪ s', 0 ≤ W i
Tactic: refine ⟨s ∪ s', W, ?_, 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
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 : ∀ i ∈ s ∪ s', 0 ≤ W i
⊢ 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}
    (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₁ : (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)
Tactic: refine ⟨s ∪ s', W, ?_, 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
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
i : ι
⊢ 0 ≤ W i
have pos : ∀ (hi : i ∈ s), 0 ≤ W i
Tactic: by_cases hi : i ∈ s
-- 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
i : ι
pos : ∀ (hi : i ∈ s), 0 ≤ W i
⊢ 0 ≤ W i
have neg : ∀ (hi : i ∉ s), 0 ≤ W i
Tactic: by_cases hi : i ∈ s
-- 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
i : ι
hi : i ∈ s
⊢ 0 ≤ W i
have pos : ∀ (hi' : i ∈ s'), 0 ≤ W i
Tactic: by_cases hi' : i ∈ s'
-- 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
i : ι
hi : i ∈ s
pos : ∀ (hi' : i ∈ s'), 0 ≤ W i
⊢ 0 ≤ W i
have neg : ∀ (hi' : i ∉ s'), 0 ≤ W i
Tactic: by_cases hi' : i ∈ s'
-- 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
i : ι
hi : i ∉ s
⊢ 0 ≤ W i
have pos : ∀ (hi' : i ∈ s'), 0 ≤ W i
Tactic: by_cases hi' : i ∈ s'
-- 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
i : ι
hi : i ∉ s
pos : ∀ (hi' : i ∈ s'), 0 ≤ W i
⊢ 0 ≤ W i
have neg : ∀ (hi' : i ∉ s'), 0 ≤ W i
Tactic: by_cases hi' : i ∈ s'