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
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)
have 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)
Tactic: classical
  refine (Set.subset_inter (convexHull_mono inf_le_left) <|
    convexHull_mono inf_le_right).antisymm ?_
  simp_rw [Set.subset_def, mem_inter_iff, Set.inf_eq_inter, ← coe_inter, mem_convexHull']
  rintro x ⟨⟨w₁, h₁w₁, h₂w₁, h₃w₁⟩, w₂, -, h₂w₂, h₃w₂⟩
  let w (x : E) : R := (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
  have h₁w : ∑ i ∈ s, w i = 0 := by simp [w, Finset.inter_eq_right.2, *]
  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]
  have ht (x) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂) : w₁ x = 0 := by
    simpa [w, hx₁, hx₂] using hs _ (ht₁ hx₁)
  refine ⟨w₁, ?_, ?_, ?_⟩
  · simp only [and_imp, Finset.mem_inter]
    exact fun y hy₁ _ ↦ h₁w₁ y hy₁
  all_goals
  · rwa [sum_subset inter_subset_left]
    rintro x
    simp_intro hx₁ hx₂
    simp [ht x hx₁ hx₂]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s 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)
have refine₁ : ∀ (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
Tactic: classical
  refine (Set.subset_inter (convexHull_mono inf_le_left) <|
    convexHull_mono inf_le_right).antisymm ?_
  simp_rw [Set.subset_def, mem_inter_iff, Set.inf_eq_inter, ← coe_inter, mem_convexHull']
  rintro x ⟨⟨w₁, h₁w₁, h₂w₁, h₃w₁⟩, w₂, -, h₂w₂, h₃w₂⟩
  let w (x : E) : R := (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
  have h₁w : ∑ i ∈ s, w i = 0 := by simp [w, Finset.inter_eq_right.2, *]
  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]
  have ht (x) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂) : w₁ x = 0 := by
    simpa [w, hx₁, hx₂] using hs _ (ht₁ hx₁)
  refine ⟨w₁, ?_, ?_, ?_⟩
  · simp only [and_imp, Finset.mem_inter]
    exact fun y hy₁ _ ↦ h₁w₁ y hy₁
  all_goals
  · rwa [sum_subset inter_subset_left]
    rintro x
    simp_intro hx₁ hx₂
    simp [ht x hx₁ hx₂]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s 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)
refine₁ :
  ∀ (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
⊢ 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)
have refine₂ : ∀ (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 : 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: classical
  refine (Set.subset_inter (convexHull_mono inf_le_left) <|
    convexHull_mono inf_le_right).antisymm ?_
  simp_rw [Set.subset_def, mem_inter_iff, Set.inf_eq_inter, ← coe_inter, mem_convexHull']
  rintro x ⟨⟨w₁, h₁w₁, h₂w₁, h₃w₁⟩, w₂, -, h₂w₂, h₃w₂⟩
  let w (x : E) : R := (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
  have h₁w : ∑ i ∈ s, w i = 0 := by simp [w, Finset.inter_eq_right.2, *]
  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]
  have ht (x) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂) : w₁ x = 0 := by
    simpa [w, hx₁, hx₂] using hs _ (ht₁ hx₁)
  refine ⟨w₁, ?_, ?_, ?_⟩
  · simp only [and_imp, Finset.mem_inter]
    exact fun y hy₁ _ ↦ h₁w₁ y hy₁
  all_goals
  · rwa [sum_subset inter_subset_left]
    rintro x
    simp_intro hx₁ hx₂
    simp [ht x hx₁ hx₂]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : Finite ι
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i)
⊢ Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x
have intro : ∀ (val : Fintype ι),
  Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : Finite ι
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i)
val : Fintype ι
⊢ Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x
have intro : ∀
  (this :
    ∀ {s : Set ι} {t : (i : ι) → Set (E i)}
      (h :
        ∀ i ∈ s, Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i))
      (hs : s = Set.univ),
      Membership.mem (γ := Set ((i : ι) → E i))
        ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x)
  (hs : ¬s = Set.univ),
  Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x
