awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : (↑t : Set E) ⊆ s
ht₂ : AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1
hw₃ : t.centerMass w id = x
t' : Finset E := {i ∈ t | w i ≠ 0}
⊢ ∀ (i : ↥t'), 0 < (w ∘ Subtype.val (p := fun (x : E) ↦ x ∈ t')) i

Tactic:
fun i =>
      (hw₁ _ (Finset.mem_filter.mp i.2).1).lt_of_ne (Finset.mem_filter.mp i.property).2.symm

Premises used: Ne.symm, LE.le.lt_of_ne, And.right, And.left, Iff.mp, Finset.mem_filter, Subtype.val, Subtype.property
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : (↑t : Set E) ⊆ s
ht₂ : AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1
hw₃ : t.centerMass w id = x
t' : Finset E := {i ∈ t | w i ≠ 0}
⊢ ∀ (i : ↥t'), 0 < (w ∘ Subtype.val (p := fun (x : E) ↦ x ∈ t')) i

Tactic:
exact fun i =>
      (hw₁ _ (Finset.mem_filter.mp i.2).1).lt_of_ne (Finset.mem_filter.mp i.property).2.symm

Premises used: LE.le.lt_of_ne, And.left, Iff.mp, Finset.mem_filter
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : (↑t : Set E) ⊆ s
ht₂ : AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1
hw₃ : t.centerMass w id = x
t' : Finset E := {i ∈ t | w i ≠ 0}
refine_4 : Eq.{u_1 + 1} (α := 𝕜) (∑ x ∈ t'.attach, w (↑x : E)) 1
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i : ↥t', (w ∘ Subtype.val (p := fun (x : E) ↦ x ∈ t')) i) 1

Tactic:
simp only [univ_eq_attach, Function.comp_apply]

Premises used: Finset.univ_eq_attach, Function.comp_apply
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : (↑t : Set E) ⊆ s
ht₂ : AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1
hw₃ : t.centerMass w id = x
t' : Finset E := {i ∈ t | w i ≠ 0}
refine_4 : Eq.{u_1 + 1} (α := 𝕜) (∑ x ∈ t', w x) 1
refine_4₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ x ∈ t, w x) 1
refine_4₂ refine_4₃ : Eq.{u_1 + 1} (α := 𝕜) 1 1
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ x ∈ t'.attach, w (↑x : E)) 1

Tactic:
rw [Finset.sum_attach, Finset.sum_filter_ne_zero, hw₂]

Premises used: Finset.sum_attach, Finset.sum_filter_ne_zero
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : (↑t : Set E) ⊆ s
ht₂ : AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1
hw₃ : t.centerMass w id = x
t' : Finset E := {i ∈ t | w i ≠ 0}
refine_5 : ∑ i ∈ t'.attach, (fun (e : E) ↦ w e • e) (↑i : E) = x
⊢ ∑ i : ↥t', (w ∘ Subtype.val (p := fun (x : E) ↦ x ∈ t')) i • (↑i : E) = x

