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
s : Finset E
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wx y) 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wy y) 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_2 :
  Membership.mem (γ := Set E)
    {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x}
    (centerMass.{u_1, u_3, u_3} (R := R) s (fun (i : E) ↦ a * wx i + b * wy i) id)
⊢ Membership.mem (γ := Set E)
    {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x}
    (a • s.centerMass wx id + b • s.centerMass wy id)

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

Premises used: Finset.centerMass_segment
-- 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 : Finset E
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wx y) 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wy y) 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Membership.mem (γ := Set E)
    {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x}
    (centerMass.{u_1, u_3, u_3} (R := R) s (fun (i : E) ↦ a * wx i + b * wy i) id)

Tactic:
⟨_, ?_, ?_, 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
s : Finset E
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wx y) 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wy y) 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_2 : ∀ y ∈ s, 0 ≤ a * wx y + b * wy y
refine_2₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, (a * wx y + b * wy y)) 1
⊢ Membership.mem (γ := Set E)
    {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x}
    (centerMass.{u_1, u_3, u_3} (R := R) s (fun (i : E) ↦ a * wx i + b * wy i) id)

Tactic:
refine ⟨_, ?_, ?_, 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 : Finset E
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wx y) 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wy y) 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : E
hi : i ∈ s
⊢ 0 ≤ a * wx i + b * wy i

Tactic:
apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀]

Premises used: mul_nonneg, add_nonneg
-- 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 : Finset E
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wx y) 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, wy y) 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, (a * wx y + b * wy y)) 1

Tactic:
simp only [Finset.sum_add_distrib, ← mul_sum, mul_one, *]

Premises used: Finset.mul_sum, Finset.sum_add_distrib, mul_one
-- 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 : Finset E
w : E → R
hw₀ : ∀ y ∈ s, 0 ≤ w y
hw₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E) (s.centerMass w id)

Tactic:
s.centerMass_mem_convexHull (fun x hx => hw₀ _ hx) (hw₁.symm ▸ zero_lt_one) fun x hx => hx

Premises used: Set.Mem, Eq.rec, Finset.centerMass_mem_convexHull, zero_lt_one, Eq.symm
-- 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 : Finset E
w : E → R
hw₀ : ∀ y ∈ s, 0 ≤ w y
hw₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E) (s.centerMass w id)

Tactic:
exact
      s.centerMass_mem_convexHull (fun x hx => hw₀ _ hx) (hw₁.symm ▸ zero_lt_one) fun x hx => hx

Premises used: Eq.rec, Finset.centerMass_mem_convexHull, zero_lt_one, Eq.symm
-- 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 : Finset E
refine_1 :
  (↑s : Set E) ⊆
    {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x}
refine_2 :
  Convex.{u_1, u_3} R (E := E)
    {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x}
refine_3 :
  Subset.{u_3} (α := Set E)
    {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x}
    ((convexHull R : (a : Set E) → Set E) (↑s : Set E))
refine_2₁ :
  Convex.{u_1, u_3} R (E := E)
    {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x}
refine_3₁ refine_3₂ :
  Subset.{u_3} (α := Set E)
    {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x}
    ((convexHull R : (a : Set E) → Set E) (↑s : Set E))
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E)
    ({x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x} :
      Set E)

Tactic:
classical
  refine Set.Subset.antisymm (convexHull_min ?_ ?_) ?_
  · intro x hx
    rw [Finset.mem_coe] at hx
    refine ⟨_, ?_, ?_, Finset.centerMass_ite_eq _ _ _ hx⟩
    · intros
      split_ifs
      exacts [zero_le_one, le_refl 0]
    · rw [Finset.sum_ite_eq, if_pos hx]
  · rintro x ⟨wx, hwx₀, hwx₁, rfl⟩ y ⟨wy, hwy₀, hwy₁, rfl⟩ a b ha hb hab
    rw [Finset.centerMass_segment _ _ _ _ hwx₁ hwy₁ _ _ hab]
    refine ⟨_, ?_, ?_, rfl⟩
    · rintro i hi
      apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀]
    · simp only [Finset.sum_add_distrib, ← mul_sum, mul_one, *]
  · rintro _ ⟨w, hw₀, hw₁, rfl⟩
    exact
      s.centerMass_mem_convexHull (fun x hx => hw₀ _ hx) (hw₁.symm ▸ zero_lt_one) fun x hx => hx

