awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi : ¬w i = 0
hzi : z i = t.centerMass w z
⊢ w i + ∑ j ∈ t, w j ≠ 0

Tactic:
have hwi : w i + ∑ j ∈ t, w j ≠ 0 := by
        refine LT.lt.ne' ?_
        have hwi : 0 < w i := by grind
        grw [hwi]
        simp only [lt_add_iff_pos_right, gt_iff_lt]
        exact (sum_nonneg hs₀).lt_of_ne' hsum_t
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
pos : t.centerMass w z ∈ interior 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 ∈ interior s

Tactic:
simp only [hzi, ← add_smul, ← add_div, ne_eq, hwi, not_false_eq_true, div_self, one_smul]

Premises used: ne_eq, one_smul, add_smul, not_false_eq_true, div_self, add_div
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
pos :
  ∀ (hijt : ∃ (i'' : ι) (j'' : ι), i'' ∈ t ∧ j'' ∈ t ∧ z i'' ≠ z j'' ∧ w i'' ≠ 0 ∧ w j'' ≠ 0),
    t.centerMass w z ∈ interior s
neg :
  ∀ (hijt : ∀ (i'' j'' : ι) (_ : i'' ∈ t) (_ : j'' ∈ t) (_ : z i'' ≠ z j'') (_ : w i'' ≠ 0), w j'' = 0),
    t.centerMass w z ∈ interior s
⊢ t.centerMass w z ∈ interior s

Tactic:
by_cases! hijt : ∃ i'' j'', i'' ∈ t ∧ j'' ∈ t ∧ z i'' ≠ z j'' ∧ w i'' ≠ 0 ∧ w j'' ≠ 0
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∃ (i'' : ι) (j'' : ι), i'' ∈ t ∧ j'' ∈ t ∧ z i'' ≠ z j'' ∧ w i'' ≠ 0 ∧ w j'' ≠ 0
⊢ t.centerMass w z ∈ interior s

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∀ (i'' j'' : ι) (_ : i'' ∈ t) (_ : j'' ∈ t) (_ : z i'' ≠ z j'') (_ : w i'' ≠ 0), w j'' = 0
neg : False
⊢ t.centerMass w z ∈ interior s

Tactic:
exfalso
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∀ (i'' j'' : ι) (_ : i'' ∈ t) (_ : j'' ∈ t) (_ : z i'' ≠ z j'') (_ : w i'' ≠ 0), w j'' = 0
⊢ ∃ i'' ∈ t, w i'' ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∀ (i'' j'' : ι) (_ : i'' ∈ t) (_ : j'' ∈ t) (_ : z i'' ≠ z j'') (_ : w i'' ≠ 0), w j'' = 0
neg : ∀ (i'' : ι) (hi'' : i'' ∈ t) (hwi'' : w i'' ≠ 0), False
⊢ False

Tactic:
obtain ⟨i'', hi'', hwi''⟩ : ∃ i'' ∈ t, w i'' ≠ 0 := by grind
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∀ (i'' j'' : ι) (_ : i'' ∈ t) (_ : j'' ∈ t) (_ : z i'' ≠ z j'') (_ : w i'' ≠ 0), w j'' = 0
i'' : ι
hi'' : i'' ∈ t
hwi'' : w i'' ≠ 0
⊢ ∀ j'' ∈ t, w j'' ≠ 0 → z j'' = Function.const ι (z i'') j''

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∀ (i'' j'' : ι) (_ : i'' ∈ t) (_ : j'' ∈ t) (_ : z i'' ≠ z j'') (_ : w i'' ≠ 0), w j'' = 0
i'' : ι
hi'' : i'' ∈ t
hwi'' : w i'' ≠ 0
⊢ ∀ j'' ∈ t, w j'' ≠ 0 → z j'' = Function.const ι (z i'') j''

Tactic:
have hijt' : ∀ j'', j'' ∈ t → w j'' ≠ 0 → z j'' = Function.const _ (z i'') j'' := by
          grind
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∀ (i'' j'' : ι) (_ : i'' ∈ t) (_ : j'' ∈ t) (_ : z i'' ≠ z j'') (_ : w i'' ≠ 0), w j'' = 0
i'' : ι
hi'' : i'' ∈ t
hwi'' : w i'' ≠ 0
hijt' : ∀ j'' ∈ t, w j'' ≠ 0 → z j'' = Function.const ι (z i'') j''
⊢ i = i' ∨ i = j'

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∀ (i'' j'' : ι) (_ : i'' ∈ t) (_ : j'' ∈ t) (_ : z i'' ≠ z j'') (_ : w i'' ≠ 0), w j'' = 0
i'' : ι
hi'' : i'' ∈ t
hwi'' : w i'' ≠ 0
hijt' : ∀ j'' ∈ t, w j'' ≠ 0 → z j'' = Function.const ι (z i'') j''
⊢ i = i' ∨ i = j'

