awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hes : e ∈ s
⊢ e ∈ t ∧ 0 < g e

Tactic:
rw [mem_filter] at hes

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
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
hes : e ∈ t ∧ 0 < g e
⊢ 0 < g e

Tactic:
hes.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
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
hes : e ∈ t ∧ 0 < g e
⊢ 0 < g e

Tactic:
exact hes.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
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
hes : e ∈ s
⊢ 0 < g e

Tactic:
have hge : 0 < g e := by
        rw [mem_filter] at hes
        exact hes.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₀
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
hes : e ∈ s
hge : 0 < g e
pos : f i₀ / g i₀ ≤ f e / g e
⊢ f i₀ / g i₀ * g e ≤ f e

Tactic:
rw [← le_div_iff₀ hge]

Premises used: le_div_iff₀
-- 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
hes : e ∈ s
hge : 0 < g e
⊢ f i₀ / g i₀ ≤ f e / g e

Tactic:
w _ hes
-- 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
hes : e ∈ s
hge : 0 < g e
⊢ f i₀ / g i₀ ≤ f e / g e

Tactic:
exact w _ hes
-- 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
hes : e ∉ s
ha : 0 ≤ f i₀ / g i₀
hb : g e ≤ 0
⊢ f i₀ / g i₀ * g e ≤ 0

Tactic:
apply mul_nonpos_of_nonneg_of_nonpos

Premises used: mul_nonpos_of_nonneg_of_nonpos
-- 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
hes : e ∉ s
⊢ 0 ≤ f i₀ / g i₀

Tactic:
apply div_nonneg (fpos i₀ (mem_of_subset (filter_subset _ t) mem)) (le_of_lt hg)

Premises used: le_of_lt, Finset.filter_subset, div_nonneg, Finset.mem_of_subset
-- 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
hes : e ∉ s
⊢ g e ≤ 0

Tactic:
simpa only [s, mem_filter, het, true_and, not_lt] using hes

Premises used: not_lt, Finset.mem_filter, true_and
-- 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
hes : e ∉ s
⊢ 0 ≤ f e

Tactic:
fpos e het
-- 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
hes : e ∉ s
_ : f i₀ / g i₀ * g e ≤ 0
⊢ f i₀ / g i₀ * g e ≤ f e

Tactic:
calc
        _ ≤ 0 := by
          apply mul_nonpos_of_nonneg_of_nonpos
          · apply div_nonneg (fpos i₀ (mem_of_subset (filter_subset _ t) mem)) (le_of_lt hg)
          · simpa only [s, mem_filter, het, true_and, not_lt] using hes
        _ ≤ f e := fpos e het
-- 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_2 : ∑ i ∈ t.erase i₀, k i • id i = t.centerMass f id
⊢ (t.erase (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ (↑t : Set E)) i₀ hi₀) : E)).centerMass k id = t.centerMass f id

Tactic:
rw [Subtype.coe_mk, centerMass_eq_of_sum_1 _ id ksum]

Premises used: Subtype.coe_mk, id, Finset.centerMass_eq_of_sum_1
-- 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
rw : HSMul.hSMul.{u_1, u, u} (α := 𝕜) 0 i₀ = 0
rw₁ rw₂ : Eq.{u + 1} (α := E) 0 0
⊢ k i₀ • i₀ = 0

Tactic:
rw [hk, zero_smul]

Premises used: zero_smul
-- 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 (α := E) (∑ e ∈ t, k e • e) (∑ e ∈ t, (f e - f i₀ / g i₀ * g e) • 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
ksum : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) 1
⊢ ∑ e ∈ t, (f e - f i₀ / g i₀ * g e) • e = t.centerMass f id

Tactic:
simp only [sub_smul, mul_smul, sum_sub_distrib, ← smul_sum, gcombo, smul_zero, sub_zero,
          centerMass, fsum, inv_one, one_smul, id]