Premises used: Set.Subset.antisymm, Finset.mul_sum, mul_nonneg, le_refl, Finset.sum_add_distrib, add_nonneg, zero_le_one, convexHull_min, mul_one, OfNat.ofNat, Finset.mem_coe, Finset.sum_ite_eq, 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 : Finset E
x : E
rw :
  Membership.mem (γ := Set E)
      {x : E | ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x} x ↔
    ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x
rw₁ rw₂ :
  (∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x) ↔
    ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E) x ↔
    ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x

Tactic:
rw [Finset.convexHull_eq, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, Finset.convexHull_eq
-- 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 : Finset E
x : E
rw :
  (∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x) ↔
    ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ ∑ y ∈ s, w y • y = x
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑s : Set E) : Set E) x ↔
    ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ ∑ y ∈ s, w y • y = x

Tactic:
rw [mem_convexHull]

Premises used: Finset.mem_convexHull
-- 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 : Finset E
x : E
⊢ (∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x) ↔
    ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ ∑ y ∈ s, w y • y = x

Tactic:
exists_congr fun w ↦ and_congr_right' <| and_congr_right fun hw ↦ ?_

Premises used: and_congr_right', and_congr_right, exists_congr
-- 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 : Finset E
x : E
refine : ∀ (w : E → R) (hw : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1), s.centerMass w id = x ↔ ∑ y ∈ s, w y • y = x
⊢ (∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ s.centerMass w id = x) ↔
    ∃ (w : E → R), (∀ y ∈ s, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1 ∧ ∑ y ∈ s, w y • y = x

Tactic:
refine exists_congr fun w ↦ and_congr_right' <| and_congr_right fun hw ↦ ?_

Premises used: and_congr_right', and_congr_right, exists_congr
-- 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 : Finset E
x : E
w : E → R
hw : Eq.{u_1 + 1} (α := R) (∑ y ∈ s, w y) 1
simp_rw : ∑ i ∈ s, w i • id i = x ↔ ∑ y ∈ s, w y • y = x
⊢ s.centerMass w id = x ↔ ∑ y ∈ s, w y • y = x

Tactic:
simp_rw [centerMass_eq_of_sum_1 _ _ hw, id_eq]

Premises used: Finset.centerMass_eq_of_sum_1, id_eq
-- 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
hs : s.Finite
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    ({x : E |
        ∃ (w : E → R),
          (∀ y ∈ s, 0 ≤ w y) ∧
            Eq.{u_1 + 1} (α := R) (∑ y ∈ hs.toFinset (s := s), w y) 1 ∧ hs.toFinset (s := s).centerMass w id = x} :
      Set E)

Tactic:
simpa only [Set.Finite.coe_toFinset, Set.Finite.mem_toFinset, exists_prop] using
    hs.toFinset.convexHull_eq

Premises used: Set.Finite.mem_toFinset, Set.Finite.coe_toFinset, exists_prop, Finset.convexHull_eq, Set.Finite.toFinset
-- 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)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)

Tactic:
Subset.antisymm ?_ ?_

Premises used: Set.Subset.antisymm
-- 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 :
  Subset (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)
refine_2 :
  Subset.{u_3} (α := Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E))
    ((convexHull R : (a : Set E) → Set E) s)
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)

Tactic:
refine Subset.antisymm ?_ ?_
-- 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 :
  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}
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E))
⊢ Subset (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)

