awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht : 1 < t
⊢ 0 < t⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht : 1 < t
⊢ t⁻¹ • x ∈ interior s

Tactic:
exact hs.smul_mem_of_zero_mem zero_mem hx hx₀ (by positivity) (inv_lt_one_of_one_lt₀ ht)

Premises used: inv_lt_one_of_one_lt₀, StrictConvex.smul_mem_of_zero_mem
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
⊢ StrictConvex 𝕜 s ↔ Convex 𝕜 s

Tactic:
⟨StrictConvex.convex, fun hs => hs.ordConnected.strictConvex⟩

Premises used: Iff.intro, Convex.ordConnected, StrictConvex.convex, Set.OrdConnected.strictConvex
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
⊢ StrictConvex 𝕜 s ↔ s.OrdConnected

Tactic:
strictConvex_iff_convex.trans convex_iff_ordConnected

Premises used: convex_iff_ordConnected, strictConvex_iff_convex, Iff.trans
-- 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 : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ w i) →
    ∀ (i j : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        Membership.mem (γ := Finset ι) ∅ j →
          z i ≠ z j →
            w i ≠ 0 →
              w j ≠ 0 → (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → z i ∈ s) → centerMass ∅ w z ∈ interior s

Tactic:
simp
-- 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 : 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
⊢ z i ∈ s

Tactic:
have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
-- 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 : 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
⊢ ∀ j ∈ t, 0 ≤ w j

Tactic:
have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
-- 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 : 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
pos : ∀ (hsum_t : Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0), (insert i t).centerMass w z ∈ interior s
neg : ∀ (hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0), (insert i t).centerMass w z ∈ interior s
⊢ (insert i t).centerMass w z ∈ interior s

Tactic:
by_cases hsum_t : ∑ j ∈ t, 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 : 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
⊢ ∀ j ∈ t, w j = 0

Tactic:
have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 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 : 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
ws : ∀ j ∈ t, w j = 0
⊢ i' ∈ t ∨ j' ∈ t

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 : 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
ws : ∀ j ∈ t, w j = 0
⊢ i' ∈ t ∨ j' ∈ t

Tactic:
have h : i' ∈ t ∨ j' ∈ t := 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 : 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
ws : ∀ j ∈ t, w j = 0
h : i' ∈ t ∨ j' ∈ t
pos : False
⊢ (insert i 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 : 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
ws : ∀ j ∈ t, w j = 0
h : i' ∈ t ∨ j' ∈ t
pos : ∀ (h : i' ∈ t), False
pos₁ : ∀ (h : j' ∈ t), False
⊢ False

Tactic:
rcases h with h | h
-- 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 : 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
ws : ∀ j ∈ t, w j = 0
h : i' ∈ t
⊢ False

Tactic:
hi'0 (ws _ h)
-- 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 : 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
ws : ∀ j ∈ t, w j = 0
h : i' ∈ t
⊢ False

Tactic:
exact hi'0 (ws _ h)
-- 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 : 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
ws : ∀ j ∈ t, w j = 0
h : j' ∈ t
⊢ False

Tactic:
hj'0 (ws _ h)
-- 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 : 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
ws : ∀ j ∈ t, w j = 0
h : j' ∈ t
⊢ False

Tactic:
exact hj'0 (ws _ h)
-- 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 : 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
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 ∈ interior s
⊢ (insert i t).centerMass w z ∈ interior s

Tactic:
rw [Finset.centerMass_insert _ _ _ hi hsum_t]

Premises used: Finset.centerMass_insert
-- 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 : 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
pos :
  ∀ (hi : w i = 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 ∈ interior s
neg :
  ∀ (hi : ¬w i = 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 ∈ 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:
by_cases hi : w i = 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
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 [hi, zero_add, zero_div, zero_smul, ne_eq, hsum_t, not_false_eq_true, div_self,
        one_smul]

Premises used: zero_div, zero_add, ne_eq, one_smul, zero_smul, not_false_eq_true, div_self
-- 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
⊢ 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
pos :
  ∀ (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
neg :
  ∀ (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
⊢ (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:
by_cases hzi : z i = t.centerMass w z

Premises used: Finset.centerMass
-- 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:
LT.lt.ne' ?_

Premises used: LT.lt.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
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
refine : 0 < w i + ∑ j ∈ t, w j
⊢ w i + ∑ j ∈ t, w j ≠ 0

Tactic:
refine LT.lt.ne' ?_

Premises used: LT.lt.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
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
⊢ 0 < w i

Tactic:
have hwi : 0 < w i := 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 : 0 < w i
grw : w i < w i + ∑ j ∈ t, w j
⊢ 0 < w i + ∑ j ∈ t, w j

Tactic:
grw [hwi]
-- 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 : 0 < w i
simp : LT.lt.{u_1} (α := R) 0 (∑ j ∈ t, w j)
⊢ w i < w i + ∑ j ∈ t, w j

Tactic:
simp only [lt_add_iff_pos_right, gt_iff_lt]

Premises used: lt_add_iff_pos_right, gt_iff_lt
-- 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 : 0 < w i
⊢ LT.lt.{u_1} (α := R) 0 (∑ j ∈ t, w j)

Tactic:
(sum_nonneg hs₀).lt_of_ne' hsum_t

Premises used: Finset.sum_nonneg, LE.le.lt_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
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 : 0 < w i
⊢ LT.lt.{u_1} (α := R) 0 (∑ j ∈ t, w j)

Tactic:
exact (sum_nonneg hs₀).lt_of_ne' hsum_t

Premises used: Finset.sum_nonneg, LE.le.lt_of_ne'