awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
⊢ t.centerMass w z = t'.centerMass w z
have rw : Eq.{u_3 + 1} (α := E) (∑ x ∈ t, HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ x ∈ t', w x)⁻¹ (w x • z x))
  (∑ x ∈ t', HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ i ∈ t', w i)⁻¹ (w x • z x))
Tactic: rw [centerMass, sum_subset ht h, smul_sum, centerMass, smul_sum]
-- 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
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
⊢ Eq.{u_3 + 1} (α := E) (∑ x ∈ t, HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ x ∈ t', w x)⁻¹ (w x • z x))
    (∑ x ∈ t', HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ i ∈ t', w i)⁻¹ (w x • z x))
have apply : ∀ x ∈ t', x ∉ t → HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ x ∈ t', w x)⁻¹ (w x • z x) = 0
Tactic: apply sum_subset ht
-- 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
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
i : ι
hit' : i ∈ t'
hit : i ∉ t
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ x ∈ t', w x)⁻¹ (w i • z i) = 0
have rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ x ∈ t', w x)⁻¹ (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 (z i)) = 0
Tactic: rw [h i hit' hit, zero_smul, smul_zero]
-- 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
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
i : ι
hit' : i ∈ t'
hit : i ∉ t
rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ x ∈ t', w x)⁻¹ (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 (z i)) = 0
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ x ∈ t', w x)⁻¹ (w i • z i) = 0
have rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ x ∈ t', w x)⁻¹ 0 = 0
Tactic: rw [h i hit' hit, zero_smul, smul_zero]
-- 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
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
i : ι
hit' : i ∈ t'
hit : i ∉ t
rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ x ∈ t', w x)⁻¹ (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 (z i)) = 0
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ x ∈ t', w x)⁻¹ 0 = 0
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∑ x ∈ t', w x)⁻¹ (w i • z i) = 0
have rw₂ : Eq.{u_3 + 1} (α := E) 0 0
Tactic: rw [h i hit' hit, zero_smul, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
ι : Type u_5
α : Type u_7
inst : Field R
inst_1 : AddCommGroup α
inst_2 : LinearOrder α
inst_3 : Module R α
inst_4 : LinearOrder R
inst_5 : IsOrderedAddMonoid α
inst_6 : PosSMulMono R α
s : Finset ι
f : ι → α
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : LT.lt.{u_1} (α := R) 0 (∑ i ∈ s, w i)
⊢ s.centerMass w f ≤ s.sup' ⋯ f
have rw : LE.le.{u_7} (α := α) (∑ i ∈ s, w i • f i) (∑ i ∈ s, w i • s.sup' sorry f)
Tactic: rw [centerMass, inv_smul_le_iff_of_pos hw₁, sum_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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ t.centerMass w z = t'.centerMass w' z'
have rw : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i • z' i)
Tactic: rw [← centerMass_filter_ne_zero, centerMass, ← centerMass_filter_ne_zero, centerMass]
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i • z' i)
have e_a : Eq.{u_1 + 1} (α := R) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹
Tactic: congr 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
e_a : Eq.{u_1 + 1} (α := R) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i • z' i)
have e_a₁ : Eq.{u_3 + 1} (α := E) (∑ i ∈ t with w i ≠ 0, w i • z i) (∑ i ∈ t' with w' i ≠ 0, w' i • z' i)
Tactic: congr 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹
have e_a : Eq.{u_1 + 1} (α := R) (∑ i ∈ t with w i ≠ 0, w i) (∑ i ∈ t' with w' i ≠ 0, w' i)
Tactic: congr 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
⊢ t.centerMass w z = t'.centerMass w' z'
have rw : {i ∈ t | w i ≠ 0}.centerMass w z = t'.centerMass w' z'
Tactic: classical
  rw [← centerMass_filter_ne_zero, centerMass, ← centerMass_filter_ne_zero, centerMass]
  congr 1
  · congr 1
    exact sum_congr (by grind) (by grind)
  · exact sum_congr (by grind) (by grind)
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
rw : {i ∈ t | w i ≠ 0}.centerMass w z = t'.centerMass w' z'
⊢ t.centerMass w z = t'.centerMass w' z'
have rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
  t'.centerMass w' z'
Tactic: classical
  rw [← centerMass_filter_ne_zero, centerMass, ← centerMass_filter_ne_zero, centerMass]
  congr 1
  · congr 1
    exact sum_congr (by grind) (by grind)
  · exact sum_congr (by grind) (by grind)
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
rw : {i ∈ t | w i ≠ 0}.centerMass w z = t'.centerMass w' z'
rw₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    t'.centerMass w' z'
⊢ t.centerMass w z = t'.centerMass w' z'
have rw₂ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
  {i ∈ t' | w' i ≠ 0}.centerMass w' z'
Tactic: classical
  rw [← centerMass_filter_ne_zero, centerMass, ← centerMass_filter_ne_zero, centerMass]
  congr 1
  · congr 1
    exact sum_congr (by grind) (by grind)
  · exact sum_congr (by grind) (by grind)
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
rw : {i ∈ t | w i ≠ 0}.centerMass w z = t'.centerMass w' z'
rw₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    t'.centerMass w' z'
rw₂ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    {i ∈ t' | w' i ≠ 0}.centerMass w' z'
⊢ t.centerMass w z = t'.centerMass w' z'
have rw₃ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i • z' i)
Tactic: classical
  rw [← centerMass_filter_ne_zero, centerMass, ← centerMass_filter_ne_zero, centerMass]
  congr 1
  · congr 1
    exact sum_congr (by grind) (by grind)
  · exact sum_congr (by grind) (by grind)
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
rw : {i ∈ t | w i ≠ 0}.centerMass w z = t'.centerMass w' z'
rw₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    t'.centerMass w' z'
rw₂ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    {i ∈ t' | w' i ≠ 0}.centerMass w' z'
rw₃ rw₄ rw₅ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i • z' i)
⊢ t.centerMass w z = t'.centerMass w' z'
have e_a : Eq.{u_1 + 1} (α := R) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹
Tactic: classical
  rw [← centerMass_filter_ne_zero, centerMass, ← centerMass_filter_ne_zero, centerMass]
  congr 1
  · congr 1
    exact sum_congr (by grind) (by grind)
  · exact sum_congr (by grind) (by grind)
-- 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
t : Finset ι
w : ι → R
z : ι → E
inst_3 : DecidableEq ι
t' : Finset ι
w' : ι → R
z' : ι → E
h : ∀ (i : ι), i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0 → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i
rw : {i ∈ t | w i ≠ 0}.centerMass w z = t'.centerMass w' z'
rw₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    t'.centerMass w' z'
rw₂ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    {i ∈ t' | w' i ≠ 0}.centerMass w' z'
rw₃ rw₄ rw₅ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t with w i ≠ 0, w i • z i) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := E) (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i • z' i)
e_a : Eq.{u_1 + 1} (α := R) (∑ i ∈ t with w i ≠ 0, w i)⁻¹ (∑ i ∈ t' with w' i ≠ 0, w' i)⁻¹
⊢ t.centerMass w z = t'.centerMass w' z'
have e_a₁ : Eq.{u_3 + 1} (α := E) (∑ i ∈ t with w i ≠ 0, w i • z i) (∑ i ∈ t' with w' i ≠ 0, w' i • z' i)
Tactic: classical
  rw [← centerMass_filter_ne_zero, centerMass, ← centerMass_filter_ne_zero, centerMass]
  congr 1
  · congr 1
    exact sum_congr (by grind) (by grind)
  · exact sum_congr (by grind) (by grind)
-- 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 : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : LT.lt.{u_1} (α := R) 0 (∑ i ∈ insert i t, w i)
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
⊢ (insert i t).centerMass w z ∈ s
have zi : z i ∈ s
Tactic: have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
-- 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 : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : LT.lt.{u_1} (α := R) 0 (∑ i ∈ insert i t, w i)
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
⊢ (insert i t).centerMass w z ∈ s
have hs₀ : ∀ j ∈ t, 0 ≤ w j
Tactic: have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
-- 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 : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : LT.lt.{u_1} (α := R) 0 (∑ i ∈ insert i t, w i)
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
⊢ (insert i t).centerMass w z ∈ s
have hpos₁ : 0 < w i + ∑ x ∈ t, w x
Tactic: rw [sum_insert hi] at hpos
Cleared hypotheses: hpos, hmem, zi, hs₀
-- 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
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
⊢ (insert i t).centerMass w z ∈ s
have pos : ∀ (hsum_t : Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0), (insert i t).centerMass w z ∈ s
Tactic: by_cases hsum_t : ∑ j ∈ t, w j = 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
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
pos : ∀ (hsum_t : Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0), (insert i t).centerMass w z ∈ s
⊢ (insert i t).centerMass w z ∈ s
have neg : ∀ (hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0), (insert i t).centerMass w z ∈ s
Tactic: by_cases hsum_t : ∑ j ∈ t, w j = 0
-- 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 : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
⊢ (insert i t).centerMass w z ∈ s
have ws : ∀ j ∈ t, w j = 0
Tactic: have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
-- 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 : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
ws : ∀ j ∈ t, w j = 0
⊢ (insert i t).centerMass w z ∈ s
have wz : Eq.{u_3 + 1} (α := E) (∑ j ∈ t, w j • z j) 0
Tactic: have wz : ∑ j ∈ t, w j • z j = 0 := sum_eq_zero fun i hi => by simp [ws i 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
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
ws : ∀ j ∈ t, w j = 0
wz : Eq.{u_3 + 1} (α := E) (∑ j ∈ t, w j • z j) 0
⊢ (insert i t).centerMass w z ∈ s
have pos : (w i)⁻¹ • w i • z i ∈ s
Tactic: simp only [centerMass, sum_insert hi, wz, hsum_t, add_zero]
-- 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 : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
ws : ∀ j ∈ t, w j = 0
wz : Eq.{u_3 + 1} (α := E) (∑ j ∈ t, w j • z j) 0
⊢ (w i)⁻¹ • w i • z i ∈ s
have hpos₁ : 0 < w i
Tactic: simp only [hsum_t, add_zero] at hpos
Cleared hypotheses: hpos
-- 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
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
⊢ (insert i t).centerMass w z ∈ s
have neg : (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z ∈ s
Tactic: rw [Finset.centerMass_insert _ _ _ hi hsum_t]
-- 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
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
⊢ (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z ∈ s
have neg : LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i)
Tactic: refine convex_iff_div.1 hs zi (ht hs₀ ?_ ?_) ?_ (sum_nonneg hs₀) hpos
-- 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
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
neg : LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i)
⊢ (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z ∈ s
have neg₁ : ∀ i ∈ t, z i ∈ s
Tactic: refine convex_iff_div.1 hs zi (ht hs₀ ?_ ?_) ?_ (sum_nonneg hs₀) hpos
-- 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
s : Set E
t_1 : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
i : ι
t : Finset ι
hi : i ∉ t
ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
hpos : 0 < w i + ∑ x ∈ t, w x
hmem : ∀ i_1 ∈ insert i t, z i_1 ∈ s
zi : z i ∈ s
hs₀ : ∀ j ∈ t, 0 ≤ w j
hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0
neg : LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i)
neg₁ : ∀ i ∈ t, z i ∈ s
⊢ (w i / (w i + ∑ j ∈ t, w j)) • z i + ((∑ j ∈ t, w j) / (w i + ∑ j ∈ t, w j)) • t.centerMass w z ∈ s
have neg₂ : 0 ≤ w i
Tactic: refine convex_iff_div.1 hs zi (ht hs₀ ?_ ?_) ?_ (sum_nonneg hs₀) hpos