Tactic:
rw [_root_.convexHull_eq]

Premises used: convexHull_eq
-- 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
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
refine_1 :
  ∃ (i : Finset E) (_ : (↑i : Set E) ⊆ s),
    Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑i : Set E) : Set E) (t.centerMass w z)
⊢ Membership.mem (γ := Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E)) (t.centerMass w z)

Tactic:
simp only [mem_iUnion]

Premises used: Set.mem_iUnion
-- 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
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
⊢ ∃ (i : Finset E) (_ : (↑i : Set E) ⊆ s),
    Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑i : Set E) : Set E) (t.centerMass w z)

Tactic:
⟨t.image z, ?_, ?_⟩

Premises used: Exists.intro, Finset.image
-- 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
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
refine_1 : (↑(Finset.image z t) : Set E) ⊆ s
refine_1₁ :
  Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑(Finset.image z t) : Set E) : Set E)
    (t.centerMass w z)
⊢ ∃ (i : Finset E) (_ : (↑i : Set E) ⊆ s),
    Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑i : Set E) : Set E) (t.centerMass w z)

Tactic:
refine ⟨t.image z, ?_, ?_⟩
-- 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
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
refine_1 : (↑t : Set ι) ⊆ z ⁻¹' s
⊢ (↑(Finset.image z t) : Set E) ⊆ s

Tactic:
rw [coe_image, Set.image_subset_iff]

Premises used: Finset.coe_image, Set.image_subset_iff
-- 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
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
⊢ (↑t : Set ι) ⊆ z ⁻¹' s

Tactic:
hz

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage
-- 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
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
⊢ (↑t : Set ι) ⊆ z ⁻¹' s

Tactic:
exact hz
-- 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
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
refine_1 : LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i)
refine_1₁ : ∀ i ∈ t, z i ∈ (↑(Finset.image z t) : Set E)
⊢ Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) (↑(Finset.image z t) : Set E) : Set E)
    (t.centerMass w z)

Tactic:
apply t.centerMass_mem_convexHull hw₀

Premises used: Finset.centerMass_mem_convexHull
-- 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
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i)

Tactic:
simp only [hw₁, zero_lt_one]

Premises used: zero_lt_one
-- 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
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
⊢ ∀ i ∈ t, z i ∈ (↑(Finset.image z t) : Set E)

Tactic:
fun i hi => Finset.mem_coe.2 (Finset.mem_image_of_mem _ hi)

Premises used: Iff.mpr, Finset.mem_image_of_mem, Finset.mem_coe
-- 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
t : Finset ι
w : ι → R
z : ι → E
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
hz : ∀ i ∈ t, z i ∈ s
⊢ ∀ i ∈ t, z i ∈ (↑(Finset.image z t) : Set E)

Tactic:
exact fun i hi => Finset.mem_coe.2 (Finset.mem_image_of_mem _ hi)

Premises used: Iff.mpr, Finset.mem_image_of_mem, Finset.mem_coe
-- 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
⊢ Subset.{u_3} (α := Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E))
    ((convexHull R : (a : Set E) → Set E) s)

Tactic:
iUnion_subset fun i => iUnion_subset convexHull_mono

Premises used: Set.iUnion_subset, convexHull_mono
-- 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
⊢ Subset.{u_3} (α := Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E))
    ((convexHull R : (a : Set E) → Set E) s)

Tactic:
exact iUnion_subset fun i => iUnion_subset convexHull_mono

Premises used: Set.iUnion_subset
-- 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 :
  Subset (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)
refine_2 refine_2₁ :
  Subset.{u_3} (α := Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E))
    ((convexHull R : (a : Set E) → Set E) s)
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    (⋃ (t : Finset E), ⋃ (_ : (↑t : Set E) ⊆ s), (convexHull R : (a : Set E) → Set E) (↑t : Set E) : Set E)

