awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
⊢ 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)))
have 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)))
Tactic: rw [← Fintype.sum_fiberwise fun g : ∀ k, κ k ↦ g i]
-- 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 : ι
⊢ 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))
have 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))
Tactic: simp_rw [sum_smul]
-- 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 : ι
⊢ 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))
have a : ∀ (j : κ i),
  Membership.mem (γ := Finset (κ i)) Finset.univ j →
    ∀ (g : { g : (k : ι) → κ k // g i = j }),
      Membership.mem (γ := Finset { g : (k : ι) → κ k // g i = j }) Finset.univ g → (↑g : (k : ι) → κ k) i = j
Tactic: congr! with j _ g _
-- 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 : ι) → κ 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
have refine_2 : 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)
Tactic: 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 _
-- 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 : ι
⊢ 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)
have refine_2 : ∀ (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
Tactic: congr! with j _
-- 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 : ι
j : κ i
h : Membership.mem (γ := Finset (κ i)) Finset.univ j
⊢ ∑
      g ∈
        piFinset (δ := κ) fun (k : ι) ↦
          if hk : k = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ,
      ∏ k : ι, w k (g k) =
    w i j
have rw : ∀ (x : ι),
  Membership.mem (γ := Finset ι) {i}ᶜ x →
    Eq.{u_1 + 1} (α := 𝕜)
      (∑ j ∈ if hk : x = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} sorry else Finset.univ, w x j)
      1
Tactic: rw [← prod_univ_sum, ← prod_mul_prod_compl, Finset.prod_singleton, Finset.sum_eq_single,
        Finset.prod_eq_one, mul_one]
-- 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 : ι
j : κ i
h : Membership.mem (γ := Finset (κ i)) Finset.univ j
rw :
  ∀ (x : ι),
    Membership.mem (γ := Finset ι) {i}ᶜ x →
      Eq.{u_1 + 1} (α := 𝕜)
        (∑ j ∈ if hk : x = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ,
          w x j)
        1
⊢ ∑
      g ∈
        piFinset (δ := κ) fun (k : ι) ↦
          if hk : k = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ,
      ∏ k : ι, w k (g k) =
    w i j
have h₀ : ∀ (b : κ i),
  Membership.mem (γ := Finset (κ i))
      (if hk : i = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} sorry else Finset.univ) b →
    b ≠ j → w i b = 0
Tactic: rw [← prod_univ_sum, ← prod_mul_prod_compl, Finset.prod_singleton, Finset.sum_eq_single,
        Finset.prod_eq_one, mul_one]
-- 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 : ι
j : κ i
h : Membership.mem (γ := Finset (κ i)) Finset.univ j
rw :
  ∀ (x : ι),
    Membership.mem (γ := Finset ι) {i}ᶜ x →
      Eq.{u_1 + 1} (α := 𝕜)
        (∑ j ∈ if hk : x = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ,
          w x j)
        1
h₀ :
  ∀ (b : κ i),
    Membership.mem (γ := Finset (κ i))
        (if hk : i = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ) b →
      b ≠ j → w i b = 0
⊢ ∑
      g ∈
        piFinset (δ := κ) fun (k : ι) ↦
          if hk : k = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ,
      ∏ k : ι, w k (g k) =
    w i j
have h₁ : (j ∉ if hk : i = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} sorry else Finset.univ) → w i j = 0
Tactic: rw [← prod_univ_sum, ← prod_mul_prod_compl, Finset.prod_singleton, Finset.sum_eq_single,
        Finset.prod_eq_one, mul_one]
-- 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 : ι
j : κ i
h : Membership.mem (γ := Finset (κ i)) Finset.univ j
⊢ ∑ g : { g : (k : ι) → κ k // g i = j }, ∏ k : ι, w k ((↑g : (k : ι) → κ k) k) = w i j
have g : ∑
    g ∈
      piFinset (δ := κ) fun (k : ι) ↦
        if hk : k = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} sorry else Finset.univ,
    ∏ k : ι, w k (g k) =
  w i j
Tactic: 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₁]
-- 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: 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₁]
-- 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
⊢ 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 ι)
  (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: 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₁]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
⊢ (convexHull 𝕜 : (a : Set V) → Set V) (range s.points) = s.closedInterior
have h : ∀ (p : V),
  Membership.mem (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) (range s.points) : Set V) p ↔ p ∈ s.closedInterior
