awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
x : E
hx : Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
hx' : Membership.mem (γ := AffineSubspace R E) (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E))) x
h :
  ∀ (s : Finset ι) (w : ι → R) (hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1)
    (hx :
      Membership.mem.{u_3, u_3} (α := E) (γ := Set E)
        {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)}
        ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E))
    (hx' :
      Membership.mem (α := E) (γ := AffineSubspace R E)
        (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E)))
        ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)),
    Membership.mem.{u_3, u_3} (α := E) (γ := Set E)
      {x : E |
        ∃ (s : Finset ι) (w : ι → R),
          (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
      ((affineCombination R s (⇑b : (a : ι) → E) : (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 (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
    x

Tactic:
obtain ⟨s, w, hw₁, rfl⟩ := (mem_affineSpan_iff_eq_affineCombination R E).mp hx'

Premises used: mem_affineSpan_iff_eq_affineCombination, Iff.mp, 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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hx :
  Membership.mem.{u_3, u_3} (α := E) (γ := Set E)
    {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)}
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
hx' :
  Membership.mem (α := E) (γ := AffineSubspace R E)
    (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E)))
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
⊢ Membership.mem.{u_3, u_3} (α := E) (γ := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)

Tactic:
⟨s, w, ?_, hw₁, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hx :
  Membership.mem.{u_3, u_3} (α := E) (γ := Set E)
    {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)}
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
hx' :
  Membership.mem (α := E) (γ := AffineSubspace R E)
    (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E)))
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
h : ∀ i ∈ s, 0 ≤ w i
⊢ Membership.mem.{u_3, u_3} (α := E) (γ := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)

Tactic:
refine ⟨s, w, ?_, hw₁, 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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hx :
  Membership.mem.{u_3, u_3} (α := E) (γ := Set E)
    {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)}
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
hx' :
  Membership.mem (α := E) (γ := AffineSubspace R E)
    (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E)))
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
i : ι
hi : i ∈ s
⊢ LE.le.{u_1} (α := R) (0 : R)
    ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)

Tactic:
specialize hx i
-- 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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hx' :
  Membership.mem (α := E) (γ := AffineSubspace R E)
    (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E)))
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
i : ι
hi : i ∈ s
hx :
  LE.le.{u_1} (α := R) (0 : R)
    ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)
⊢ 0 ≤ w i

Tactic:
rw [b.coord_apply_combination_of_mem hi hw₁] at hx

Premises used: AffineBasis.coord_apply_combination_of_mem
-- 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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hx' :
  Membership.mem (α := E) (γ := AffineSubspace R E)
    (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E)))
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
i : ι
hi : i ∈ s
hx : 0 ≤ w i
⊢ 0 ≤ w i

Tactic:
hx
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hx' :
  Membership.mem (α := E) (γ := AffineSubspace R E)
    (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E)))
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
i : ι
hi : i ∈ s
hx : 0 ≤ w i
⊢ 0 ≤ w i

Tactic:
exact hx
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s t₁ t₂ : Finset E
hs : AffineIndependent R (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) ((↑t₁ : Set E) ∩ (↑t₂ : Set E)) : Set E)
    ((convexHull R : (a : Set E) → Set E) (↑t₁ : Set E) ∩ (convexHull R : (a : Set E) → Set E) (↑t₂ : Set E) : Set E)

Tactic:
(Set.subset_inter (convexHull_mono inf_le_left) <|
    convexHull_mono inf_le_right).antisymm ?_

Premises used: inf_le_right, convexHull_mono, Set.subset_inter, HasSubset.Subset.antisymm, inf_le_left
-- 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 t₁ t₂ : Finset E
hs : AffineIndependent R (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
refine :
  Subset (α := Set E)
    ((convexHull R : (a : Set E) → Set E) (↑t₁ : Set E) ∩ (convexHull R : (a : Set E) → Set E) (↑t₂ : Set E) : Set E)
    ((convexHull R : (a : Set E) → Set E) ((↑t₁ : Set E) ⊓ (↑t₂ : Set E)) : Set E)
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) ((↑t₁ : Set E) ∩ (↑t₂ : Set E)) : Set E)
    ((convexHull R : (a : Set E) → Set E) (↑t₁ : Set E) ∩ (convexHull R : (a : Set E) → Set E) (↑t₂ : Set E) : Set E)

Tactic:
refine (Set.subset_inter (convexHull_mono inf_le_left) <|
    convexHull_mono inf_le_right).antisymm ?_

