awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : x ∈ (↑K : Set V)
n : ℕ
⊢ 0 ≤ (↑(u n) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Body
Goal:
V : Type u_1
inst : SeminormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : x ∈ (↑K : Set V)
n : ℕ
⊢ 1 ≤ 1 + (↑(u n) : ℝ)

Tactic:
exact le_add_of_nonneg_right (by positivity)

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
h : ¬AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
x : E
m : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) x
simp :
  ∀ (m : ∃ (w : E → 𝕜), (∀ y ∈ t, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1 ∧ t.centerMass w id = x),
    ∃ (y : (↑(↑t : Set E) : Type u)) (w : E → 𝕜),
      (∀ y_1 ∈ t.erase (↑y : E), 0 ≤ w y_1) ∧
        Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t.erase (↑y : E), w y) 1 ∧ (t.erase (↑y : E)).centerMass w id = x
⊢ ∃ (y : (↑(↑t : Set E) : Type u)),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(t.erase (↑y : E)) : Set E) : Set E) x

Tactic:
simp only [Finset.convexHull_eq, mem_setOf_eq] at m ⊢

Premises used: Set.mem_setOf_eq, Finset.convexHull_eq
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
h : ¬AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
x : E
m : ∃ (w : E → 𝕜), (∀ y ∈ t, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, w y) 1 ∧ t.centerMass w id = x
obtain :
  ∀ (f : E → 𝕜) (fpos : ∀ y ∈ t, 0 ≤ f y) (fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1),
    ∃ (y : (↑(↑t : Set E) : Type u)) (w : E → 𝕜),
      (∀ y_1 ∈ t.erase (↑y : E), 0 ≤ w y_1) ∧
        Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t.erase (↑y : E), w y) 1 ∧ (t.erase (↑y : E)).centerMass w id = t.centerMass f id
⊢ ∃ (y : (↑(↑t : Set E) : Type u)) (w : E → 𝕜),
    (∀ y_1 ∈ t.erase (↑y : E), 0 ≤ w y_1) ∧
      Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t.erase (↑y : E), w y) 1 ∧ (t.erase (↑y : E)).centerMass w id = x

Tactic:
obtain ⟨f, fpos, fsum, rfl⟩ := m

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
h : ¬AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
obtain :
  ∀ (g : E → 𝕜) (gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0) (gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0)
    (gpos : ∃ x ∈ t, g x ≠ 0),
    ∃ (y : (↑(↑t : Set E) : Type u)) (w : E → 𝕜),
      (∀ y_1 ∈ t.erase (↑y : E), 0 ≤ w y_1) ∧
        Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t.erase (↑y : E), w y) 1 ∧ (t.erase (↑y : E)).centerMass w id = t.centerMass f id
⊢ ∃ (y : (↑(↑t : Set E) : Type u)) (w : E → 𝕜),
    (∀ y_1 ∈ t.erase (↑y : E), 0 ≤ w y_1) ∧
      Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t.erase (↑y : E), w y) 1 ∧ (t.erase (↑y : E)).centerMass w id = t.centerMass f id

Tactic:
obtain ⟨g, gcombo, gsum, gpos⟩ := exists_nontrivial_relation_sum_zero_of_not_affine_ind h

Premises used: exists_nontrivial_relation_sum_zero_of_not_affine_ind
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
h : ¬AffineIndependent 𝕜 (P := E) (ι := ↥t) (Subtype.val (p := fun (x : E) ↦ x ∈ t))
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ x ∈ t, g x ≠ 0
⊢ ∃ i ∈ t, 0 < g i

Tactic:
replace gpos := exists_pos_of_sum_zero_of_exists_nonzero g gsum gpos
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
apply : s.Nonempty
⊢ ∃ i₀ ∈ s, ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i

Tactic:
apply s.exists_min_image fun z => f z / g z

Premises used: HDiv.hDiv, Finset.exists_min_image
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
⊢ ∃ x ∈ t, 0 < g x

Tactic:
gpos
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
obtain : ∀ (x : E) (hx : x ∈ t) (hgx : 0 < g x), s.Nonempty
⊢ s.Nonempty

Tactic:
obtain ⟨x, hx, hgx⟩ : ∃ x ∈ t, 0 < g x := gpos
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
s : Finset E := {z ∈ t | 0 < g z}
x : E
hx : x ∈ t
hgx : 0 < g x
⊢ s.Nonempty

