awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
⊢ (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
have empty : (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ w i) →
  LT.lt.{u_1} (α := R) 0 (∑ i ∈ ∅, w i) →
    (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → z i ∈ s) → centerMass ∅ w z ∈ s
Tactic: induction t using Finset.induction with
  | empty => simp
  | insert i t hi ht =>
    intro h₀ hpos hmem
    have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
    have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
    rw [sum_insert hi] at hpos
    by_cases hsum_t : ∑ j ∈ t, w j = 0
    · have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
      have wz : ∑ j ∈ t, w j • z j = 0 := sum_eq_zero fun i hi => by simp [ws i hi]
      simp only [centerMass, sum_insert hi, wz, hsum_t, add_zero]
      simp only [hsum_t, add_zero] at hpos
      rw [← mul_smul, inv_mul_cancel₀ (ne_of_gt hpos), one_smul]
      exact zi
    · rw [Finset.centerMass_insert _ _ _ hi hsum_t]
      refine convex_iff_div.1 hs zi (ht hs₀ ?_ ?_) ?_ (sum_nonneg hs₀) hpos
      · exact lt_of_le_of_ne (sum_nonneg hs₀) (Ne.symm hsum_t)
      · intro j hj
        exact hmem j (mem_insert_of_mem hj)
      · exact h₀ _ (mem_insert_self _ _)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
empty :
  (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ w i) →
    LT.lt.{u_1} (α := R) 0 (∑ i ∈ ∅, w i) →
      (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → z i ∈ s) → centerMass ∅ w z ∈ s
⊢ (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
have insert : ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
  (ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s),
  (∀ i_1 ∈ insert i t, 0 ≤ w i_1) →
    LT.lt.{u_1} (α := R) 0 (∑ i ∈ insert i t, w i) → (∀ i_1 ∈ insert i t, z i_1 ∈ s) → (insert i t).centerMass w z ∈ s
Tactic: induction t using Finset.induction with
  | empty => simp
  | insert i t hi ht =>
    intro h₀ hpos hmem
    have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
    have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
    rw [sum_insert hi] at hpos
    by_cases hsum_t : ∑ j ∈ t, w j = 0
    · have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
      have wz : ∑ j ∈ t, w j • z j = 0 := sum_eq_zero fun i hi => by simp [ws i hi]
      simp only [centerMass, sum_insert hi, wz, hsum_t, add_zero]
      simp only [hsum_t, add_zero] at hpos
      rw [← mul_smul, inv_mul_cancel₀ (ne_of_gt hpos), one_smul]
      exact zi
    · rw [Finset.centerMass_insert _ _ _ hi hsum_t]
      refine convex_iff_div.1 hs zi (ht hs₀ ?_ ?_) ?_ (sum_nonneg hs₀) hpos
      · exact lt_of_le_of_ne (sum_nonneg hs₀) (Ne.symm hsum_t)
      · intro j hj
        exact hmem j (mem_insert_of_mem hj)
      · exact h₀ _ (mem_insert_self _ _)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
⊢ (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
have empty : (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ w i) →
  LT.lt.{u_1} (α := R) 0 (∑ i ∈ ∅, w i) →
    (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → z i ∈ s) → centerMass ∅ w z ∈ s
Tactic: classical
  induction t using Finset.induction with
  | empty => simp
  | insert i t hi ht =>
    intro h₀ hpos hmem
    have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
    have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
    rw [sum_insert hi] at hpos
    by_cases hsum_t : ∑ j ∈ t, w j = 0
    · have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
      have wz : ∑ j ∈ t, w j • z j = 0 := sum_eq_zero fun i hi => by simp [ws i hi]
      simp only [centerMass, sum_insert hi, wz, hsum_t, add_zero]
      simp only [hsum_t, add_zero] at hpos
      rw [← mul_smul, inv_mul_cancel₀ (ne_of_gt hpos), one_smul]
      exact zi
    · rw [Finset.centerMass_insert _ _ _ hi hsum_t]
      refine convex_iff_div.1 hs zi (ht hs₀ ?_ ?_) ?_ (sum_nonneg hs₀) hpos
      · exact lt_of_le_of_ne (sum_nonneg hs₀) (Ne.symm hsum_t)
      · intro j hj
        exact hmem j (mem_insert_of_mem hj)
      · exact h₀ _ (mem_insert_self _ _)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
ι : Type u_5
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
t : Finset ι
w : ι → R
z : ι → E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
hs : Convex R s
empty :
  (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ w i) →
    LT.lt.{u_1} (α := R) 0 (∑ i ∈ ∅, w i) →
      (∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → z i ∈ s) → centerMass ∅ w z ∈ s
⊢ (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s
have insert : ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
  (ht : (∀ i ∈ t, 0 ≤ w i) → LT.lt.{u_1} (α := R) 0 (∑ i ∈ t, w i) → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ s),
  (∀ i_1 ∈ insert i t, 0 ≤ w i_1) →
    LT.lt.{u_1} (α := R) 0 (∑ i ∈ insert i t, w i) → (∀ i_1 ∈ insert i t, z i_1 ∈ s) → (insert i t).centerMass w z ∈ s
Tactic: classical
  induction t using Finset.induction with
  | empty => simp
  | insert i t hi ht =>
    intro h₀ hpos hmem
    have zi : z i ∈ s := hmem _ (mem_insert_self _ _)
    have hs₀ : ∀ j ∈ t, 0 ≤ w j := fun j hj => h₀ j <| mem_insert_of_mem hj
    rw [sum_insert hi] at hpos
    by_cases hsum_t : ∑ j ∈ t, w j = 0
    · have ws : ∀ j ∈ t, w j = 0 := (sum_eq_zero_iff_of_nonneg hs₀).1 hsum_t
      have wz : ∑ j ∈ t, w j • z j = 0 := sum_eq_zero fun i hi => by simp [ws i hi]
      simp only [centerMass, sum_insert hi, wz, hsum_t, add_zero]
      simp only [hsum_t, add_zero] at hpos
      rw [← mul_smul, inv_mul_cancel₀ (ne_of_gt hpos), one_smul]
      exact zi
    · rw [Finset.centerMass_insert _ _ _ hi hsum_t]
      refine convex_iff_div.1 hs zi (ht hs₀ ?_ ?_) ?_ (sum_nonneg hs₀) hpos
      · exact lt_of_le_of_ne (sum_nonneg hs₀) (Ne.symm hsum_t)
      · intro j hj
        exact hmem j (mem_insert_of_mem hj)
      · exact h₀ _ (mem_insert_self _ _)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
⊢ HasFiniteSupport (w ∘ PLift.down)
have by_contra : ∀ (H : ¬HasFiniteSupport (w ∘ PLift.down)), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (hypothesis)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
H : ¬HasFiniteSupport (w ∘ PLift.down)
⊢ False
have h₂ : Eq.{u_1 + 1} (α := R) 0 1
Tactic: rw [finsum, dif_neg H] at h₁
Cleared hypotheses: h₁, hz, H
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (hypothesis)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
⊢ ∑ᶠ (i : ι), w i • z i ∈ s
have hfin_w : HasFiniteSupport (w ∘ PLift.down)
Tactic: have hfin_w : HasFiniteSupport (w ∘ PLift.down) := by
    by_contra H
    rw [finsum, dif_neg H] at h₁
    exact zero_ne_one h₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (hypothesis)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
⊢ ∑ᶠ (i : ι), w i • z i ∈ s
have hsub : support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
  (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))
Tactic: have hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ hfin_w.toFinset :=
    (support_smul_subset_left _ _).trans hfin_w.coe_toFinset.ge
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub :
  support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))
⊢ ∑ᶠ (i : ι), w i • z i ∈ s
have rw : ∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down • z i.down ∈ s
Tactic: rw [finsum_eq_sum_plift_of_support_subset hsub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub :
  support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))