Premises used: inv_one, sub_zero, sub_smul, smul_zero, id, one_smul, Finset.sum_sub_distrib, Finset.smul_sum, Finset.centerMass, SemigroupAction.mul_smul
-- 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 ∈ t, (f e - f i₀ / g i₀ * g e) • e = t.centerMass f id
⊢ ∑ i ∈ t.erase i₀, k i • id i = t.centerMass f id

Tactic:
calc
      ∑ e ∈ t.erase i₀, k e • e = ∑ e ∈ t, k e • e := sum_erase _ (by rw [hk, zero_smul])
      _ = ∑ e ∈ t, (f e - f i₀ / g i₀ * g e) • e := rfl
      _ = t.centerMass f id := by
        simp only [sub_smul, mul_smul, sum_sub_distrib, ← smul_sum, gcombo, smul_zero, sub_zero,
          centerMass, fsum, inv_one, one_smul, id]

Premises used: id, Finset.centerMass, Finset.sum_erase, 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
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
⊢ Set.Nonempty.{u} (α := Finset E)
    {t : Finset E |
      (↑t : Set E) ⊆ s ∧ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) x}

Tactic:
simpa only [convexHull_eq_union_convexHull_finite_subsets s, exists_prop, mem_iUnion] using hx

Premises used: Set.mem_iUnion, exists_prop, convexHull_eq_union_convexHull_finite_subsets
-- 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
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
⊢ (↑(minCardFinsetOfMemConvexHull (s := s) hx) : Set E) ⊆ s

Tactic:
(Function.argminOn_mem _ { t : Finset E | ↑t ⊆ s ∧ x ∈ convexHull 𝕜 (t : Set E) } _).1

Premises used: setOf, Membership.mem, HasSubset.Subset, Function.argminOn_mem, And, convexHull, SetLike.coe, And.left, DFunLike.coe
-- 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
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
⊢ Membership.mem (γ := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑(minCardFinsetOfMemConvexHull (s := s) hx) : Set E) : Set E) x

Tactic:
(Function.argminOn_mem _ { t : Finset E | ↑t ⊆ s ∧ x ∈ convexHull 𝕜 (t : Set E) } _).2

Premises used: Set.Mem, setOf, Membership.mem, HasSubset.Subset, Function.argminOn_mem, And, convexHull, SetLike.coe, And.right, DFunLike.coe
-- 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
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
rw :
  Set.Nonempty.{u} (α := E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(minCardFinsetOfMemConvexHull (s := s) hx) : Set E))
⊢ (minCardFinsetOfMemConvexHull (s := s) hx).Nonempty

Tactic:
rw [← Finset.coe_nonempty, ← @convexHull_nonempty_iff 𝕜]

Premises used: Finset.coe_nonempty, convexHull_nonempty_iff
-- 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
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
⊢ Set.Nonempty.{u} (α := E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(minCardFinsetOfMemConvexHull (s := s) hx) : Set E))

Tactic:
⟨x, mem_minCardFinsetOfMemConvexHull hx⟩

Premises used: Caratheodory.mem_minCardFinsetOfMemConvexHull, Set.Nonempty, Exists.intro
-- 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
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
⊢ Set.Nonempty.{u} (α := E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑(minCardFinsetOfMemConvexHull (s := s) hx) : Set E))

Tactic:
exact ⟨x, mem_minCardFinsetOfMemConvexHull hx⟩
-- 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
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
t : Finset E
ht₁ : (↑t : Set E) ⊆ s
ht₂ : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) x
⊢ Membership.mem (γ := Set (Finset E))
    {t : Finset E |
      (↑t : Set E) ⊆ s ∧ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) x}
    t

Tactic:
⟨ht₁, ht₂⟩

Premises used: Set.Mem, setOf, And.intro
-- 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
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
t : Finset E
ht₁ : (↑t : Set E) ⊆ s
ht₂ : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) x
⊢ Membership.mem (γ := Set (Finset E))
    {t : Finset E |
      (↑t : Set E) ⊆ s ∧ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (↑t : Set E) : Set E) x}
    t