Tactic:
change (∑ i ∈ t'.attach, (fun e => w e • e) ↑i) = x

Premises used: Finset.attach, HSMul.hSMul, Subtype.val, Finset.sum
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : (↑t : Set E) ⊆ s
ht₂ : AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1
hw₃ : t.centerMass w id = x
t' : Finset E := {i ∈ t | w i ≠ 0}
refine_5 : ∑ x ∈ t, w x • x = x
refine_5₁ : ∀ x ∈ t, w x • x ≠ 0 → w x ≠ 0
⊢ ∑ i ∈ t'.attach, (fun (e : E) ↦ w e • e) (↑i : E) = x

Tactic:
rw [Finset.sum_attach (f := fun e => w e • e), Finset.sum_filter_of_ne]

Premises used: Finset.sum_attach, Finset.sum_filter_of_ne, HSMul.hSMul
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : (↑t : Set E) ⊆ s
ht₂ : AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1
hw₃ : t.centerMass w id = x
t' : Finset E := {i ∈ t | w i ≠ 0}
⊢ ∑ i ∈ t, w i • id i = x

Tactic:
rw [t.centerMass_eq_of_sum_1 id hw₂] at hw₃

Premises used: id, Finset.centerMass_eq_of_sum_1
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : (↑t : Set E) ⊆ s
ht₂ : AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1
hw₃ : ∑ i ∈ t, w i • id i = x
t' : Finset E := {i ∈ t | w i ≠ 0}
⊢ ∑ x ∈ t, w x • x = x

Tactic:
hw₃
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : (↑t : Set E) ⊆ s
ht₂ : AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1
hw₃ : ∑ i ∈ t, w i • id i = x
t' : Finset E := {i ∈ t | w i ≠ 0}
⊢ ∑ x ∈ t, w x • x = x

Tactic:
exact hw₃
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : (↑t : Set E) ⊆ s
ht₂ : AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1
hw₃ : t.centerMass w id = x
t' : Finset E := {i ∈ t | w i ≠ 0}
e : E
refine_5 : e ∈ t → w e • e ≠ 0 → w e ≠ 0
⊢ e ∈ t → w e • e ≠ 0 → w e ≠ 0

Tactic:
_
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : (↑t : Set E) ⊆ s
ht₂ : AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1
hw₃ : t.centerMass w id = x
t' : Finset E := {i ∈ t | w i ≠ 0}
e : E
h : e ∈ t
hwe : w e • e ≠ 0
contra : w e = 0
refine_5 : w e • e = 0
⊢ False

Tactic:
apply hwe
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : (↑t : Set E) ⊆ s
ht₂ : AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1
hw₃ : t.centerMass w id = x
t' : Finset E := {i ∈ t | w i ≠ 0}
e : E
h : e ∈ t
hwe : w e • e ≠ 0
contra : w e = 0
refine_5 : HSMul.hSMul.{u_1, u, u} (α := 𝕜) 0 e = 0
refine_5₁ refine_5₂ : Eq.{u + 1} (α := E) 0 0
⊢ w e • e = 0

Tactic:
rw [contra, zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
w : ι → R
z : ι → E
⊢ centerMass ∅ w z = 0

Tactic:
simp only [centerMass, sum_empty, smul_zero]

Premises used: smul_zero, Finset.centerMass, Finset.sum_empty
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i j : ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
hne : i ≠ j
simp : (w i + w j)⁻¹ • (w i • z i + w j • z j) = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j
⊢ centerMass {i, j} w z = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j

Tactic:
simp only [centerMass, sum_pair hne]

Premises used: Finset.sum_pair, Finset.centerMass
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i j : ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
hne : i ≠ j
⊢ (w i + w j)⁻¹ • (w i • z i + w j • z j) = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j

Tactic:
module
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
ha : i ∉ t
hw : Ne.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
simp :
  (w i / (w i + ∑ i ∈ t, w i)) • z i + HSMul.hSMul (β := E) (w i + ∑ i ∈ t, w i)⁻¹ (∑ i ∈ t, w i • z i) =
    (w i / (w i + ∑ i ∈ t, w i)) • z i +
      HSMul.hSMul (β := E) ((∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹) (∑ i ∈ t, w i • z i)
⊢ (insert i t).centerMass w z =
    (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z

Tactic:
simp only [centerMass, sum_insert ha, smul_add, (mul_smul _ _ _).symm, ← div_eq_inv_mul]

Premises used: Finset.centerMass, Finset.sum_insert, div_eq_inv_mul, Eq.symm, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
ha : i ∉ t
hw : Ne.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
e_a : (w i + ∑ i ∈ t, w i)⁻¹ = (∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹
⊢ (w i / (w i + ∑ i ∈ t, w i)) • z i + HSMul.hSMul (β := E) (w i + ∑ i ∈ t, w i)⁻¹ (∑ i ∈ t, w i • z i) =
    (w i / (w i + ∑ i ∈ t, w i)) • z i +
      HSMul.hSMul (β := E) ((∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹) (∑ i ∈ t, w i • z i)

Tactic:
congr 2
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i : ι
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
ha : i ∉ t
hw : Ne.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
e_a : (w i + ∑ i ∈ t, w i)⁻¹ = HMul.hMul (α := R) (∑ i ∈ t, w i) (∑ i ∈ t, w i)⁻¹ / (w i + ∑ i ∈ t, w i)
e_a₁ : (w i + ∑ i ∈ t, w i)⁻¹ = 1 / (w i + ∑ i ∈ t, w i)
e_a₂ e_a₃ : (w i + ∑ i ∈ t, w i)⁻¹ = (w i + ∑ i ∈ t, w i)⁻¹
⊢ (w i + ∑ i ∈ t, w i)⁻¹ = (∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹

Tactic:
rw [div_mul_eq_mul_div, mul_inv_cancel₀ hw, one_div]

Premises used: mul_inv_cancel₀, div_mul_eq_mul_div, one_div
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i : ι
w : ι → R
z : ι → E
hw : w i ≠ 0
rw : (w i)⁻¹ • w i • z i = z i
⊢ centerMass {i} w z = z i

Tactic:
rw [centerMass, sum_singleton, sum_singleton]

Premises used: Finset.sum_singleton, Finset.centerMass
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i : ι
w : ι → R
z : ι → E
hw : w i ≠ 0
match_scalars : (w i)⁻¹ * (w i * 1) = 1
⊢ (w i)⁻¹ • w i • z i = z i

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i : ι
w : ι → R
z : ι → E
hw : w i ≠ 0
⊢ (w i)⁻¹ * (w i * 1) = 1

Tactic:
field
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
t : Finset ι
w : ι → R
z : ι → E
⊢ t.centerMass (-w) z = t.centerMass w z

Tactic:
simp [centerMass, inv_neg]

Premises used: inv_neg, Finset.centerMass
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : Field R'
inst_2 : AddCommGroup E
inst_3 : Module R E
t : Finset ι
w : ι → R
z : ι → E
c : R'
inst_4 : Module R' R
inst_5 : Module R' E
inst_6 : SMulCommClass R' R R
inst_7 : IsScalarTower R' R R
inst_8 : SMulCommClass R R' E
inst_9 : IsScalarTower R' R E
hc : c ≠ 0
⊢ t.centerMass (c • w) z = t.centerMass w z

Tactic:
simp [centerMass, -smul_assoc, smul_assoc c, ← smul_sum, smul_inv₀, smul_smul_smul_comm, hc]

Premises used: smul_assoc, smul_smul_smul_comm, smul_inv₀, Finset.smul_sum, Finset.centerMass
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
t : Finset ι
w : ι → R
z : ι → E
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
⊢ t.centerMass w z = ∑ i ∈ t, w i • z i

Tactic:
simp only [Finset.centerMass, hw, inv_one, one_smul]

Premises used: inv_one, one_smul, Finset.centerMass
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
c : R
t : Finset ι
w : ι → R
z : ι → E
⊢ (t.centerMass w fun (i : ι) ↦ c • z i) = c • t.centerMass w z

Tactic:
simp only [Finset.centerMass, Finset.smul_sum, (mul_smul _ _ _).symm, mul_comm c, mul_assoc]

Premises used: mul_assoc, Finset.smul_sum, mul_comm, Finset.centerMass, Eq.symm, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, ws i) 1
hwt : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, wt i) 1
a b : R
hab : a + b = 1
rw :
  Eq.{u_3 + 1} (α := E) (∑ x ∈ s.disjSum t, Sum.elim (fun (x : ι) ↦ a • ws x • zs x) (fun (x : ι') ↦ b • wt x • zt x) x)
    (∑ i ∈ s.disjSum t,
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) i)
        (Sum.elim zs zt i))
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s.disjSum t, Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) i) 1
⊢ a • s.centerMass ws zs + b • t.centerMass wt zt =
    (s.disjSum t).centerMass (R := R) (Sum.elim (fun (i : ι) ↦ a * ws i) fun (j : ι') ↦ b * wt j) (Sum.elim zs zt)

Tactic:
rw [s.centerMass_eq_of_sum_1 _ hws, t.centerMass_eq_of_sum_1 _ hwt, smul_sum, smul_sum, ←
    Finset.sum_sumElim, Finset.centerMass_eq_of_sum_1]

Premises used: Finset.sum_sumElim, Finset.smul_sum, Finset.centerMass_eq_of_sum_1
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, ws i) 1
hwt : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, wt i) 1
a b : R
hab : a + b = 1
e_f :
  ∀ (val : ι),
    Sum.elim (fun (x : ι) ↦ a • ws x • zs x) (fun (x : ι') ↦ b • wt x • zt x) (Sum.inl val) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) (Sum.inl val))
        (Sum.elim zs zt (Sum.inl val))
e_f₁ :
  ∀ (val : ι'),
    Sum.elim (fun (x : ι) ↦ a • ws x • zs x) (fun (x : ι') ↦ b • wt x • zt x) (Sum.inr val) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) (Sum.inr val))
        (Sum.elim zs zt (Sum.inr val))
⊢ Eq.{u_3 + 1} (α := E) (∑ x ∈ s.disjSum t, Sum.elim (fun (x : ι) ↦ a • ws x • zs x) (fun (x : ι') ↦ b • wt x • zt x) x)
    (∑ i ∈ s.disjSum t,
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) i)
        (Sum.elim zs zt i))

Tactic:
congr with ⟨⟩
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, ws i) 1
hwt : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, wt i) 1
a b : R
hab : a + b = 1
val : ι
⊢ Sum.elim (fun (x : ι) ↦ a • ws x • zs x) (fun (x : ι') ↦ b • wt x • zt x) (Sum.inl val) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) (Sum.inl val))
      (Sum.elim zs zt (Sum.inl val))

Tactic:
simp only [Sum.elim_inl, Sum.elim_inr, mul_smul]

Premises used: Sum.elim_inr, Sum.elim_inl, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, ws i) 1
hwt : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, wt i) 1
a b : R
hab : a + b = 1
val : ι'
⊢ Sum.elim (fun (x : ι) ↦ a • ws x • zs x) (fun (x : ι') ↦ b • wt x • zt x) (Sum.inr val) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) (Sum.inr val))
      (Sum.elim zs zt (Sum.inr val))

Tactic:
simp only [Sum.elim_inl, Sum.elim_inr, mul_smul]

Premises used: Sum.elim_inr, Sum.elim_inl, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
ι' : Type u_6
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Finset ι
t : Finset ι'
ws : ι → R
zs : ι → E
wt : ι' → R
zt : ι' → E
hws : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, ws i) 1
hwt : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, wt i) 1
a b : R
hab : a + b = 1
hw : HAdd.hAdd (α := R) (∑ x ∈ s, a * ws x) (∑ x ∈ t, b * wt x) = 1
hw₁ : a * ∑ i ∈ s, ws i + ∑ x ∈ t, b * wt x = 1
hw₂ : a * ∑ i ∈ s, ws i + b * ∑ i ∈ t, wt i = 1
hw₃ : a * 1 + b * ∑ i ∈ t, wt i = 1
hw₄ : a * 1 + b * 1 = 1
hw₅ : a + b * 1 = 1
hw₆ : a + b = 1
hw₇ hw₈ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s.disjSum t, Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) i) 1

Tactic:
rw [sum_sumElim, ← mul_sum, ← mul_sum, hws, hwt, mul_one, mul_one, hab]

Premises used: Finset.mul_sum, Finset.sum_sumElim, mul_one
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Finset ι
w₁ w₂ : ι → R
z : ι → E
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
a b : R
hab : a + b = 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (a * w₁ i + b * w₂ i)) 1

Tactic:
simp only [← mul_sum, sum_add_distrib, mul_one, *]

Premises used: Finset.mul_sum, Finset.sum_add_distrib, mul_one
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Finset ι
w₁ w₂ : ι → R
z : ι → E
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
a b : R
hab : a + b = 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (a * w₁ i + b * w₂ i)) 1

Tactic:
have hw : (∑ i ∈ s, (a * w₁ i + b * w₂ i)) = 1 := by
    simp only [← mul_sum, sum_add_distrib, mul_one, *]
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Finset ι
w₁ w₂ : ι → R
z : ι → E
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w₂ i) 1
a b : R
hab : a + b = 1
hw : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, (a * w₁ i + b * w₂ i)) 1
⊢ a • s.centerMass w₁ z + b • s.centerMass w₂ z =
    centerMass.{u_1, u_3, u_5} (R := R) s (fun (i : ι) ↦ a * w₁ i + b * w₂ i) z

Tactic:
simp only [Finset.centerMass_eq_of_sum_1, smul_sum, sum_add_distrib, add_smul, mul_smul, *]

Premises used: Finset.sum_add_distrib, add_smul, Finset.smul_sum, Finset.centerMass_eq_of_sum_1, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i : ι
t : Finset ι
z : ι → E
inst_3 : DecidableEq ι
hi : i ∈ t
rw : ∑ i_1 ∈ t, HSMul.hSMul.{u_1, u_3, u_3} (α := R) (if i = i_1 then 1 else 0) (z i_1) = z i
hw : Eq.{u_1 + 1} (α := R) (∑ i_1 ∈ t, if i = i_1 then 1 else 0) 1
⊢ centerMass.{u_1, u_3, u_5} (R := R) t (fun (j : ι) ↦ if i = j then 1 else 0) z = z i

Tactic:
rw [Finset.centerMass_eq_of_sum_1]

Premises used: Finset.centerMass_eq_of_sum_1
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i : ι
t : Finset ι
z : ι → E
inst_3 : DecidableEq ι
hi : i ∈ t
trans :
  Eq.{u_3 + 1} (α := E) (∑ i_1 ∈ t, HSMul.hSMul.{u_1, u_3, u_3} (α := R) (if i = i_1 then 1 else 0) (z i_1))
    (∑ j ∈ t, if i = j then z i else 0)
trans₁ : (∑ j ∈ t, if i = j then z i else 0) = z i
⊢ ∑ i_1 ∈ t, HSMul.hSMul.{u_1, u_3, u_3} (α := R) (if i = i_1 then 1 else 0) (z i_1) = z i

Tactic:
trans ∑ j ∈ t, if i = j then z i else 0
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i : ι
t : Finset ι
z : ι → E
inst_3 : DecidableEq ι
hi : i ∈ t
e_f : ∀ (i_1 : ι), HSMul.hSMul.{u_1, u_3, u_3} (α := R) (if i = i_1 then 1 else 0) (z i_1) = if i = i_1 then z i else 0
⊢ Eq.{u_3 + 1} (α := E) (∑ i_1 ∈ t, HSMul.hSMul.{u_1, u_3, u_3} (α := R) (if i = i_1 then 1 else 0) (z i_1))
    (∑ j ∈ t, if i = j then z i else 0)

Tactic:
congr with i
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i_1 : ι
t : Finset ι
z : ι → E
inst_3 : DecidableEq ι
hi : i_1 ∈ t
i : ι
pos : ∀ (h : i_1 = i), HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 (z i) = z i_1
neg : ∀ (h : ¬i_1 = i), HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 (z i) = 0
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (if i_1 = i then 1 else 0) (z i) = if i_1 = i then z i_1 else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i_1 : ι
t : Finset ι
z : ι → E
inst_3 : DecidableEq ι
hi : i_1 ∈ t
i : ι
h : i_1 = i
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 (z i) = z i_1

Tactic:
h ▸ one_smul _ _

Premises used: Eq.rec, one_smul
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i_1 : ι
t : Finset ι
z : ι → E
inst_3 : DecidableEq ι
hi : i_1 ∈ t
i : ι
h : ¬i_1 = i
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 (z i) = 0

Tactic:
zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i_1 : ι
t : Finset ι
z : ι → E
inst_3 : DecidableEq ι
hi : i_1 ∈ t
i : ι
h : i_1 = i
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 (z i) = z i_1

Tactic:
exacts [h ▸ one_smul _ _, zero_smul _ _]

Premises used: zero_smul
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i : ι
t : Finset ι
z : ι → E
inst_3 : DecidableEq ι
hi : i ∈ t
rw : (if i ∈ t then z i else 0) = z i
rw₁ rw₂ : z i = z i
⊢ (∑ j ∈ t, if i = j then z i else 0) = z i

Tactic:
rw [sum_ite_eq, if_pos hi]

Premises used: if_pos, Finset.sum_ite_eq
-- Module: Mathlib.Analysis.Convex.Combination
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
i : ι
t : Finset ι
z : ι → E
inst_3 : DecidableEq ι
hi : i ∈ t
hw : Eq.{u_1 + 1} (α := R) (if i ∈ t then 1 else 0) 1
hw₁ hw₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i_1 ∈ t, if i = i_1 then 1 else 0) 1

Tactic:
rw [sum_ite_eq, if_pos hi]

Premises used: if_pos, Finset.sum_ite_eq