Tactic:
classical
  refine Subset.antisymm ?_ ?_
  · rw [_root_.convexHull_eq]
    rintro x ⟨ι, t, w, z, hw₀, hw₁, hz, rfl⟩
    simp only [mem_iUnion]
    refine ⟨t.image z, ?_, ?_⟩
    · rw [coe_image, Set.image_subset_iff]
      exact hz
    · apply t.centerMass_mem_convexHull hw₀
      · simp only [hw₁, zero_lt_one]
      · exact fun i hi => Finset.mem_coe.2 (Finset.mem_image_of_mem _ hi)
  · exact iUnion_subset fun i => iUnion_subset convexHull_mono

Premises used: Iff.mpr, Set.iUnion_subset, Set.mem_iUnion, Finset.coe_image, zero_lt_one, Set.image_subset_iff, convexHull_eq, Finset.mem_image_of_mem, Finset.mem_coe, 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
p₁ p₂ : E
rw : Eq (α := Submodule R E) (vectorSpan R (P := E) ((convexHull R : (a : Set E) → Set E) {p₁, p₂})) (R ∙ (p₂ -ᵥ p₁))
rw₁ :
  Eq (α := Submodule R E)
    (AffineSubspace.direction (P := E) (affineSpan R ((convexHull R : (a : Set E) → Set E) {p₁, p₂}))) (R ∙ (p₂ -ᵥ p₁))
rw₂ : Eq (α := Submodule R E) (AffineSubspace.direction (P := E) (affineSpan R {p₁, p₂})) (R ∙ (p₂ -ᵥ p₁))
rw₃ : Eq (α := Submodule R E) (vectorSpan R (P := E) {p₁, p₂}) (R ∙ (p₂ -ᵥ p₁))
rw₄ : Eq (α := Submodule R E) (R ∙ (p₂ -ᵥ p₁)) (R ∙ (p₂ -ᵥ p₁))
rw₅ rw₆ : Eq (α := Submodule R E) (R ∙ (p₂ - p₁)) (R ∙ (p₂ - p₁))
⊢ Eq (α := Submodule R E) (vectorSpan R (segment R p₁ p₂)) (R ∙ (p₂ -ᵥ p₁))

Tactic:
rw [← convexHull_pair, ← direction_affineSpan, affineSpan_convexHull,
      direction_affineSpan, vectorSpan_pair_rev, vsub_eq_sub]

Premises used: direction_affineSpan, affineSpan_convexHull, vectorSpan_pair_rev, convexHull_pair, vsub_eq_sub
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
F : Type u_4
inst : Field R
inst_1 : AddCommGroup E
inst_2 : AddCommGroup F
inst_3 : Module R E
inst_4 : Module R F
s : Set E
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
t : Set F
x : E
y : F
hx : Membership.mem (γ := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E) x
hy : Membership.mem (γ := Set F) ((convexHull R : (a : Set F) → Set F) t : Set F) y
rw :
  ∀
    (hx :
      ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E),
        (∀ (i : ι), 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x)
    (hy :
      ∃ (ι : Type) (x : Fintype ι) (w : ι → R) (z : ι → F),
        (∀ (i : ι), 0 ≤ w i) ∧ Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ t) ∧ ∑ i : ι, w i • z i = y),
    ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → R) (z : ι → E × F),
      (∀ (i : ι), 0 ≤ w i) ∧
        Eq.{u_1 + 1} (α := R) (∑ i : ι, w i) 1 ∧ (∀ (i : ι), z i ∈ s ×ˢ t) ∧ ∑ i : ι, w i • z i = (x, y)
⊢ Membership.mem (γ := Set (E × F)) ((convexHull R : (a : Set (E × F)) → Set (E × F)) (s ×ˢ t) : Set (E × F)) (x, y)

Tactic:
rw [mem_convexHull_iff_exists_fintype] at hx hy ⊢

Premises used: mem_convexHull_iff_exists_fintype