⊢ ∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down • z i.down ∈ s
have refine_1 : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down) 1
Tactic: refine hs.sum_mem (fun _ _ => h₀ _) ?_ fun i hi => hz _ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub :
  support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))
refine_1 : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down) 1
⊢ ∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down • z i.down ∈ s
have refine_2 : ∀ (i : PLift ι) (hi : i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w), w i.down ≠ 0
Tactic: refine hs.sum_mem (fun _ _ => h₀ _) ?_ fun i hi => hz _ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub :
  support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down) 1
have refine_1 : ∀
  (h₁ :
    Eq.{u_1 + 1} (α := R)
      (if h : HasFiniteSupport.{u_8, u_1} (α := PLift ι) (M := R) ((fun (i : ι) ↦ w i) ∘ PLift.down) then
        ∑ i ∈ Finite.toFinset (s := support.{u_8, u_1} (M := R) ((fun (i : ι) ↦ w i) ∘ PLift.down)) h, w i.down
      else 0)
      1)
  (hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s) (hfin_w : HasFiniteSupport (w ∘ PLift.down))
  (hsub :
    support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
      (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))),
  Eq.{u_1 + 1} (α := R) (∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down) 1
Tactic: rwa [finsum, dif_pos hfin_w] at h₁
Cleared hypotheses: h₁, hz, hfin_w, hsub
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub :
  support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))
