awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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 ∘ Subtype.val (p := fun (x : E) ↦ x ∈ t')) i • (↑i : E) = x
have refine_5 : ∑ i ∈ t'.attach, (fun (e : E) ↦ w e • e) (↑i : E) = x
Tactic: change (∑ i ∈ t'.attach, (fun e => w e • e) ↑i) = x
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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'.attach, (fun (e : E) ↦ w e • e) (↑i : E) = x
have refine_5 : ∑ x ∈ t, w x • x = x
Tactic: rw [Finset.sum_attach (f := fun e => w e • e), Finset.sum_filter_of_ne]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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
⊢ ∑ i ∈ t'.attach, (fun (e : E) ↦ w e • e) (↑i : E) = x
have refine_5₁ : ∀ x ∈ t, w x • x ≠ 0 → w x ≠ 0
Tactic: rw [Finset.sum_attach (f := fun e => w e • e), Finset.sum_filter_of_ne]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (hypothesis)
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}
⊢ ∑ x ∈ t, w x • x = x
have hw₄ : ∑ i ∈ t, w i • id i = x
Tactic: rw [t.centerMass_eq_of_sum_1 id hw₂] at hw₃
Cleared hypotheses: hw₃, t'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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
⊢ False
have refine_5 : w e • e = 0
Tactic: apply hwe
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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
⊢ w e • e = 0
have refine_5 : HSMul.hSMul.{u_1, u, u} (α := 𝕜) 0 e = 0
Tactic: rw [contra, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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
⊢ w e • e = 0
have refine_5₁ : Eq.{u + 1} (α := E) 0 0
Tactic: rw [contra, zero_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ centerMass {i, j} w z = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j
have 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
Tactic: simp only [centerMass, sum_pair hne]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ (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
have 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)
Tactic: simp only [centerMass, sum_insert ha, smul_add, (mul_smul _ _ _).symm, ← div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ (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)
have e_a : (w i + ∑ i ∈ t, w i)⁻¹ = (∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ (w i + ∑ i ∈ t, w i)⁻¹ = (∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹
have 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)
Tactic: rw [div_mul_eq_mul_div, mul_inv_cancel₀ hw, one_div]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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)
⊢ (w i + ∑ i ∈ t, w i)⁻¹ = (∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹
have e_a₁ : (w i + ∑ i ∈ t, w i)⁻¹ = 1 / (w i + ∑ i ∈ t, w i)
Tactic: rw [div_mul_eq_mul_div, mul_inv_cancel₀ hw, one_div]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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)
⊢ (w i + ∑ i ∈ t, w i)⁻¹ = (∑ i ∈ t, w i) / (w i + ∑ i ∈ t, w i) * (∑ i ∈ t, w i)⁻¹
have e_a₂ : (w i + ∑ i ∈ t, w i)⁻¹ = (w i + ∑ i ∈ t, w i)⁻¹
Tactic: rw [div_mul_eq_mul_div, mul_inv_cancel₀ hw, one_div]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ centerMass {i} w z = z i
have rw : (w i)⁻¹ • w i • z i = z i
Tactic: rw [centerMass, sum_singleton, sum_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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 • z i = z i
have match_scalars : (w i)⁻¹ * (w i * 1) = 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ 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)
have 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))
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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))
⊢ 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)
have hw : 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 [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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ 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))
have 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))
Tactic: congr with ⟨⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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))
⊢ 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))
have 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))
Tactic: congr with ⟨⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s.disjSum t, Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) i) 1
have hw : HAdd.hAdd (α := R) (∑ x ∈ s, a * ws x) (∑ x ∈ t, b * wt x) = 1
Tactic: rw [sum_sumElim, ← mul_sum, ← mul_sum, hws, hwt, mul_one, mul_one, hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s.disjSum t, Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) i) 1
have hw₁ : a * ∑ i ∈ s, ws i + ∑ x ∈ t, b * wt x = 1
Tactic: rw [sum_sumElim, ← mul_sum, ← mul_sum, hws, hwt, mul_one, mul_one, hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s.disjSum t, Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) i) 1
have hw₂ : a * ∑ i ∈ s, ws i + b * ∑ i ∈ t, wt i = 1
Tactic: rw [sum_sumElim, ← mul_sum, ← mul_sum, hws, hwt, mul_one, mul_one, hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s.disjSum t, Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) i) 1
have hw₃ : a * 1 + b * ∑ i ∈ t, wt i = 1
Tactic: rw [sum_sumElim, ← mul_sum, ← mul_sum, hws, hwt, mul_one, mul_one, hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s.disjSum t, Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) i) 1
have hw₄ : a * 1 + b * 1 = 1
Tactic: rw [sum_sumElim, ← mul_sum, ← mul_sum, hws, hwt, mul_one, mul_one, hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s.disjSum t, Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) i) 1
have hw₅ : a + b * 1 = 1
Tactic: rw [sum_sumElim, ← mul_sum, ← mul_sum, hws, hwt, mul_one, mul_one, hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ s.disjSum t, Sum.elim (fun (i : ι) ↦ a * ws i) (fun (j : ι') ↦ b * wt j) i) 1
have hw₇ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [sum_sumElim, ← mul_sum, ← mul_sum, hws, hwt, mul_one, mul_one, hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (hypothesis)
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
⊢ 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
have hw : 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, *]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ centerMass.{u_1, u_3, u_5} (R := R) t (fun (j : ι) ↦ if i = j then 1 else 0) z = z i
have 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
Tactic: rw [Finset.centerMass_eq_of_sum_1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ centerMass.{u_1, u_3, u_5} (R := R) t (fun (j : ι) ↦ if i = j then 1 else 0) z = z i
have hw : Eq.{u_1 + 1} (α := R) (∑ i_1 ∈ t, if i = i_1 then 1 else 0) 1
Tactic: rw [Finset.centerMass_eq_of_sum_1]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ ∑ 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
have 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)
Tactic: trans ∑ j ∈ t, if i = j then z i else 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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)
⊢ ∑ 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
have trans₁ : (∑ j ∈ t, if i = j then z i else 0) = z i
Tactic: trans ∑ j ∈ t, if i = j then z i else 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ 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)
have 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
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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 : ι
⊢ 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
have pos : ∀ (h : i_1 = i), HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 (z i) = z i_1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ 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
have neg : ∀ (h : ¬i_1 = i), HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 (z i) = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ (∑ j ∈ t, if i = j then z i else 0) = z i
have rw : (if i ∈ t then z i else 0) = z i
Tactic: rw [sum_ite_eq, if_pos hi]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ (∑ j ∈ t, if i = j then z i else 0) = z i
have rw₁ : z i = z i
Tactic: rw [sum_ite_eq, if_pos hi]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ i_1 ∈ t, if i = i_1 then 1 else 0) 1
have hw : Eq.{u_1 + 1} (α := R) (if i ∈ t then 1 else 0) 1
Tactic: rw [sum_ite_eq, if_pos hi]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ i_1 ∈ t, if i = i_1 then 1 else 0) 1
have hw₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [sum_ite_eq, if_pos hi]