Tactic:
⟨x, mem_filter.mpr ⟨hx, hgx⟩⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Finset.Nonempty, Finset.mem_filter
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
s : Finset E := {z ∈ t | 0 < g z}
x : E
hx : x ∈ t
hgx : 0 < g x
⊢ s.Nonempty

Tactic:
exact ⟨x, mem_filter.mpr ⟨hx, hgx⟩⟩
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
obtain :
  ∀ (i₀ : E) (mem : i₀ ∈ s) (w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i),
    ∃ (y : (↑(↑t : Set E) : Type u)) (w : E → 𝕜),
      (∀ y_1 ∈ t.erase (↑y : E), 0 ≤ w y_1) ∧
        Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t.erase (↑y : E), w y) 1 ∧ (t.erase (↑y : E)).centerMass w id = t.centerMass f id
⊢ ∃ (y : (↑(↑t : Set E) : Type u)) (w : E → 𝕜),
    (∀ y_1 ∈ t.erase (↑y : E), 0 ≤ w y_1) ∧
      Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t.erase (↑y : E), w y) 1 ∧ (t.erase (↑y : E)).centerMass w id = t.centerMass f id

Tactic:
obtain ⟨i₀, mem, w⟩ : ∃ i₀ ∈ s, ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i := by
    apply s.exists_min_image fun z => f z / g z
    obtain ⟨x, hx, hgx⟩ : ∃ x ∈ t, 0 < g x := gpos
    exact ⟨x, mem_filter.mpr ⟨hx, hgx⟩⟩
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
⊢ i₀ ∈ t ∧ 0 < g i₀

Tactic:
rw [mem_filter] at mem

Premises used: Finset.mem_filter
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
mem₁ : i₀ ∈ t ∧ 0 < g i₀
⊢ ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i

Tactic:
rw [mem_filter] at mem

Premises used: Finset.mem_filter
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ t ∧ 0 < g i₀
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
⊢ 0 < g i₀

Tactic:
mem.2

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ t ∧ 0 < g i₀
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
⊢ 0 < g i₀

Tactic:
exact mem.2

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
⊢ 0 < g i₀

Tactic:
have hg : 0 < g i₀ := by
    rw [mem_filter] at mem
    exact mem.2
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
⊢ i₀ ∈ t

Tactic:
have hi₀ : i₀ ∈ t := filter_subset _ _ mem
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun (z : E) ↦ f z - f i₀ / g i₀ * g z
⊢ k i₀ = 0

Tactic:
simp [k, ne_of_gt hg]

Premises used: ne_of_gt
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun (z : E) ↦ f z - f i₀ / g i₀ * g z
⊢ k i₀ = 0

Tactic:
have hk : k i₀ = 0 := by simp [k, ne_of_gt hg]
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun (z : E) ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
rw : ∑ x ∈ t.erase i₀, k x
| ∑ e ∈ t, k e

Tactic:
rw [← insert_erase hi₀, sum_insert (notMem_erase i₀ t), hk, zero_add]

Premises used: zero_add, Finset.notMem_erase, Finset.sum_insert, Finset.insert_erase
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun (z : E) ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
conv_rhs : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) (∑ e ∈ t, k e)
conv_rhs₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) (∑ x ∈ t.erase i₀, k x)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) (∑ e ∈ t, k e)

Tactic:
conv_rhs => rw [← insert_erase hi₀, sum_insert (notMem_erase i₀ t), hk, zero_add]

Premises used: zero_add, Finset.notMem_erase, Finset.sum_insert, Finset.insert_erase
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun (z : E) ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, k e) (∑ e ∈ t, (f e - f i₀ / g i₀ * g e))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun (z : E) ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
rw : HSub.hSub (α := 𝕜) (∑ x ∈ t, f x) (∑ x ∈ t, f i₀ / g i₀ * g x) = 1
rw₁ : HSub.hSub (α := 𝕜) 1 (∑ x ∈ t, f i₀ / g i₀ * g x) = 1
rw₂ : 1 - f i₀ / g i₀ * ∑ i ∈ t, g i = 1
rw₃ : 1 - f i₀ / g i₀ * 0 = 1
rw₄ : HSub.hSub (α := 𝕜) 1 0 = 1
rw₅ rw₆ : Eq.{u_1 + 1} (α := 𝕜) 1 1
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, (f e - f i₀ / g i₀ * g e)) 1