Premises used: inf_le_right, convexHull_mono, Set.subset_inter, HasSubset.Subset.antisymm, inf_le_left
-- 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 t₁ t₂ : Finset E
hs : AffineIndependent R (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
simp_rw :
  ∀ (x : E),
    ((∃ (w : E → R), (∀ y ∈ t₁, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w y) 1 ∧ ∑ y ∈ t₁, w y • y = x) ∧
        ∃ (w : E → R), (∀ y ∈ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w y) 1 ∧ ∑ y ∈ t₂, w y • y = x) →
      ∃ (w : E → R),
        (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
⊢ Subset (α := Set E)
    ((convexHull R : (a : Set E) → Set E) (↑t₁ : Set E) ∩ (convexHull R : (a : Set E) → Set E) (↑t₂ : Set E) : Set E)
    ((convexHull R : (a : Set E) → Set E) ((↑t₁ : Set E) ⊓ (↑t₂ : Set E)) : Set E)

Tactic:
simp_rw [Set.subset_def, mem_inter_iff, Set.inf_eq_inter, ← coe_inter, mem_convexHull']

Premises used: Set.subset_def, Finset.mem_convexHull', Set.mem_inter_iff, Set.inf_eq_inter, Finset.coe_inter
-- 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 t₁ t₂ : Finset E
hs : AffineIndependent R (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0

Tactic:
simp [w, Finset.inter_eq_right.2, *]

Premises used: Iff.mpr, Finset.inter_eq_right
-- 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 t₁ t₂ : Finset E
hs : AffineIndependent R (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0

Tactic:
have h₁w : ∑ i ∈ s, w i = 0 := by simp [w, Finset.inter_eq_right.2, *]
-- 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 t₁ t₂ : Finset E
hs : AffineIndependent R (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
⊢ Eq (α := E) (∑ x ∈ s, w x • x) 0

Tactic:
simp only [w, sub_smul, zero_smul, ite_smul, Finset.sum_sub_distrib, ← Finset.sum_filter, h₃w₁,
      Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht₁, Finset.inter_eq_right.2 ht₂, h₃w₂,
      sub_self]

Premises used: Iff.mpr, sub_self, sub_smul, zero_smul, Finset.sum_sub_distrib, Finset.inter_eq_right, ite_smul, Finset.sum_filter, Finset.filter_mem_eq_inter
-- 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 t₁ t₂ : Finset E
hs : AffineIndependent R (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
⊢ ∀ x ∈ s, w x = 0

Tactic:
replace hs := hs.eq_zero_of_sum_eq_zero_subtype h₁w <| by
    simp only [w, sub_smul, zero_smul, ite_smul, Finset.sum_sub_distrib, ← Finset.sum_filter, h₃w₁,
      Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht₁, Finset.inter_eq_right.2 ht₂, h₃w₂,
      sub_self]
-- 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 t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x_1 : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x_1
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x_1
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
x : E
hx₁ : x ∈ t₁
hx₂ : x ∉ t₂
⊢ w₁ x = 0

Tactic:
simpa [w, hx₁, hx₂] using hs _ (ht₁ hx₁)
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
⊢ ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0

Tactic:
have ht (x) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂) : w₁ x = 0 := by
    simpa [w, hx₁, hx₂] using hs _ (ht₁ hx₁)
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
⊢ ∃ (w : E → R), (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x

Tactic:
⟨w₁, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
refine_1 : ∀ y ∈ t₁ ∩ t₂, 0 ≤ w₁ y
refine_2 : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w₁ y) 1
refine_3 : ∑ y ∈ t₁ ∩ t₂, w₁ y • y = x
⊢ ∃ (w : E → R), (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x

Tactic:
refine ⟨w₁, ?_, ?_, ?_⟩
-- 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 t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
refine_1 : ∀ y ∈ t₁, y ∈ t₂ → 0 ≤ w₁ y
⊢ ∀ y ∈ t₁ ∩ t₂, 0 ≤ w₁ y

Tactic:
simp only [and_imp, Finset.mem_inter]

Premises used: and_imp, Finset.mem_inter
-- 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 t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
⊢ ∀ y ∈ t₁, y ∈ t₂ → 0 ≤ w₁ y

Tactic:
fun y hy₁ _ ↦ h₁w₁ y hy₁
-- 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 t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
⊢ ∀ y ∈ t₁, y ∈ t₂ → 0 ≤ w₁ y

Tactic:
exact fun y hy₁ _ ↦ h₁w₁ y hy₁
-- 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 t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
refine_2 : ∀ x ∈ t₁, x ∉ t₁ ∩ t₂ → w₁ x = 0
⊢ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w₁ y) 1

Tactic:
rwa [sum_subset inter_subset_left]

Premises used: Finset.sum_subset, Finset.inter_subset_left
-- 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 t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x_1 : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x_1
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x_1
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
x : E
refine_2 : ∀ (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
⊢ x ∈ t₁ → x ∉ t₁ ∩ t₂ → w₁ x = 0

Tactic:
simp_intro hx₁ hx₂
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x_1 : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x_1
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x_1
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
x : E
hx₁ : x ∈ t₁
hx₂ : x ∉ t₂
⊢ w₁ x = 0

Tactic:
simp [ht x hx₁ hx₂]
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
refine_3 : ∀ x ∈ t₁, x ∉ t₁ ∩ t₂ → w₁ x • x = 0
⊢ ∑ y ∈ t₁ ∩ t₂, w₁ y • y = x

Tactic:
rwa [sum_subset inter_subset_left]

Premises used: Finset.sum_subset, Finset.inter_subset_left
-- 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 t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x_1 : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x_1
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x_1
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
x : E
refine_3 : ∀ (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0 ∨ x = 0
⊢ x ∈ t₁ → x ∉ t₁ ∩ t₂ → w₁ x • x = 0

Tactic:
simp_intro hx₁ hx₂
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x_1 : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x_1
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x_1
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
x : E
hx₁ : x ∈ t₁
hx₂ : x ∉ t₂
⊢ w₁ x = 0 ∨ x = 0

Tactic:
simp [ht x hx₁ hx₂]
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
t₁ t₂ : Finset E
inst_5 : DecidableEq E
hs : AffineIndependent R (P := E) (ι := ↥(t₁ ∪ t₂)) (Subtype.val (p := fun (x : E) ↦ x ∈ t₁ ∪ t₂))
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) ((↑t₁ : Set E) ∩ (↑t₂ : Set E)) : Set E)
    ((convexHull R : (a : Set E) → Set E) (↑t₁ : Set E) ∩ (convexHull R : (a : Set E) → Set E) (↑t₂ : Set E) : Set E)

Tactic:
hs.convexHull_inter subset_union_left subset_union_right

Premises used: Finset.subset_union_left, Finset.subset_union_right, AffineIndependent.convexHull_inter