-- 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
intro₁ :
  ∀ (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
cases cases₁ :
  ∀ (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
cases₂ :
  ∀ (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
cases₃ :
  ∀ (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
cases₄ :
  ∀ (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
refine_1 :
  ∀ (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
refine_2 refine_2₁ :
  ∀ (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
refine_2₂ :
  ∀ (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 : ι) → κ 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
refine_2₃ :
  ∀ (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)
      (∑ 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))
      (∑ j : κ i, w i j • f i j)
refine_2₄ :
  ∀ (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 : ι) (j : κ i),
    Membership.mem (γ := Finset (κ i)) Finset.univ j →
      ∑ g : { g : (k : ι) → κ k // g i = j }, ∏ k : ι, w k ((↑g : (k : ι) → κ k) k) = w i j
⊢ 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:
classical
  cases nonempty_fintype ι
  wlog hs : s = Set.univ generalizing s t
  · rw [← pi_univ_ite]
    refine this (fun i _ ↦ ?_) rfl
    split_ifs with hi
    · exact h i hi
    · simp
  subst hs
  simp only [Set.mem_univ, mem_convexHull_iff_exists_fintype, true_implies] at h
  choose κ _ w f hw₀ hw₁ hft hf using h
  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 _ _) ?_
  · rw [← Fintype.prod_sum]
    exact prod_eq_one fun _ _ ↦ hw₁ _
  ext i
  calc
    _ = ∑ g : ∀ i, κ i, (∏ i, w i (g i)) • f i (g i) := by
      simp only [Finset.sum_apply, Pi.smul_apply]
    _ = ∑ j : κ i, ∑ g : {g : ∀ k, κ k // g i = j},
          (∏ k, w k (g.1 k)) • f i ((g : ∀ i, κ i) i) := by
      rw [← Fintype.sum_fiberwise fun g : ∀ k, κ k ↦ g i]
    _ = ∑ j : κ i, (∑ g : {g : ∀ k, κ k // g i = j}, ∏ k, w k (g.1 k)) • f i j := by
      simp_rw [sum_smul]
      congr! with j _ g _
      exact g.2
    _ = ∑ j : κ i, w i j • f i j := ?_
    _ = x i := hf _
  congr! with j _
  calc
    ∑ g : {g : ∀ k, κ k // g i = j}, ∏ k, w k (g.1 k)
      = ∑ g ∈ piFinset fun k ↦ if hk : k = i then hk ▸ {j} else univ, ∏ k, w k (g k) :=
      Finset.sum_bij' (fun g _ ↦ g) (fun g hg ↦ ⟨g, by simpa using mem_piFinset.1 hg i⟩)
        (by aesop) (by simp) (by simp) (by simp) (by simp)
    _ = w i j := by
      rw [← prod_univ_sum, ← prod_mul_prod_compl, Finset.prod_singleton, Finset.sum_eq_single,
        Finset.prod_eq_one, mul_one] <;> simp +contextual [hw₁]

Premises used: Set.univ, Fintype.prod_sum, nonempty_fintype, true_implies, Set.pi_univ_ite, mem_convexHull_iff_exists_fintype, Finset.sum_bij', Set.mem_univ