Tactic: wlog hs : s = Set.univ generalizing s t
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : Finite ι
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i)
val : Fintype ι
intro :
  ∀
    (this :
      ∀ {s : Set ι} {t : (i : ι) → Set (E i)}
        (h :
          ∀ i ∈ s,
            Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i))
        (hs : s = Set.univ),
        Membership.mem (γ := Set ((i : ι) → E i))
          ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x)
    (hs : ¬s = Set.univ),
    Membership.mem (γ := Set ((i : ι) → E i))
      ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x
⊢ Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x
have wlog : ∀ {s : Set ι} {t : (i : ι) → Set (E i)}
  (h : ∀ i ∈ s, Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i))
  (hs : s = Set.univ),
  Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x
Tactic: wlog hs : s = Set.univ generalizing s t
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : Finite ι
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i)
val : Fintype ι
this :
  ∀ {s : Set ι} {t : (i : ι) → Set (E i)}
    (h :
      ∀ i ∈ s, Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i))
    (hs : s = Set.univ),
    Membership.mem (γ := Set ((i : ι) → E i))
      ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x
hs : ¬s = Set.univ
⊢ Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x
have intro : Membership.mem (γ := Set ((i : ι) → E i))
  ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i))
      (Set.pi (α := E) Set.univ fun (i : ι) ↦ if i ∈ s then t i else Set.univ) :
    Set ((i : ι) → E i))
  x
Tactic: rw [← pi_univ_ite]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : Finite ι
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i)
val : Fintype ι
this :
  ∀ {s : Set ι} {t : (i : ι) → Set (E i)}
    (h :
      ∀ i ∈ s, Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i))
    (hs : s = Set.univ),
    Membership.mem (γ := Set ((i : ι) → E i))
      ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x
hs : ¬s = Set.univ
⊢ Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i))
        (Set.pi (α := E) Set.univ fun (i : ι) ↦ if i ∈ s then t i else Set.univ) :
      Set ((i : ι) → E i))
    x
have intro : ∀ (i : ι),
  Membership.mem (γ := Set ι) Set.univ i →
    Membership.mem (γ := Set (E i))
      ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (if i ∈ s then t i else Set.univ) : Set (E i)) (x i)
Tactic: refine this (fun i _ ↦ ?_) rfl
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : Finite ι
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i)
val : Fintype ι
this :
  ∀ {s : Set ι} {t : (i : ι) → Set (E i)}
    (h :
      ∀ i ∈ s, Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i))
    (hs : s = Set.univ),
    Membership.mem (γ := Set ((i : ι) → E i))
      ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x
hs : ¬s = Set.univ
i : ι
h_1 : Membership.mem (γ := Set ι) Set.univ i
⊢ Membership.mem (γ := Set (E i))
    ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (if i ∈ s then t i else Set.univ) : Set (E i)) (x i)
have pos : ∀ (hi : i ∈ s), Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : Finite ι
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
s : Set ι
t : (i : ι) → Set (E i)
x : (i : ι) → E i
h : ∀ i ∈ s, Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i)
val : Fintype ι
this :
  ∀ {s : Set ι} {t : (i : ι) → Set (E i)}
    (h :
      ∀ i ∈ s, Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i))
    (hs : s = Set.univ),
    Membership.mem (γ := Set ((i : ι) → E i))
      ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x
hs : ¬s = Set.univ
i : ι
h_1 : Membership.mem (γ := Set ι) Set.univ i
pos :
  ∀ (hi : i ∈ s), Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i)
⊢ Membership.mem (γ := Set (E i))
    ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (if i ∈ s then t i else Set.univ) : Set (E i)) (x i)