refine_1 :
  ∀
    (h₁ :
      Eq.{u_1 + 1} (α := R)
        (if h : HasFiniteSupport.{u_8, u_1} (α := PLift ι) (M := R) ((fun (i : ι) ↦ w i) ∘ PLift.down) then
          ∑ i ∈ Finite.toFinset (s := support.{u_8, u_1} (M := R) ((fun (i : ι) ↦ w i) ∘ PLift.down)) h, w i.down
        else 0)
        1)
    (hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s) (hfin_w : HasFiniteSupport (w ∘ PLift.down))
    (hsub :
      support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
        (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))),
    Eq.{u_1 + 1} (α := R) (∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down) 1
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down) 1
have refine_1₁ : ∀ (hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s) (hfin_w : HasFiniteSupport (w ∘ PLift.down))
  (h₁ :
    Eq.{u_1 + 1} (α := R)
      (∑ i ∈ Finite.toFinset (s := support.{u_8, u_1} (M := R) ((fun (i : ι) ↦ w i) ∘ PLift.down)) hfin_w, w i.down) 1)
  (hsub :
    support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
      (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))),
  Eq.{u_1 + 1} (α := R) (∑ i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w, w i.down) 1
Tactic: rwa [finsum, dif_pos hfin_w] at h₁
Cleared hypotheses: h₁, hz, hfin_w, hsub
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
ι : Sort u_8
w : ι → R
z : ι → E
s : Set E
hs : Convex R s
h₀ : ∀ (i : ι), 0 ≤ w i
h₁ : Eq.{u_1 + 1} (α := R) (∑ᶠ (i : ι), w i) 1
hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s
hfin_w : HasFiniteSupport (w ∘ PLift.down)
hsub :
  support.{u_8, u_3} (M := E) ((fun (i : ι) ↦ w i • z i) ∘ PLift.down) ⊆
    (↑(Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w) : Set (PLift ι))
