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_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 : ι
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
⊢ 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:
congr! with j _ g _
-- 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 : ι
j : κ i
h : Membership.mem (γ := Finset (κ i)) Finset.univ j
g : { g : (k : ι) → κ k // g i = j }
h_1 : Membership.mem (γ := Finset { g : (k : ι) → κ k // g i = j }) Finset.univ g
⊢ (↑g : (k : ι) → κ k) i = j

Tactic:
g.2

Premises used: Subtype.property
-- 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 : ι
j : κ i
h : Membership.mem (γ := Finset (κ i)) Finset.univ j
g : { g : (k : ι) → κ k // g i = j }
h_1 : Membership.mem (γ := Finset { g : (k : ι) → κ k // g i = j }) Finset.univ g
⊢ (↑g : (k : ι) → κ k) i = j

Tactic:
exact g.2

Premises used: Subtype.property
-- 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)
    (∑ 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:
?_
-- 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 : ι
⊢ ∑ j : κ i, w i j • f i j = x i

Tactic:
hf _
-- 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 : ι
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)
⊢ (∑ 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:
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 _
-- 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 : ι
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
⊢ 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:
congr! with j _
-- 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 : ι
j : κ i
h : Membership.mem (γ := Finset (κ i)) Finset.univ j
g : (a : ι) → κ a
hg :
  Membership.mem (γ := Finset ((a : ι) → κ a))
    (piFinset (δ := κ) fun (k : ι) ↦
      if hk : k = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ)
    g
⊢ g i = j

Tactic:
simpa using mem_piFinset.1 hg i

Premises used: Fintype.mem_piFinset, Iff.mp
-- 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 : ι
j : κ i
h : Membership.mem (γ := Finset (κ i)) Finset.univ j
⊢ ∀ (a : { g : (k : ι) → κ k // g i = j })
    (ha : Membership.mem (γ := Finset { g : (k : ι) → κ k // g i = j }) Finset.univ a),
    Membership.mem (γ := Finset ((a : ι) → κ a))
      (piFinset (δ := κ) fun (k : ι) ↦
        if hk : k = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ)
      ((fun (g : { g : (k : ι) → κ k // g i = j })
            (x : Membership.mem (γ := Finset { g : (k : ι) → κ k // g i = j }) Finset.univ g) ↦
          (↑g : (k : ι) → κ k))
        a ha)

Tactic:
aesop
-- 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 : ι
j : κ i
h : Membership.mem (γ := Finset (κ i)) Finset.univ j
⊢ ∀ (a : (a : ι) → κ a)
    (ha :
      Membership.mem (γ := Finset ((a : ι) → κ a))
        (piFinset (δ := κ) fun (k : ι) ↦
          if hk : k = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ)
        a),
    Membership.mem (γ := Finset { g : (k : ι) → κ k // g i = j }) Finset.univ
      ((fun (g : (a : ι) → κ a)
            (hg :
              Membership.mem (γ := Finset ((a : ι) → κ a))
                (piFinset (δ := κ) fun (k : ι) ↦
                  if hk : k = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ)
                g) ↦
          (Subtype.mk (p := fun (g : (k : ι) → κ k) ↦ g i = j) g ⋯ : { g : (k : ι) → κ k // g i = j }))
        a ha)

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 : 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
⊢ ∀ (a : { g : (k : ι) → κ k // g i = j })
    (ha : Membership.mem (γ := Finset { g : (k : ι) → κ k // g i = j }) Finset.univ a),
    (fun (g : (a : ι) → κ a)
            (hg :
              Membership.mem (γ := Finset ((a : ι) → κ a))
                (piFinset (δ := κ) fun (k : ι) ↦
                  if hk : k = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ)
                g) ↦
          (Subtype.mk (p := fun (g : (k : ι) → κ k) ↦ g i = j) g ⋯ : { g : (k : ι) → κ k // g i = j }))
        ((fun (g : { g : (k : ι) → κ k // g i = j })
              (x : Membership.mem (γ := Finset { g : (k : ι) → κ k // g i = j }) Finset.univ g) ↦
            (↑g : (k : ι) → κ k))
          a ha)
        ⋯ =
      a

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 : 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
⊢ ∀ (a : (a : ι) → κ a)
    (ha :
      Membership.mem (γ := Finset ((a : ι) → κ a))
        (piFinset (δ := κ) fun (k : ι) ↦
          if hk : k = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ)
        a),
    (fun (g : { g : (k : ι) → κ k // g i = j })
            (x : Membership.mem (γ := Finset { g : (k : ι) → κ k // g i = j }) Finset.univ g) ↦
          (↑g : (k : ι) → κ k))
        ((fun (g : (a : ι) → κ a)
              (hg :
                Membership.mem (γ := Finset ((a : ι) → κ a))
                  (piFinset (δ := κ) fun (k : ι) ↦
                    if hk : k = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ)
                  g) ↦
            (Subtype.mk (p := fun (g : (k : ι) → κ k) ↦ g i = j) g ⋯ : { g : (k : ι) → κ k // g i = j }))
          a ha)
        ⋯ =
      a

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 : 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
⊢ ∀ (a : { g : (k : ι) → κ k // g i = j })
    (ha : Membership.mem (γ := Finset { g : (k : ι) → κ k // g i = j }) Finset.univ a),
    Eq.{u_1 + 1} (α := 𝕜) (∏ k : ι, w k ((↑a : (k : ι) → κ k) k))
      (∏ k : ι,
        w k
          ((fun (g : { g : (k : ι) → κ k // g i = j })
                (x : Membership.mem (γ := Finset { g : (k : ι) → κ k // g i = j }) Finset.univ g) ↦
              (↑g : (k : ι) → κ k))
            a ha k))

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 : 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
h₁ :
  (j ∉ if hk : i = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ) → w i j = 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

Tactic:
rw [← prod_univ_sum, ← prod_mul_prod_compl, Finset.prod_singleton, Finset.sum_eq_single,
        Finset.prod_eq_one, mul_one]

Premises used: Finset.prod_singleton, Finset.prod_eq_one, Finset.prod_mul_prod_compl, Finset.sum_eq_single, mul_one, Finset.prod_univ_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
i : ι
j : κ i
h : Membership.mem (γ := Finset (κ i)) Finset.univ j
⊢ ∀ (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

Tactic:
simp +contextual [hw₁]
-- 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 : ι
j : κ i
h : Membership.mem (γ := Finset (κ i)) Finset.univ j
⊢ ∀ (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

Tactic:
simp +contextual [hw₁]
-- 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 : ι
j : κ i
h : Membership.mem (γ := Finset (κ i)) Finset.univ j
⊢ (j ∉ if hk : i = i then Eq.rec (motive := fun (x : ι) (h : i = x) ↦ Finset (κ x)) {j} ⋯ else Finset.univ) → w i j = 0

Tactic:
simp +contextual [hw₁]
-- 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 : ι
j : κ i
h : Membership.mem (γ := Finset (κ i)) Finset.univ j
g :
  ∑
      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
⊢ ∑ g : { g : (k : ι) → κ k // g i = j }, ∏ k : ι, w k ((↑g : (k : ι) → κ k) 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₁]

Premises used: Finset.univ, Fintype.piFinset, dite, Finset.sum_bij', Eq
-- 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)
⊢ Eq (α := Set ((i : ι) → E i))
    ((convexHull 𝕜 : (a : Set ((i : ι) → E i)) → Set ((i : ι) → E i)) (s.pi (α := E) t) : Set ((i : ι) → E i))
    (s.pi (α := E) fun (i : ι) ↦ (convexHull 𝕜 : (a : Set (E i)) → Set (E i)) (t i) : Set ((i : ι) → E i))

Tactic:
Set.Subset.antisymm (convexHull_min (Set.pi_mono fun _ _ ↦ subset_convexHull _ _) <| convex_pi <|
    fun _ _ ↦ convex_convexHull _ _) fun _ ↦ mem_convexHull_pi

Premises used: Set.Subset.antisymm, convex_pi, mem_convexHull_pi, subset_convexHull, convex_convexHull, convexHull_min, Set.pi_mono
-- Module: Mathlib.Analysis.Convex.Combination
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
h :
  ∀ (p : V),
    Membership.mem (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) (range s.points) : Set V) p ↔ p ∈ s.closedInterior
⊢ (convexHull 𝕜 : (a : Set V) → Set V) (range s.points) = s.closedInterior

Tactic:
ext p
-- Module: Mathlib.Analysis.Convex.Combination
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
⊢ Membership.mem (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) (range s.points) : Set V) p ↔ p ∈ s.closedInterior

Tactic:
rw [convexHull_range_eq_exists_affineCombination, Set.mem_setOf]

Premises used: Set.mem_setOf, convexHull_range_eq_exists_affineCombination
-- Module: Mathlib.Analysis.Convex.Combination
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
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
⊢ (∃ (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