awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
x : ι
h : x ∈ s'
⊢ x ∈ s'

Tactic:
simp_all
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
x : ι
h : x ∈ s
⊢ x ∈ s

Tactic:
simp_all
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
x : ι
h : x ∈ s ∪ s'
h_1 : x ∉ s'
⊢ (if x ∈ s' then b * w' x else 0) = 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
x : ι
h : x ∈ s ∪ s'
h_1 : x ∉ s
⊢ (if x ∈ s then a * w x else 0) = 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
⊢ (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
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
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))

Tactic:
⟨s ∪ s', W, ?_, hW₁, ?_⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Union.union
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
refine_2 : ∀ i ∈ s ∪ s', 0 ≤ W i
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)
⊢ 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))

Tactic:
refine ⟨s ∪ s', W, ?_, 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
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
neg : ∀ (hi : i ∉ s), 0 ≤ W i
⊢ 0 ≤ W i

Tactic:
by_cases hi : i ∈ s
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
hi : i ∈ s
pos : ∀ (hi' : i ∈ s'), 0 ≤ W i
neg : ∀ (hi' : i ∉ s'), 0 ≤ W i
⊢ 0 ≤ W i

Tactic:
by_cases hi' : i ∈ s'
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
hi : i ∉ s
pos : ∀ (hi' : i ∈ s'), 0 ≤ W i
neg : ∀ (hi' : i ∉ s'), 0 ≤ W i
⊢ 0 ≤ W i

Tactic:
by_cases hi' : i ∈ s'
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
hi : i ∈ s
hi' : i ∈ s'
⊢ 0 ≤ W i

Tactic:
simp [W, hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]

Premises used: mul_nonneg, add_nonneg
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
hi : i ∈ s
hi' : i ∉ s'
⊢ 0 ≤ W i

Tactic:
simp [W, hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]

Premises used: mul_nonneg, add_nonneg
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
hi : i ∉ s
hi' : i ∈ s'
⊢ 0 ≤ W i

Tactic:
simp [W, hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]

Premises used: mul_nonneg, add_nonneg
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
hi : i ∉ s
hi' : i ∉ s'
⊢ 0 ≤ W i

Tactic:
simp [W, hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]

Premises used: mul_nonneg, add_nonneg
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
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)
⊢ (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:
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]

Premises used: Finset.sum_add_distrib, Finset.affineCombination_eq_linear_combination, add_smul, Union.union
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
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
refine_2₂ : ∀ x ∈ s ∪ s', x ∉ s → (if x ∈ s then a * 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)

Tactic:
rw [← sum_subset subset_union_left, ← sum_subset subset_union_right]

Premises used: Finset.subset_union_left, Finset.sum_subset, Finset.subset_union_right
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
⊢ 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:
simp only [ite_smul, sum_ite_of_true fun _ hi => hi, mul_smul, ← smul_sum]

Premises used: Finset.smul_sum, Finset.sum_ite_of_true, ite_smul, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
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 : ι
refine_2 : i ∈ s ∪ s' → i ∉ s' → (if i ∈ s' then b * w' i else 0) • v i = 0
⊢ i ∈ s ∪ s' → i ∉ s' → (if i ∈ s' then b * w' i else 0) • v i = 0

Tactic:
_
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
h : i ∈ s ∪ s'
hi' : i ∉ s'
⊢ (if i ∈ s' then b * w' i else 0) • v i = 0

Tactic:
simp [hi']
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
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 : ι
refine_2 : i ∈ s ∪ s' → i ∉ s → (if i ∈ s then a * w i else 0) • v i = 0
⊢ i ∈ s ∪ s' → i ∉ s → (if i ∈ s then a * w i else 0) • v i = 0

Tactic:
_
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun (i : ι) ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
h : i ∈ s ∪ s'
hi' : i ∉ s
⊢ (if i ∈ s then a * w i else 0) • v i = 0

Tactic:
simp [hi']
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
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)

Tactic:
affineCombination_mem_convexHull hw₀ hw₁

Premises used: affineCombination_mem_convexHull
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
s : Finset ι
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)

Tactic:
exact affineCombination_mem_convexHull hw₀ hw₁

Premises used: affineCombination_mem_convexHull
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
v : ι → E
refine_1 :
  Set.range v ⊆
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v : (a : ι → R) → E) w = x}
refine_2 :
  Convex.{u_1, u_3} R (E := E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v : (a : ι → R) → E) w = x}
refine_3 :
  Subset.{u_3} (α := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v : (a : ι → R) → E) w = x}
    ((convexHull R : (a : Set E) → Set E) (Set.range v))
refine_2₁ :
  Convex.{u_1, u_3} R (E := E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v : (a : ι → R) → E) w = x}
refine_3₁ refine_3₂ :
  Subset.{u_3} (α := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v : (a : ι → R) → E) w = x}
    ((convexHull R : (a : Set E) → Set E) (Set.range v))
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) (Set.range v) : Set E)
    ({x : E |
        ∃ (s : Finset ι) (w : ι → R),
          (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v : (a : ι → R) → E) w = x} :
      Set E)

Tactic:
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₁

Premises used: Finset.sum_add_distrib, add_nonneg, Finset.subset_union_left, add_smul, Finset.sum_subset, Finset.smul_sum, Finset.sum_ite_of_true, ite_smul, Finset.subset_union_right, SemigroupAction.mul_smul, 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
⊢ 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)

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

Premises used: Set.Subset.antisymm, convexHull_min
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
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}
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)
⊢ 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)

Tactic:
refine 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 : Set E
x : E
hx : x ∈ s
right : (centerMass.{u_1, u_3, 0} (R := R) {PUnit.unit} (fun (x : PUnit.{1}) ↦ 1) fun (x_1 : PUnit.{1}) ↦ x) = x
⊢ 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

Tactic:
use PUnit, {PUnit.unit}, fun _ => 1, fun _ => x, fun _ _ => zero_le_one, sum_singleton _ _,
      fun _ _ => hx

Premises used: zero_le_one, Finset.sum_singleton, PUnit, PUnit.unit, 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 : Set E
x : E
hx : x ∈ s
⊢ (centerMass.{u_1, u_3, 0} (R := R) {PUnit.unit} (fun (x : PUnit.{1}) ↦ 1) fun (x_1 : PUnit.{1}) ↦ x) = x

Tactic:
simp only [Finset.centerMass, Finset.sum_singleton, inv_one, one_smul]

Premises used: inv_one, one_smul, Finset.sum_singleton, Finset.centerMass
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s : 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 :
  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))
⊢ 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)

Tactic:
rw [Finset.centerMass_segment' _ _ _ _ _ _ hwx₁ hwy₁ _ _ hab]

Premises used: Finset.centerMass_segment'