awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Combination
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)
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
⊢ 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 ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Convex.Combination
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
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
⊢ 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

Premises used: Set.univ
-- Module: Mathlib.Analysis.Convex.Combination
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
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
⊢ 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:
rw [← pi_univ_ite]

Premises used: Set.pi_univ_ite
-- Module: Mathlib.Analysis.Convex.Combination
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

Tactic:
this (fun i _ ↦ ?_) rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Combination
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
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)
⊢ 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:
refine this (fun i _ ↦ ?_) rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Combination
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)
neg :
  ∀ (hi : i ∉ s),
    Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) Set.univ : 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)

Tactic:
split_ifs with hi
-- Module: Mathlib.Analysis.Convex.Combination
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
hi : i ∈ s
⊢ Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i)

Tactic:
h i hi
-- Module: Mathlib.Analysis.Convex.Combination
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
hi : i ∈ s
⊢ Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set (E i)) (x i)

Tactic:
exact h i hi
-- Module: Mathlib.Analysis.Convex.Combination
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
hi : i ∉ s
⊢ Membership.mem (γ := Set (E i)) ((convexHull 𝕜 : (a : Set (E i)) → Set (E i)) Set.univ : Set (E i)) (x i)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Combination
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
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
⊢ 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:
subst hs
-- Module: Mathlib.Analysis.Convex.Combination
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)
⊢ ∀ (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

Premises used: true_implies, mem_convexHull_iff_exists_fintype, Set.mem_univ
-- Module: Mathlib.Analysis.Convex.Combination
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
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
⊢ 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
-- Module: Mathlib.Analysis.Convex.Combination
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

Tactic:
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 _ _) ?_

Premises used: Finset.univ, Set.Mem, Finset.prod, mem_convexHull_of_exists_fintype, Finset.prod_nonneg
-- Module: Mathlib.Analysis.Convex.Combination
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
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
⊢ 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:
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 _ _) ?_
-- Module: Mathlib.Analysis.Convex.Combination
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 : ι, ∑ j : κ i, w i j) 1
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i : (i : ι) → κ i, (fun (k : (i : ι) → κ i) ↦ (∏ i : ι, w i (k i) : 𝕜)) i) 1

Tactic:
rw [← Fintype.prod_sum]

Premises used: Fintype.prod_sum
-- Module: Mathlib.Analysis.Convex.Combination
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 : ι, ∑ j : κ i, w i j) 1

Tactic:
prod_eq_one fun _ _ ↦ hw₁ _

Premises used: Finset.prod_eq_one
-- Module: Mathlib.Analysis.Convex.Combination
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 : ι, ∑ j : κ i, w i j) 1

Tactic:
exact prod_eq_one fun _ _ ↦ hw₁ _

Premises used: Finset.prod_eq_one
-- Module: Mathlib.Analysis.Convex.Combination
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_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
⊢ ∑ 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:
ext i
-- Module: Mathlib.Analysis.Convex.Combination
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 : ι
⊢ Eq.{u_3 + 1} (α := E 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)
    (∑ g : (i : ι) → κ i, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (∏ i : ι, w i (g i)) (f i (g i)))

Tactic:
simp only [Finset.sum_apply, Pi.smul_apply]

Premises used: Finset.sum_apply, Pi.smul_apply
-- Module: Mathlib.Analysis.Convex.Combination
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 : ι
rw rw₁ :
  Eq.{u_3 + 1} (α := E i)
    (∑ j : κ i,
      ∑ i_1 : { i_1 : (k : ι) → κ k // i_1 i = j },
        HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (∏ i_2 : ι, w i_2 ((↑i_1 : (k : ι) → κ k) i_2))
          (f i ((↑i_1 : (k : ι) → κ k) i)))
    (∑ j : κ i,
      ∑ g : { g : (k : ι) → κ k // g i = j },
        HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (∏ k : ι, w k ((↑g : (k : ι) → κ k) k)) (f i ((↑g : (k : ι) → κ k) i)))
⊢ Eq.{u_3 + 1} (α := E i) (∑ g : (i : ι) → κ i, HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (∏ i : ι, w i (g i)) (f i (g i)))
    (∑ j : κ i,
      ∑ g : { g : (k : ι) → κ k // g i = j },
        HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (∏ k : ι, w k ((↑g : (k : ι) → κ k) k)) (f i ((↑g : (k : ι) → κ k) i)))

Tactic:
rw [← Fintype.sum_fiberwise fun g : ∀ k, κ k ↦ g i]

Premises used: Fintype.sum_fiberwise
-- Module: Mathlib.Analysis.Convex.Combination
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 : ι
simp_rw :
  Eq.{u_3 + 1} (α := E i)
    (∑ j : κ i,
      ∑ g : { g : (k : ι) → κ k // g i = j },
        HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (∏ k : ι, w k ((↑g : (k : ι) → κ k) k)) (f i ((↑g : (k : ι) → κ k) i)))
    (∑ x : κ i,
      ∑ i_1 : { g : (k : ι) → κ k // g i = x },
        HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (∏ k : ι, w k ((↑i_1 : (k : ι) → κ k) k)) (f i x))
⊢ Eq.{u_3 + 1} (α := E i)
    (∑ j : κ i,
      ∑ g : { g : (k : ι) → κ k // g i = j },
        HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (∏ k : ι, w k ((↑g : (k : ι) → κ k) k)) (f i ((↑g : (k : ι) → κ k) i)))
    (∑ j : κ i,
      HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜)
        (∑ g : { g : (k : ι) → κ k // g i = j }, ∏ k : ι, w k ((↑g : (k : ι) → κ k) k)) (f i j))

Tactic:
simp_rw [sum_smul]

Premises used: Finset.sum_smul