Tactic:
exact ⟨ht₁, ht₂⟩
-- 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
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
k : ℕ := #(minCardFinsetOfMemConvexHull (s := s) hx) - 1
⊢ #(minCardFinsetOfMemConvexHull (s := s) hx) = k + 1

Tactic:
have hk : #(minCardFinsetOfMemConvexHull hx) = k + 1 :=
    (Nat.succ_pred_eq_of_pos (Finset.card_pos.mpr (minCardFinsetOfMemConvexHull_nonempty hx))).symm
-- 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
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
k : ℕ := #(minCardFinsetOfMemConvexHull (s := s) hx) - 1
hk : #(minCardFinsetOfMemConvexHull (s := s) hx) = k + 1
by_contra :
  ∀
    (h :
      ¬AffineIndependent 𝕜 (P := E) (ι := ↥(minCardFinsetOfMemConvexHull (s := s) hx))
          (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ minCardFinsetOfMemConvexHull (s := s) hx))),
    False
⊢ AffineIndependent 𝕜 (P := E) (ι := ↥(minCardFinsetOfMemConvexHull (s := s) hx))
    (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ minCardFinsetOfMemConvexHull (s := s) hx))

Tactic:
by_contra h
-- 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
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
k : ℕ := #(minCardFinsetOfMemConvexHull (s := s) hx) - 1
hk : #(minCardFinsetOfMemConvexHull (s := s) hx) = k + 1
h :
  ¬AffineIndependent 𝕜 (P := E) (ι := ↥(minCardFinsetOfMemConvexHull (s := s) hx))
      (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ minCardFinsetOfMemConvexHull (s := s) hx))
obtain :
  ∀ (p : (↑(↑(minCardFinsetOfMemConvexHull (s := s) hx) : Set E) : Type u))
    (hp :
      Membership.mem (γ := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) (↑((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E)) : Set E) :
          Set E)
        x),
    False
⊢ False

Tactic:
obtain ⟨p, hp⟩ := mem_convexHull_erase h (mem_minCardFinsetOfMemConvexHull hx)

Premises used: Caratheodory.mem_minCardFinsetOfMemConvexHull, Caratheodory.mem_convexHull_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
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
k : ℕ := #(minCardFinsetOfMemConvexHull (s := s) hx) - 1
hk : #(minCardFinsetOfMemConvexHull (s := s) hx) = k + 1
h :
  ¬AffineIndependent 𝕜 (P := E) (ι := ↥(minCardFinsetOfMemConvexHull (s := s) hx))
      (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ minCardFinsetOfMemConvexHull (s := s) hx))
p : (↑(↑(minCardFinsetOfMemConvexHull (s := s) hx) : Set E) : Type u)
hp :
  Membership.mem (γ := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E)) : Set E) :
      Set E)
    x
⊢ #(minCardFinsetOfMemConvexHull (s := s) hx) ≤ #((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E))

Tactic:
have contra := minCardFinsetOfMemConvexHull_card_le_card hx (Set.Subset.trans
    (Finset.erase_subset (p : E) (minCardFinsetOfMemConvexHull hx))
    (minCardFinsetOfMemConvexHull_subseteq hx)) hp
-- 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
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x
k : ℕ := #(minCardFinsetOfMemConvexHull (s := s) hx) - 1
hk : #(minCardFinsetOfMemConvexHull (s := s) hx) = k + 1
h :
  ¬AffineIndependent 𝕜 (P := E) (ι := ↥(minCardFinsetOfMemConvexHull (s := s) hx))
      (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ minCardFinsetOfMemConvexHull (s := s) hx))
p : (↑(↑(minCardFinsetOfMemConvexHull (s := s) hx) : Set E) : Type u)
hp :
  Membership.mem (γ := Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (↑((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E)) : Set E) :
      Set E)
    x
contra : #(minCardFinsetOfMemConvexHull (s := s) hx) ≤ #((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E))
⊢ ¬#((minCardFinsetOfMemConvexHull (s := s) hx).erase (↑p : E)) < #(minCardFinsetOfMemConvexHull (s := s) hx)

Tactic:
rw [← not_lt] at contra

Premises used: not_lt