awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (hypothesis)
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 + ∑ j ∈ t, w j
have hwi : 0 < w i
Tactic: have hwi : 0 < w i := by grind
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ 0 < w i + ∑ j ∈ t, w j
have grw : w i < w i + ∑ j ∈ t, w j
Tactic: grw [hwi]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ w i < w i + ∑ j ∈ t, w j
have simp : LT.lt.{u_1} (α := R) 0 (∑ j ∈ t, w j)
Tactic: simp only [lt_add_iff_pos_right, gt_iff_lt]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (hypothesis)
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
have hwi : 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ (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
have pos : 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ t.centerMass w z ∈ interior s
have pos : ∀ (hijt : ∃ (i'' : ι) (j'' : ι), i'' ∈ t ∧ j'' ∈ t ∧ z i'' ≠ z j'' ∧ w i'' ≠ 0 ∧ w j'' ≠ 0),
  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
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ t.centerMass w z ∈ interior s
have neg : ∀ (hijt : ∀ (i'' j'' : ι) (_ : i'' ∈ t) (_ : j'' ∈ t) (_ : z i'' ≠ z j'') (_ : w i'' ≠ 0), w j'' = 0),
  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
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ False
have neg : ∀ (i'' : ι) (hi'' : i'' ∈ t) (hwi'' : w i'' ≠ 0), False
Tactic: obtain ⟨i'', hi'', hwi''⟩ : ∃ i'' ∈ t, w i'' ≠ 0 := by grind
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (hypothesis)
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
⊢ False
have hijt' : ∀ 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (hypothesis)
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''
⊢ False
have hi₁ : i = i' ∨ i = j'
Tactic: have hi : i = i' ∨ i = j' := by grind
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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''
have rw : t.centerMass w (Function.const ι (z i'')) = z i''
Tactic: rw [t.centerMass_congr_fun hijt', t.centerMass_const hsum_t]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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''
⊢ t.centerMass w z = z i''
have rw₁ : z i'' = z i''
Tactic: rw [t.centerMass_congr_fun hijt', t.centerMass_const hsum_t]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (hypothesis)
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'
⊢ False
have hzi'' : 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ (∀ 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
have empty : (∀ (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: induction t using Finset.induction with
  | empty => simp
  | insert i t hi ht =>
    intro h₀ i' j' hi' hj' hi'j' hi'0 hj'0 hmem
    have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
    have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
    by_cases hsum_t : ∑ j ∈ t, w j = 0
    · have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
      have h : i' ∈ t ∨ j' ∈ t := by grind
      exfalso
      rcases h with h | h
      · exact hi'0 (ws _ h)
      · exact hj'0 (ws _ h)
    rw [Finset.centerMass_insert _ _ _ hi hsum_t]
    by_cases hi : w i = 0
    · simp only [hi, zero_add, zero_div, zero_smul, ne_eq, hsum_t, not_false_eq_true, div_self,
        one_smul]
      grind
    by_cases hzi : z i = t.centerMass w z
    · 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
      simp only [hzi, ← add_smul, ← add_div, ne_eq, hwi, not_false_eq_true, div_self, one_smul]
      by_cases! hijt : ∃ i'' j'', i'' ∈ t ∧ j'' ∈ t ∧ z i'' ≠ z j'' ∧ w i'' ≠ 0 ∧ w j'' ≠ 0
      · grind
      · exfalso
        obtain ⟨i'', hi'', hwi''⟩ : ∃ i'' ∈ t, w i'' ≠ 0 := by grind
        have hijt' : ∀ j'', j'' ∈ t → w j'' ≠ 0 → z j'' = Function.const _ (z i'') j'' := by
          grind
        have hi : i = i' ∨ i = j' := by grind
        have hzi'' : t.centerMass w z = z i'' := by
          rw [t.centerMass_congr_fun hijt', t.centerMass_const hsum_t]
        grind
    · 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)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
empty :
  (∀ (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
⊢ (∀ 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
have insert : ∀ (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),
  (∀ i_1 ∈ insert i t, 0 ≤ w i_1) →
    ∀ (i_1 j : ι),
      i_1 ∈ insert i t →
        j ∈ insert i t →
          z i_1 ≠ z j → w i_1 ≠ 0 → w j ≠ 0 → (∀ i_2 ∈ insert i t, z i_2 ∈ s) → (insert i t).centerMass w z ∈ interior s
Tactic: induction t using Finset.induction with
  | empty => simp
  | insert i t hi ht =>
    intro h₀ i' j' hi' hj' hi'j' hi'0 hj'0 hmem
    have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
    have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
    by_cases hsum_t : ∑ j ∈ t, w j = 0
    · have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
      have h : i' ∈ t ∨ j' ∈ t := by grind
      exfalso
      rcases h with h | h
      · exact hi'0 (ws _ h)
      · exact hj'0 (ws _ h)
    rw [Finset.centerMass_insert _ _ _ hi hsum_t]
    by_cases hi : w i = 0
    · simp only [hi, zero_add, zero_div, zero_smul, ne_eq, hsum_t, not_false_eq_true, div_self,
        one_smul]
      grind
    by_cases hzi : z i = t.centerMass w z
    · 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
      simp only [hzi, ← add_smul, ← add_div, ne_eq, hwi, not_false_eq_true, div_self, one_smul]
      by_cases! hijt : ∃ i'' j'', i'' ∈ t ∧ j'' ∈ t ∧ z i'' ≠ z j'' ∧ w i'' ≠ 0 ∧ w j'' ≠ 0
      · grind
      · exfalso
        obtain ⟨i'', hi'', hwi''⟩ : ∃ i'' ∈ t, w i'' ≠ 0 := by grind
        have hijt' : ∀ j'', j'' ∈ t → w j'' ≠ 0 → z j'' = Function.const _ (z i'') j'' := by
          grind
        have hi : i = i' ∨ i = j' := by grind
        have hzi'' : t.centerMass w z = z i'' := by
          rw [t.centerMass_congr_fun hijt', t.centerMass_const hsum_t]
        grind
    · 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)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictCombination (goal)
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
⊢ (∀ 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
have empty : (∀ (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: classical
  induction t using Finset.induction with
  | empty => simp
  | insert i t hi ht =>
    intro h₀ i' j' hi' hj' hi'j' hi'0 hj'0 hmem
    have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
    have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
    by_cases hsum_t : ∑ j ∈ t, w j = 0
    · have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
      have h : i' ∈ t ∨ j' ∈ t := by grind
      exfalso
      rcases h with h | h
      · exact hi'0 (ws _ h)
      · exact hj'0 (ws _ h)
    rw [Finset.centerMass_insert _ _ _ hi hsum_t]
    by_cases hi : w i = 0
    · simp only [hi, zero_add, zero_div, zero_smul, ne_eq, hsum_t, not_false_eq_true, div_self,
        one_smul]
      grind
    by_cases hzi : z i = t.centerMass w z
    · 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
      simp only [hzi, ← add_smul, ← add_div, ne_eq, hwi, not_false_eq_true, div_self, one_smul]
      by_cases! hijt : ∃ i'' j'', i'' ∈ t ∧ j'' ∈ t ∧ z i'' ≠ z j'' ∧ w i'' ≠ 0 ∧ w j'' ≠ 0
      · grind
      · exfalso
        obtain ⟨i'', hi'', hwi''⟩ : ∃ i'' ∈ t, w i'' ≠ 0 := by grind
        have hijt' : ∀ j'', j'' ∈ t → w j'' ≠ 0 → z j'' = Function.const _ (z i'') j'' := by
          grind
        have hi : i = i' ∨ i = j' := by grind
        have hzi'' : t.centerMass w z = z i'' := by
          rw [t.centerMass_congr_fun hijt', t.centerMass_const hsum_t]
        grind
    · 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)
Cleared hypotheses: t