Tactic:
have hi : i = i' ∨ i = j' := by grind
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi_2 : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∀ (i'' j'' : ι) (_ : i'' ∈ t) (_ : j'' ∈ t) (_ : z i'' ≠ z j'') (_ : w i'' ≠ 0), w j'' = 0
i'' : ι
hi'' : i'' ∈ t
hwi'' : w i'' ≠ 0
hijt' : ∀ j'' ∈ t, w j'' ≠ 0 → z j'' = Function.const ι (z i'') j''
hi : i = i' ∨ i = j'
rw : t.centerMass w (Function.const ι (z i'')) = z i''
rw₁ rw₂ : z i'' = z i''
⊢ t.centerMass w z = z i''

Tactic:
rw [t.centerMass_congr_fun hijt', t.centerMass_const hsum_t]

Premises used: Finset.centerMass_const, Finset.centerMass_congr_fun
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi_2 : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∀ (i'' j'' : ι) (_ : i'' ∈ t) (_ : j'' ∈ t) (_ : z i'' ≠ z j'') (_ : w i'' ≠ 0), w j'' = 0
i'' : ι
hi'' : i'' ∈ t
hwi'' : w i'' ≠ 0
hijt' : ∀ j'' ∈ t, w j'' ≠ 0 → z j'' = Function.const ι (z i'') j''
hi : i = i' ∨ i = j'
⊢ t.centerMass w z = z i''

Tactic:
have hzi'' : t.centerMass w z = z i'' := by
          rw [t.centerMass_congr_fun hijt', t.centerMass_const hsum_t]
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi_2 : ¬w i = 0
hzi : z i = t.centerMass w z
hwi : w i + ∑ j ∈ t, w j ≠ 0
hijt : ∀ (i'' j'' : ι) (_ : i'' ∈ t) (_ : j'' ∈ t) (_ : z i'' ≠ z j'') (_ : w i'' ≠ 0), w j'' = 0
i'' : ι
hi'' : i'' ∈ t
hwi'' : w i'' ≠ 0
hijt' : ∀ j'' ∈ t, w j'' ≠ 0 → z j'' = Function.const ι (z i'') j''
hi : i = i' ∨ i = j'
hzi'' : t.centerMass w z = z i''
⊢ False

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi : ¬w i = 0
hzi : ¬z i = t.centerMass w z
⊢ 0 < w i

Tactic:
grind
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
w : ι → R
z : ι → V
hs : StrictConvex R s
i : ι
t : Finset ι
hi_1 : i ∉ t
ht :
  (∀ i ∈ t, 0 ≤ w i) →
    ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s
h₀ : ∀ i_1 ∈ insert i t, 0 ≤ w i_1
i' j' : ι
hi' : i' ∈ insert i t
hj' : j' ∈ insert i t
hi'j' : z i' ≠ z j'
hi'0 : w i' ≠ 0
hj'0 : w j' ≠ 0
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
hi : ¬w i = 0
hzi : ¬z 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 ∈ interior s

Tactic:
exact strictConvex_iff_div.1 hs zi
        (hs.convex.centerMass_mem hs₀ (lt_of_le_of_ne (sum_nonneg hs₀) (Ne.symm hsum_t))
          (fun j hj ↦ hmem j (mem_insert_of_mem hj))) hzi (by grind)
        ((sum_nonneg hs₀).lt_of_ne' hsum_t)

Premises used: Convex.centerMass_mem, Ne.symm, Finset.sum_nonneg, Finset.mem_insert_of_mem, Iff.mp, strictConvex_iff_div, StrictConvex.convex, LE.le.lt_of_ne', lt_of_le_of_ne
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
t : Finset ι
w : ι → R
z : ι → V
hs : StrictConvex R s
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ s
rw : t.centerMass w z ∈ interior s
⊢ ∑ k ∈ t, w k • z k ∈ interior s

Tactic:
rw [← t.centerMass_eq_of_sum_1 _ h1]

Premises used: Finset.centerMass_eq_of_sum_1
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
t : Finset ι
w : ι → R
z : ι → V
hs : StrictConvex R s
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ s
⊢ t.centerMass w z ∈ interior s

Tactic:
hs.centerMass_mem_interior h0 i j hi hj hij hi0 hj0 hz

Premises used: StrictConvex.centerMass_mem_interior
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
R : Type u_1
V : Type u_2
ι : Type u_4
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup V
inst_5 : Module R V
s : Set V
t : Finset ι
w : ι → R
z : ι → V
hs : StrictConvex R s
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ s
⊢ t.centerMass w z ∈ interior s

Tactic:
exact hs.centerMass_mem_interior h0 i j hi hj hij hi0 hj0 hz

Premises used: StrictConvex.centerMass_mem_interior
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
p : V
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ closedBall p r
inl : ∀ (hz : ∀ i ∈ t, z i ∈ closedBall p 0), t.centerMass w z ∈ ball p 0
inr : ∀ (hr : r ≠ 0), t.centerMass w z ∈ ball p r
⊢ t.centerMass w z ∈ ball p r

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
p : V
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ closedBall p 0
⊢ t.centerMass w z ∈ ball p 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
p : V
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ closedBall p r
hr : r ≠ 0
inr : t.centerMass w z ∈ interior (closedBall p r)
⊢ t.centerMass w z ∈ ball p r

Tactic:
rw [← interior_closedBall _ hr]

Premises used: interior_closedBall
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
p : V
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ closedBall p r
hr : r ≠ 0
⊢ t.centerMass w z ∈ interior (closedBall p r)

Tactic:
(strictConvex_closedBall _ _ _).centerMass_mem_interior h0 i j hi hj hij hi0 hj0 hz

Premises used: Set.Mem, strictConvex_closedBall, StrictConvex.centerMass_mem_interior
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
p : V
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ closedBall p r
hr : r ≠ 0
⊢ t.centerMass w z ∈ interior (closedBall p r)

Tactic:
exact (strictConvex_closedBall _ _ _).centerMass_mem_interior h0 i j hi hj hij hi0 hj0 hz

Premises used: strictConvex_closedBall, StrictConvex.centerMass_mem_interior
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
p : V
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq (α := ℝ) (∑ i ∈ t, w i) 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ closedBall p r
rw : t.centerMass w z ∈ ball p r
⊢ ∑ k ∈ t, w k • z k ∈ ball p r

Tactic:
rw [← t.centerMass_eq_of_sum_1 _ h1]

Premises used: Finset.centerMass_eq_of_sum_1
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
p : V
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq (α := ℝ) (∑ i ∈ t, w i) 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ closedBall p r
⊢ t.centerMass w z ∈ ball p r

Tactic:
centerMass_mem_ball_of_strictConvexSpace h0 hi hj hij hi0 hj0 hz

Premises used: centerMass_mem_ball_of_strictConvexSpace
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
p : V
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq (α := ℝ) (∑ i ∈ t, w i) 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, z i ∈ closedBall p r
⊢ t.centerMass w z ∈ ball p r

Tactic:
exact centerMass_mem_ball_of_strictConvexSpace h0 hi hj hij hi0 hj0 hz

Premises used: centerMass_mem_ball_of_strictConvexSpace
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq (α := ℝ) (∑ i ∈ t, w i) 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, ‖z i‖ ≤ r
⊢ ∀ i ∈ t, Membership.mem (γ := Set V) (closedBall 0 r) (z i)

Tactic:
simp_rw [← mem_closedBall_zero_iff] at hz

Premises used: mem_closedBall_zero_iff
-- Module: Mathlib.Analysis.Convex.StrictCombination
Goal:
V : Type u_2
ι : Type u_4
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
t : Finset ι
w : ι → ℝ
r : ℝ
z : ι → V
h0 : ∀ i ∈ t, 0 ≤ w i
h1 : Eq (α := ℝ) (∑ i ∈ t, w i) 1
i j : ι
hi : i ∈ t
hj : j ∈ t
hij : z i ≠ z j
hi0 : w i ≠ 0
hj0 : w j ≠ 0
hz : ∀ i ∈ t, Membership.mem (γ := Set V) (closedBall 0 r) (z i)
rw : Membership.mem (γ := Set V) (ball 0 r) (∑ k ∈ t, w k • z k)
⊢ norm.{u_2} (E := V) (∑ k ∈ t, w k • z k) < r

Tactic:
rw [← mem_ball_zero_iff]

Premises used: mem_ball_zero_iff