-- 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)
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
⊢ 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 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
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₁]
Cleared hypotheses: h