awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (hypothesis)
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 : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
hn : ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε / C
⊢ |(↑(u n) : ℝ)| * ‖y‖ < ε
have hn₁ : |(↑(u n) : ℝ)| * C < ε
Tactic: rw [lt_div_iff₀' hC_pos, mul_comm, NNReal.coe_zero, sub_zero, Real.norm_eq_abs] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
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 : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
hn : |(↑(u n) : ℝ)| * C < ε
⊢ |(↑(u n) : ℝ)| * ‖y‖ < ε
have h₁ : |(↑(u n) : ℝ)| * ‖y‖ ≤ |(↑(u n) : ℝ)| * C
Tactic: refine lt_of_le_of_lt ?_ hn
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
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 : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ‖(↑(u n) : ℝ) - (↑0 : ℝ)‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ (↑K : Set V), ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
y : V
hyK : y ∈ (↑K : Set V)
h : Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) ((1 + (↑(u n) : ℝ)) • y)
hn : |(↑(u n) : ℝ)| * C < ε
⊢ |(↑(u n) : ℝ)| * ‖y‖ ≤ |(↑(u n) : ℝ)| * C
have h₁ : ‖y‖ ≤ C
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Body (goal)
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)
⊢ Membership.mem (γ := Set V) (⋂ (n : ℕ), (1 + (↑(u n) : ℝ)) • (↑K : Set V)) x
have h₁ : ∀ (n : ℕ), 1 ≤ 1 + (↑(u n) : ℝ)
Tactic: refine Set.mem_iInter.mpr (fun n => Convex.mem_smul_of_zero_mem K.convex h_zero h ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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
⊢ ∃ (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
have 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
Tactic: simp only [Finset.convexHull_eq, mem_setOf_eq] at m ⊢
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨f, fpos, fsum, rfl⟩ := m
Cleared hypotheses: x, m
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨g, gcombo, gsum, gpos⟩ := exists_nontrivial_relation_sum_zero_of_not_affine_ind h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (hypothesis)
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
⊢ ∃ (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
have gpos₁ : ∃ i ∈ t, 0 < g i
Tactic: replace gpos := exists_pos_of_sum_zero_of_exists_nonzero g gsum gpos
Cleared hypotheses: gpos
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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₀ ∈ s, ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i
have apply : s.Nonempty
Tactic: apply s.exists_min_image fun z => f z / g z
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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}
⊢ s.Nonempty
have obtain : ∀ (x : E) (hx : x ∈ t) (hgx : 0 < g x), s.Nonempty
Tactic: obtain ⟨x, hx, hgx⟩ : ∃ x ∈ t, 0 < g x := gpos
Cleared hypotheses: gpos
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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}
⊢ ∃ (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
have 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
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⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (hypothesis)
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₀
have mem₁ : i₀ ∈ t ∧ 0 < g i₀
Tactic: rw [mem_filter] at mem
Cleared hypotheses: mem, w
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (hypothesis)
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
⊢ ∃ (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
have hg : 0 < g i₀
Tactic: have hg : 0 < g i₀ := by
    rw [mem_filter] at mem
    exact mem.2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (hypothesis)
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₀
⊢ ∃ (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
have hi₀ : i₀ ∈ t
Tactic: have hi₀ : i₀ ∈ t := filter_subset _ _ mem
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (hypothesis)
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
⊢ ∃ (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
have hk : k i₀ = 0
Tactic: have hk : k i₀ = 0 := by simp [k, ne_of_gt hg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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 ∈ t, k e
have rw : ∑ x ∈ t.erase i₀, k x
Tactic: rw [← insert_erase hi₀, sum_insert (notMem_erase i₀ t), hk, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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) (∑ e ∈ t, k e)
have conv_rhs : 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) (∑ e ∈ t, k e)
have conv_rhs₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) (∑ x ∈ t.erase i₀, k x)
Tactic: conv_rhs => rw [← insert_erase hi₀, sum_insert (notMem_erase i₀ t), hk, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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, (f e - f i₀ / g i₀ * g e)) 1
have rw : HSub.hSub (α := 𝕜) (∑ x ∈ t, f x) (∑ x ∈ t, f i₀ / g i₀ * g x) = 1
Tactic: rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, (f e - f i₀ / g i₀ * g e)) 1
have rw₁ : HSub.hSub (α := 𝕜) 1 (∑ x ∈ t, f i₀ / g i₀ * g x) = 1
Tactic: rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, (f e - f i₀ / g i₀ * g e)) 1
have rw₂ : 1 - f i₀ / g i₀ * ∑ i ∈ t, g i = 1
Tactic: rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, (f e - f i₀ / g i₀ * g e)) 1
have rw₃ : 1 - f i₀ / g i₀ * 0 = 1
Tactic: rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, (f e - f i₀ / g i₀ * g e)) 1
have rw₄ : HSub.hSub (α := 𝕜) 1 0 = 1
Tactic: rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, (f e - f i₀ / g i₀ * g e)) 1
have rw₅ : Eq.{u_1 + 1} (α := 𝕜) 1 1
Tactic: rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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
have e : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) (∑ e ∈ t, k e)
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (goal)
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)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t.erase i₀, k e) 1
have e₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ e ∈ t, (f e - f i₀ / g i₀ * g 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Caratheodory (hypothesis)
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
⊢ ∃ (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
have ksum : 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]