awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x y : E
inst_5 : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
match_scalars : 1 = (1 - t) * 1 + t * 1
⊢ x + t • y = (1 - t) • x + t • (x + y)
have match_scalars₁ : t * 1 = t * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x y : E
inst_5 : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • y ∈ interior s
have h : x + t • y = (1 - t) • x + t • (x + y)
Tactic: have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x y : E
inst_5 : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ interior s
have rw : (1 - t) • x + t • (x + y) ∈ interior s
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x y : E
inst_5 : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h_1 : x + t • y = (1 - t) • x + t • (x + y)
h : x = x + y
⊢ x + y = x + 0
have rw : x = x + 0
Tactic: rw [← h, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x y : E
inst_5 : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h_1 : x + t • y = (1 - t) • x + t • (x + y)
h : x = x + y
rw : x = x + 0
⊢ x + y = x + 0
have rw₁ : x = x
Tactic: rw [← h, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x y : E
inst_5 : AddRightMono 𝕜
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ interior s
have a : x + t • (y - x) ∈ openSegment 𝕜 x y
Tactic: apply h.openSegment_subset hx hy hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x y : E
inst_5 : AddRightMono 𝕜
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ openSegment 𝕜 x y
have a : Membership.mem (γ := Set E) ((fun (θ : 𝕜) ↦ x + θ • (y - x)) '' Ioo 0 1) (x + t • (y - x))
Tactic: rw [openSegment_eq_image']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
s : Set F
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : Continuous.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F)
hfinj : Injective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
x : E
hx : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ Membership.mem (γ := Set E) (interior ((⇑f : (a : E) → F) ⁻¹' s)) (a • x + b • y)
have refine : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' interior s) (a • x + b • y)
Tactic: refine preimage_interior_subset_interior_preimage hf ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
s : Set F
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : Continuous.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F)
hfinj : Injective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
x : E
hx : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' interior s) (a • x + b • y)
have rw : HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F) ∈ interior s
Tactic: rw [mem_preimage, Convex.combo_affine_apply hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
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
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s
have h₁ : a = a / (a + b)
Tactic: convert! h hx hy hxy ha hb
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
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
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h₁ : a = a / (a + b)
⊢ a • x + b • y ∈ interior s
have h₂ : b = b / (a + b)
Tactic: convert! h hx hy hxy ha hb
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
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
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a = a / (a + b)
have h₁ : a = a / 1
Tactic: rw [hab, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
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
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h₁ : a = a / 1
⊢ a = a / (a + b)
have h₂ : a = a
Tactic: rw [hab, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
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
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ b = b / (a + b)
have h₁ : b = b / 1
Tactic: rw [hab, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
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
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h₁ : b = b / 1
⊢ b = b / (a + b)
have h₂ : b = b
Tactic: rw [hab, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
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
⊢ x ∈ t • interior s
have rw : t⁻¹ • x ∈ interior s
Tactic: rw [mem_smul_set_iff_inv_smul_mem₀ (by positivity)]
-- 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 : 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
⊢ (insert i t).centerMass w z ∈ interior s
have zi : z i ∈ s
Tactic: have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
-- 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 : 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
⊢ (insert i t).centerMass w z ∈ interior 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.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 : 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
⊢ (insert i t).centerMass w z ∈ interior s
have pos : ∀ (hsum_t : Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0), (insert i t).centerMass w z ∈ interior s
Tactic: by_cases hsum_t : ∑ j ∈ t, 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 : 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
⊢ (insert i t).centerMass w z ∈ interior s
have neg : ∀ (hsum_t : ¬Eq.{u_1 + 1} (α := R) (∑ j ∈ t, w j) 0), (insert i t).centerMass w z ∈ interior s
Tactic: by_cases hsum_t : ∑ j ∈ t, w j = 0
-- 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 : 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
⊢ (insert i t).centerMass w z ∈ interior 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.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 : 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
⊢ (insert i t).centerMass w z ∈ interior s
have h : i' ∈ t ∨ j' ∈ t
Tactic: have h : i' ∈ t ∨ j' ∈ t := 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 : 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
⊢ (insert i t).centerMass w z ∈ interior s
have pos : 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 : 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
⊢ False
have pos : ∀ (h : i' ∈ t), False
Tactic: rcases h with h | h
Cleared hypotheses: h
-- 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 : 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
⊢ False
have pos₁ : ∀ (h : j' ∈ t), False
Tactic: rcases h with h | h
Cleared hypotheses: h
-- 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 : 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
⊢ (insert i t).centerMass w z ∈ interior 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 ∈ interior s
Tactic: rw [Finset.centerMass_insert _ _ _ hi 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 : 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
⊢ (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 : ∀ (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
Tactic: by_cases hi : w i = 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 : 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
⊢ (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 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
Tactic: by_cases hi : w i = 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
⊢ (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 [hi, zero_add, zero_div, zero_smul, ne_eq, hsum_t, 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
⊢ (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 : ∀ (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: by_cases hzi : z i = t.centerMass w z
-- 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
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
⊢ (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 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
Tactic: by_cases hzi : z i = t.centerMass w z
-- 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
⊢ w i + ∑ j ∈ t, w j ≠ 0
have refine : 0 < w i + ∑ j ∈ t, w j
Tactic: refine LT.lt.ne' ?_