i : PLift ι
hi : i ∈ Finite.toFinset (s := support (w ∘ PLift.down)) hfin_w
⊢ w i.down ≠ 0
have refine_2 : ∀ (hi : i ∈ support (w ∘ PLift.down)), w i.down ≠ 0
Tactic: rwa [hfin_w.mem_toFinset] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
⊢ Convex R s ↔
    ∀ (t : Finset E) (w : E → R),
      (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
have refine : (∀ (t : Finset E) (w : E → R),
    (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s) →
  Convex R s
Tactic: refine ⟨fun hs t w hw₀ hw₁ hts => hs.sum_mem hw₀ hw₁ hts, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s
have pos : ∀ (h_cases : x = y), a • x + b • y ∈ s
Tactic: by_cases h_cases : x = y
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
pos : ∀ (h_cases : x = y), a • x + b • y ∈ s
⊢ a • x + b • y ∈ s
have neg : ∀ (h_cases : ¬x = y), a • x + b • y ∈ s
Tactic: by_cases h_cases : x = y
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
⊢ a • x + b • y ∈ s
have h₁ : a • x + b • y = ∑ x ∈ {x, y}, (if x = y then b else a) • x
Tactic: convert! h { x, y } (fun z => if z = y then b else a) _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
h₁ : a • x + b • y = ∑ x ∈ {x, y}, (if x = y then b else a) • x
⊢ a • x + b • y ∈ s
have neg : ∀ (i : E), Membership.mem (γ := Finset E) {x, y} i → LE.le.{u_1} (α := R) 0 ((fun (z : E) ↦ if z = y then b else a) i)
Tactic: convert! h { x, y } (fun z => if z = y then b else a) _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
h₁ : a • x + b • y = ∑ x ∈ {x, y}, (if x = y then b else a) • x
neg :
  ∀ (i : E), Membership.mem (γ := Finset E) {x, y} i → LE.le.{u_1} (α := R) 0 ((fun (z : E) ↦ if z = y then b else a) i)
⊢ a • x + b • y ∈ s
have neg₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ {x, y}, (fun (z : E) ↦ if z = y then b else a) i) 1
Tactic: convert! h { x, y } (fun z => if z = y then b else a) _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
h₁ : a • x + b • y = ∑ x ∈ {x, y}, (if x = y then b else a) • x
neg :
  ∀ (i : E), Membership.mem (γ := Finset E) {x, y} i → LE.le.{u_1} (α := R) 0 ((fun (z : E) ↦ if z = y then b else a) i)
neg₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ {x, y}, (fun (z : E) ↦ if z = y then b else a) i) 1
⊢ a • x + b • y ∈ s
have neg₂ : ∀ (x_1 : E), Membership.mem (γ := Finset E) {x, y} x_1 → x_1 ∈ s
Tactic: convert! h { x, y } (fun z => if z = y then b else a) _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (hypothesis)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
hi : Membership.mem (γ := Finset E) {x, y} i
⊢ i ∈ s
have hi₁ : i = x ∨ i = y
Tactic: simp only [Finset.mem_singleton, Finset.mem_insert] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
hi : i = x ∨ i = y
⊢ i ∈ s
have neg : i = x → i ∈ s
Tactic: cases hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
h :
  ∀ (t : Finset E) (w : E → R),
    (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h_cases : ¬x = y
i : E
hi : i = x ∨ i = y
neg : i = x → i ∈ s
⊢ i ∈ s
have neg₁ : i = y → i ∈ s
Tactic: cases hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.Convex.Combination (goal)
Goal:
R : Type u_1
E : Type u_3
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
s : Set E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
⊢ Convex R s ↔
    ∀ (t : Finset E) (w : E → R),
      (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s
have refine : (∀ (t : Finset E) (w : E → R),
    (∀ i ∈ t, 0 ≤ w i) → Eq.{u_1 + 1} (α := R) (∑ i ∈ t, w i) 1 → (∀ x ∈ t, x ∈ s) → ∑ x ∈ t, w x • x ∈ s) →
  Convex R s
Tactic: classical
  refine ⟨fun hs t w hw₀ hw₁ hts => hs.sum_mem hw₀ hw₁ hts, ?_⟩
  intro h x hx y hy a b ha hb hab
  by_cases h_cases : x = y
  · rw [h_cases, ← add_smul, hab, one_smul]
    exact hy
  · convert! h { x, y } (fun z => if z = y then b else a) _ _ _
    · simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial]
    · grind
    · simp only [sum_pair h_cases, if_neg h_cases, if_pos trivial, hab]
    · intro i hi
      simp only [Finset.mem_singleton, Finset.mem_insert] at hi
      cases hi <;> subst i <;> assumption