Tactic:
rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]

Premises used: Finset.mul_sum, sub_zero, MulZeroClass.mul_zero, Finset.sum_sub_distrib
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun (z : E) ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
e : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) (∑ e ∈ t, k e)
e₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, (f e - f i₀ / g i₀ * g e)) 1
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) 1

Tactic:
calc
      ∑ e ∈ t.erase i₀, k e = ∑ e ∈ t, k e := by
        conv_rhs => rw [← insert_erase hi₀, sum_insert (notMem_erase i₀ t), hk, zero_add]
      _ = ∑ e ∈ t, (f e - f i₀ / g i₀ * g e) := rfl
      _ = 1 := by rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]

Premises used: Finset.erase, rfl
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun (z : E) ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) 1

Tactic:
have ksum : ∑ e ∈ t.erase i₀, k e = 1 := by
    calc
      ∑ e ∈ t.erase i₀, k e = ∑ e ∈ t, k e := by
        conv_rhs => rw [← insert_erase hi₀, sum_insert (notMem_erase i₀ t), hk, zero_add]
      _ = ∑ e ∈ t, (f e - f i₀ / g i₀ * g e) := rfl
      _ = 1 := by rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun (z : E) ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) 1
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) 1

Tactic:
ksum
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun (z : E) ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) 1
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t.erase (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (↑t : Set E)) i₀ hi₀) : E), k y) 1

Tactic:
convert! ksum
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun (z : E) ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) 1
refine_1 : ∀ y ∈ t.erase (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (↑t : Set E)) i₀ hi₀) : E), 0 ≤ k y
refine_2 :
  (t.erase (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (↑t : Set E)) i₀ hi₀) : E)).centerMass k id = t.centerMass f id
⊢ ∃ (y : (↑(↑t : Set E) : Type u)) (w : E → 𝕜),
    (∀ y_1 ∈ t.erase (↑y : E), 0 ≤ w y_1) ∧
      Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t.erase (↑y : E), w y) 1 ∧ (t.erase (↑y : E)).centerMass w id = t.centerMass f id

Tactic:
refine ⟨⟨i₀, hi₀⟩, k, ?_, by convert! ksum, ?_⟩
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun (z : E) ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) 1
refine_1 : ∀ (y : E), ¬y = i₀ → y ∈ t → f i₀ / g i₀ * g y ≤ f y
⊢ ∀ y ∈ t.erase (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (↑t : Set E)) i₀ hi₀) : E), 0 ≤ k y

Tactic:
simp only [k, and_imp, sub_nonneg, mem_erase, Ne]

Premises used: and_imp, Ne, Finset.mem_erase, sub_nonneg
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun (z : E) ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) 1
e : E
refine_1 : ¬e = i₀ → e ∈ t → f i₀ / g i₀ * g e ≤ f e
⊢ ¬e = i₀ → e ∈ t → f i₀ / g i₀ * g e ≤ f e

Tactic:
_
-- Module: Mathlib.Analysis.Convex.Caratheodory
Goal:
𝕜 : Type u_1
E : Type u
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : DecidableEq E
t : Finset E
f : E → 𝕜
fpos : ∀ y ∈ t, 0 ≤ f y
fsum : Eq.{u_1 + 1} (α := 𝕜) (∑ y ∈ t, f y) 1
g : E → 𝕜
gcombo : Eq (α := E) (∑ e ∈ t, g e • e) 0
gsum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, g e) 0
gpos : ∃ i ∈ t, 0 < g i
s : Finset E := {z ∈ t | 0 < g z}
i₀ : E
mem : i₀ ∈ s
w : ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
hg : 0 < g i₀
hi₀ : i₀ ∈ t
k : E → 𝕜 := fun (z : E) ↦ f z - f i₀ / g i₀ * g z
hk : k i₀ = 0
ksum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) 1
e : E
h : ¬e = i₀
het : e ∈ t
pos : ∀ (hes : e ∈ s), f i₀ / g i₀ * g e ≤ f e
neg : ∀ (hes : e ∉ s), f i₀ / g i₀ * g e ≤ f e
⊢ f i₀ / g i₀ * g e ≤ f e

Tactic:
by_cases hes : e ∈ s