have neg : ∀ (hi : i ∉ s),
  Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) Set.univ : Set (E i)) (x i)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : Finite ι
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
s_1 : Set ι
t_1 : (i : ι) → Set (E i)
x : (i : ι) → E i
val : Fintype ι
s : Set ι
t : (i : ι) → Set (E i)
h : ∀ i ∈ s, Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i)
hs : s = Set.univ
⊢ Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i)) x
have subst : ∀
  (h :
    ∀ (i : ι),
      Membership.mem (γ := Set ι) Set.univ i →
        Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i)),
  Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (Set.pi (α := E) Set.univ t) :
      Set ((i : ι) → E i))
    x
Tactic: subst hs
Cleared hypotheses: s, h, hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (hypothesis)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : Finite ι
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
s : Set ι
t_1 : (i : ι) → Set (E i)
x : (i : ι) → E i
val : Fintype ι
t : (i : ι) → Set (E i)
h :
  ∀ (i : ι),
    Membership.mem (γ := Set ι) Set.univ i →
      Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i)
⊢ Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (Set.pi (α := E) Set.univ t) :
      Set ((i : ι) → E i))
    x
have h₁ : ∀ (i : ι),
  ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → 𝕜) (z : ι → E i),
    (∀ (i : ι), 0 ≤ w i) ∧
      Eq.{u_1 + 1} (α := 𝕜) (∑ i : ι, w i) 1 ∧ (∀ (i_1 : ι), z i_1 ∈ t i) ∧ ∑ i_1 : ι, w i_1 • z i_1 = x i
Tactic: simp only [Set.mem_univ, mem_convexHull_iff_exists_fintype, true_implies] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : Finite ι
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
s : Set ι
t_1 : (i : ι) → Set (E i)
x : (i : ι) → E i
val : Fintype ι
t : (i : ι) → Set (E i)
h :
  ∀ (i : ι),
    ∃ (ι : Type) (x_1 : Fintype ι) (w : ι → 𝕜) (z : ι → E i),
      (∀ (i : ι), 0 ≤ w i) ∧
        Eq.{u_1 + 1} (α := 𝕜) (∑ i : ι, w i) 1 ∧ (∀ (i_1 : ι), z i_1 ∈ t i) ∧ ∑ i_1 : ι, w i_1 • z i_1 = x i
⊢ Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (Set.pi (α := E) Set.univ t) :
      Set ((i : ι) → E i))
    x
have choose : ∀ (κ : (i : ι) → Type) (x_1 : (i : ι) → Fintype (κ i)) (w : (i : ι) → κ i → 𝕜) (f : (i : ι) → κ i → E i)
  (hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1) (hw₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) (∑ i_1 : κ i, w i i_1) 1)
  (hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i) (hf : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 • f i i_1 = x i),
  Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (Set.pi (α := E) Set.univ t) :
      Set ((i : ι) → E i))
    x
Tactic: choose κ _ w f hw₀ hw₁ hft hf using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : Finite ι
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
s : Set ι
t_1 : (i : ι) → Set (E i)
x : (i : ι) → E i
val : Fintype ι
t : (i : ι) → Set (E i)
κ : (i : ι) → Type
x_1 : (i : ι) → Fintype (κ i)
w : (i : ι) → κ i → 𝕜
f : (i : ι) → κ i → E i
hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1
hw₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) (∑ i_1 : κ i, w i i_1) 1
hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i
hf : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 • f i i_1 = x i
⊢ Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (Set.pi (α := E) Set.univ t) :
      Set ((i : ι) → E i))
    x