Tactic: ext p
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
p : V
⊢ Membership.mem (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) (range s.points) : Set V) p ↔ p ∈ s.closedInterior
have h : (∃ (s_1 : Finset (Fin (n + 1))) (w : Fin (n + 1) → 𝕜),
    (∀ i ∈ s_1, 0 ≤ w i) ∧
      s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w = p) ↔
  p ∈ s.closedInterior
Tactic: rw [convexHull_range_eq_exists_affineCombination, Set.mem_setOf]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
p : V
⊢ (∃ (s_1 : Finset (Fin (n + 1))) (w : Fin (n + 1) → 𝕜),
      (∀ i ∈ s_1, 0 ≤ w i) ∧
        s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w = p) ↔
    p ∈ s.closedInterior
have h : (∃ (s_1 : Finset (Fin (n + 1))) (w : Fin (n + 1) → 𝕜),
    (∀ i ∈ s_1, 0 ≤ w i) ∧
      s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w = p) →
  p ∈ s.closedInterior
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
p : V
h :
  (∃ (s_1 : Finset (Fin (n + 1))) (w : Fin (n + 1) → 𝕜),
      (∀ i ∈ s_1, 0 ≤ w i) ∧
        s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w = p) →
    p ∈ s.closedInterior
⊢ (∃ (s_1 : Finset (Fin (n + 1))) (w : Fin (n + 1) → 𝕜),
      (∀ i ∈ s_1, 0 ≤ w i) ∧
        s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w = p) ↔
    p ∈ s.closedInterior
have h₁ : p ∈ s.closedInterior →
  ∃ (s_1 : Finset (Fin (n + 1))) (w : Fin (n + 1) → 𝕜),
    (∀ i ∈ s_1, 0 ≤ w i) ∧ s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
p : V
h :
  ∃ (s_1 : Finset (Fin (n + 1))) (w : Fin (n + 1) → 𝕜),
    (∀ i ∈ s_1, 0 ≤ w i) ∧ s_1.sum w = 1 ∧ (Finset.affineCombination 𝕜 s_1 s.points : (a : Fin (n + 1) → 𝕜) → V) w = p
⊢ p ∈ s.closedInterior
have h₁ : ∀ (u : Finset (Fin (n + 1))) (w : Fin (n + 1) → 𝕜) (hw : ∀ i ∈ u, 0 ≤ w i) (hw1 : u.sum w = 1),
  Membership.mem (α := V) s.closedInterior ((Finset.affineCombination 𝕜 u s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)
Tactic: obtain ⟨u, w, hw, hw1, rfl⟩ := h
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
i : Fin (n + 1)
hi : i ∈ u
⊢ w i ≤ 1
have rw : w i ≤ u.sum w
Tactic: rw [← hw1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
⊢ Membership.mem (α := V) s.closedInterior ((Finset.affineCombination 𝕜 u s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)
have hw' : ∀ i ∈ u, w i ≤ 1
Tactic: have hw' : ∀ i ∈ u, w i ≤ 1 := by
      intro i hi
      rw [← hw1]
      apply Finset.single_le_sum (fun j hj ↦ hw j hj) hi
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
⊢ Membership.mem (α := V) s.closedInterior ((Finset.affineCombination 𝕜 u s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)
have hw1' : Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), (↑u : Set (Fin (n + 1))).indicator w i) 1
Tactic: have hw1' : ∑ i, (u : Set (Fin (n + 1))).indicator w i = 1 := by
      simpa [Finset.sum_indicator_subset _ u.subset_univ] using hw1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : Eq.{u_1 + 1} (α := 𝕜) (∑ i : Fin (n + 1), (↑u : Set (Fin (n + 1))).indicator w i) 1
⊢ Membership.mem (α := V) s.closedInterior ((Finset.affineCombination 𝕜 u s.points : (a : Fin (n + 1) → 𝕜) → V) w : V)
have h : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set 𝕜) (Icc 0 1) ((↑u : Set (Fin (n + 1))).indicator w i)
Tactic: rw [Finset.affineCombination_indicator_subset _ _ u.subset_univ,
      affineCombination_mem_closedInterior_iff hw1']