have refine_1 : Eq.{u_1 + 1} (α := 𝕜) (∑ i : (i : ι) → κ i, (fun (k : (i : ι) → κ i) ↦ (∏ i : ι, w i (k i) : 𝕜)) i) 1
Tactic: refine mem_convexHull_of_exists_fintype (fun k : Π i, κ i ↦ ∏ i, w i (k i)) (fun g i ↦ f _ (g i))
    (fun g ↦ prod_nonneg fun _ _ ↦ hw₀ _ _) ?_ (fun _ _ _ ↦ hft _ _) ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : Finite ι
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
s : Set ι
t_1 : (i : ι) → Set (E i)
x : (i : ι) → E i
val : Fintype ι
t : (i : ι) → Set (E i)
κ : (i : ι) → Type
x_1 : (i : ι) → Fintype (κ i)
w : (i : ι) → κ i → 𝕜
f : (i : ι) → κ i → E i
hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1
hw₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) (∑ i_1 : κ i, w i i_1) 1
hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i
hf : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 • f i i_1 = x i
refine_1 : Eq.{u_1 + 1} (α := 𝕜) (∑ i : (i : ι) → κ i, (fun (k : (i : ι) → κ i) ↦ (∏ i : ι, w i (k i) : 𝕜)) i) 1
⊢ Membership.mem (γ := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (Set.pi (α := E) Set.univ t) :
      Set ((i : ι) → E i))
    x
have refine_2 : ∑ i : (i : ι) → κ i,
    HSMul.hSMul (α := 𝕜) (β := (i : ι) → E i) ((fun (k : (i : ι) → κ i) ↦ (∏ i : ι, w i (k i) : 𝕜)) i)
      ((fun (g : (i : ι) → κ i) (i : ι) ↦ f i (g i)) i) =
  x
Tactic: refine mem_convexHull_of_exists_fintype (fun k : Π i, κ i ↦ ∏ i, w i (k i)) (fun g i ↦ f _ (g i))
    (fun g ↦ prod_nonneg fun _ _ ↦ hw₀ _ _) ?_ (fun _ _ _ ↦ hft _ _) ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : Finite ι
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
s : Set ι
t_1 : (i : ι) → Set (E i)
x : (i : ι) → E i
val : Fintype ι
t : (i : ι) → Set (E i)
κ : (i : ι) → Type
x_1 : (i : ι) → Fintype (κ i)
w : (i : ι) → κ i → 𝕜
f : (i : ι) → κ i → E i
hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1
hw₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) (∑ i_1 : κ i, w i i_1) 1
hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i
hf : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 • f i i_1 = x i
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i : (i : ι) → κ i, (fun (k : (i : ι) → κ i) ↦ (∏ i : ι, w i (k i) : 𝕜)) i) 1
have refine_1 : Eq.{u_1 + 1} (α := 𝕜) (∏ i : ι, ∑ j : κ i, w i j) 1
Tactic: rw [← Fintype.prod_sum]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : Finite ι
inst_1 : Field 𝕜
inst_2 : LinearOrder 𝕜
inst_3 : IsStrictOrderedRing 𝕜
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
s : Set ι
t_1 : (i : ι) → Set (E i)
x : (i : ι) → E i
val : Fintype ι
t : (i : ι) → Set (E i)
κ : (i : ι) → Type
x_1 : (i : ι) → Fintype (κ i)
w : (i : ι) → κ i → 𝕜
f : (i : ι) → κ i → E i
hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1
hw₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := 𝕜) (∑ i_1 : κ i, w i i_1) 1
hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i
hf : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 • f i i_1 = x i
⊢ ∑ i : (i : ι) → κ i,
      HSMul.hSMul (α := 𝕜) (β := (i : ι) → E i) ((fun (k : (i : ι) → κ i) ↦ (∏ i : ι, w i (k i) : 𝕜)) i)
        ((fun (g : (i : ι) → κ i) (i : ι) ↦ f i (g i)) i) =
    x
have refine_2 : ∀ (i : ι),
  (∑ i : (i : ι) → κ i,
        HSMul.hSMul (α := 𝕜) (β := (i : ι) → E i) ((fun (k : (i : ι) → κ i) ↦ (∏ i : ι, w i (k i) : 𝕜)) i)
          ((fun (g : (i : ι) → κ i) (i : ι) ↦ f i (g i)) i))
      i =
    x i
Tactic: ext i