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
inst : Field R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : LinearOrder R
inst_4 : IsStrictOrderedRing R
s t : Set E
simp_rw :
  (convexHull R : (a : Set E) → Set E) (s + -t) =
    HAdd.hAdd (α := Set E) (β := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
      (-(convexHull R : (a : Set E) → Set E) t : Set E)
⊢ (convexHull R : (a : Set E) → Set E) (s - t) =
    HSub.hSub (α := Set E) (β := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
      ((convexHull R : (a : Set E) → Set E) t : Set E)
have simp_rw₁ : HAdd.hAdd (α := Set E) (β := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    ((convexHull R : (a : Set E) → Set E) (-t) : Set E) =
  HAdd.hAdd (α := Set E) (β := Set E) ((convexHull R : (a : Set E) → Set E) s : Set E)
    (-(convexHull R : (a : Set E) → Set E) t : Set E)
Tactic: simp_rw [sub_eq_add_neg, convexHull_add, ← convexHull_neg]
-- 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
ι : Type u_8
b : AffineBasis ι R E
⊢ Eq.{u_3 + 1} (α := Set E)
    ((convexHull R : (a : Set E) → Set E) (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E)) : Set E)
    ({x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} : Set E)
have rw : Eq.{u_3 + 1} (α := Set E)
  {x : E |
    ∃ (s : Finset ι) (w : ι → R),
      (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
  {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)}
Tactic: rw [convexHull_range_eq_exists_affineCombination]
-- 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
ι : Type u_8
b : AffineBasis ι R E
⊢ Eq.{u_3 + 1} (α := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
    {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)}
have h : ∀ (x : E),
  Membership.mem (γ := Set E)
      {x : E |
        ∃ (s : Finset ι) (w : ι → R),
          (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
      x ↔
    Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
Tactic: ext x
-- 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
ι : Type u_8
b : AffineBasis ι R E
x : E
⊢ Membership.mem (γ := Set E)
      {x : E |
        ∃ (s : Finset ι) (w : ι → R),
          (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
      x ↔
    Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
have h : Membership.mem (γ := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
    x →
  Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
Tactic: refine ⟨?_, fun hx => ?_⟩
-- 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
ι : Type u_8
b : AffineBasis ι R E
x : E
h :
  Membership.mem (γ := Set E)
      {x : E |
        ∃ (s : Finset ι) (w : ι → R),
          (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
      x →
    Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
⊢ Membership.mem (γ := Set E)
      {x : E |
        ∃ (s : Finset ι) (w : ι → R),
          (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
      x ↔
    Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
have h₁ : ∀
  (hx :
    Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x),
  Membership.mem (γ := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
    x
Tactic: refine ⟨?_, fun hx => ?_⟩
-- 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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
⊢ LE.le.{u_1} (α := R) (0 : R)
    ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)
have pos : ∀ (hi : i ∈ s),
  LE.le.{u_1} (α := R) (0 : R)
    ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)
Tactic: by_cases hi : i ∈ s
-- 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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
pos :
  ∀ (hi : i ∈ s),
    LE.le.{u_1} (α := R) (0 : R)
      ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)
⊢ LE.le.{u_1} (α := R) (0 : R)
    ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)
have neg : ∀ (hi : i ∉ s),
  LE.le.{u_1} (α := R) (0 : R)
    ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)
Tactic: by_cases hi : i ∈ s
-- 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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
hi : i ∈ s
⊢ LE.le.{u_1} (α := R) (0 : R)
    ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)
have pos : 0 ≤ w i
Tactic: rw [b.coord_apply_combination_of_mem hi hw₁]
-- 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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
hi : i ∉ s
⊢ LE.le.{u_1} (α := R) (0 : R)
    ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)
have neg : LE.le.{u_1} (α := R) 0 0
Tactic: rw [b.coord_apply_combination_of_notMem hi hw₁]
-- 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
ι : Type u_8
b : AffineBasis ι R E
x : E
hx : Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
⊢ Membership.mem (γ := AffineSubspace R E) (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E))) x
have rw : Membership.mem (γ := AffineSubspace R E) ⊤ x
Tactic: rw [b.tot]
-- 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
ι : Type u_8
b : AffineBasis ι R E
x : E
hx : Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
⊢ Membership.mem (γ := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
    x
have hx' : Membership.mem (γ := AffineSubspace R E) (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E))) x
Tactic: have hx' : x ∈ affineSpan R (range b) := by
      rw [b.tot]
      exact AffineSubspace.mem_top R E x
-- 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
ι : Type u_8
b : AffineBasis ι R E
x : E
hx : Membership.mem (γ := Set E) {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)} x
hx' : Membership.mem (γ := AffineSubspace R E) (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E))) x
⊢ Membership.mem (γ := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
    x
have h : ∀ (s : Finset ι) (w : ι → R) (hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1)
  (hx :
    Membership.mem.{u_3, u_3} (α := E) (γ := Set E)
      {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)}
      ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E))
  (hx' :
    Membership.mem (α := E) (γ := AffineSubspace R E)
      (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E)))
      ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)),
  Membership.mem.{u_3, u_3} (α := E) (γ := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
Tactic: obtain ⟨s, w, hw₁, rfl⟩ := (mem_affineSpan_iff_eq_affineCombination R E).mp hx'
Cleared hypotheses: x, hx, hx'
-- 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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hx :
  Membership.mem.{u_3, u_3} (α := E) (γ := Set E)
    {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)}
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
hx' :
  Membership.mem (α := E) (γ := AffineSubspace R E)
    (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E)))
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
⊢ Membership.mem.{u_3, u_3} (α := E) (γ := Set E)
    {x : E |
      ∃ (s : Finset ι) (w : ι → R),
        (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w = x}
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
have h : ∀ i ∈ s, 0 ≤ w i
Tactic: refine ⟨s, w, ?_, hw₁, rfl⟩
-- 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
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 1
hx :
  Membership.mem.{u_3, u_3} (α := E) (γ := Set E)
    {x : E | ∀ (i : ι), LE.le.{u_1} (α := R) (0 : R) ((b.coord i : (a : E) → R) x : R)}
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
hx' :
  Membership.mem (α := E) (γ := AffineSubspace R E)
    (affineSpan R (Set.range.{u_3, u_8 + 1} (ι := ι) (⇑b : (a : ι) → E)))
    ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E)
i : ι
hi : i ∈ s
⊢ 0 ≤ w i
have hx₁ : LE.le.{u_1} (α := R) (0 : R)
  ((b.coord i : (a : E) → R) ((affineCombination R s (⇑b : (a : ι) → E) : (a : ι → R) → E) w : E) : R)
Tactic: specialize hx i
Cleared hypotheses: hx
-- 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
s t₁ t₂ : Finset E
hs : AffineIndependent R (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
⊢ Eq (α := Set E) ((convexHull R : (a : Set E) → Set E) ((↑t₁ : Set E) ∩ (↑t₂ : Set E)) : Set E)
    ((convexHull R : (a : Set E) → Set E) (↑t₁ : Set E) ∩ (convexHull R : (a : Set E) → Set E) (↑t₂ : Set E) : Set E)
have refine : Subset (α := Set E)
  ((convexHull R : (a : Set E) → Set E) (↑t₁ : Set E) ∩ (convexHull R : (a : Set E) → Set E) (↑t₂ : Set E) : Set E)
  ((convexHull R : (a : Set E) → Set E) ((↑t₁ : Set E) ⊓ (↑t₂ : Set E)) : Set E)
Tactic: refine (Set.subset_inter (convexHull_mono inf_le_left) <|
    convexHull_mono inf_le_right).antisymm ?_
-- 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
s t₁ t₂ : Finset E
hs : AffineIndependent R (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
⊢ Subset (α := Set E)
    ((convexHull R : (a : Set E) → Set E) (↑t₁ : Set E) ∩ (convexHull R : (a : Set E) → Set E) (↑t₂ : Set E) : Set E)
    ((convexHull R : (a : Set E) → Set E) ((↑t₁ : Set E) ⊓ (↑t₂ : Set E)) : Set E)
have simp_rw : ∀ (x : E),
  ((∃ (w : E → R), (∀ y ∈ t₁, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w y) 1 ∧ ∑ y ∈ t₁, w y • y = x) ∧
      ∃ (w : E → R), (∀ y ∈ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w y) 1 ∧ ∑ y ∈ t₂, w y • y = x) →
    ∃ (w : E → R), (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
Tactic: simp_rw [Set.subset_def, mem_inter_iff, Set.inf_eq_inter, ← coe_inter, mem_convexHull']
-- 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
s t₁ t₂ : Finset E
hs : AffineIndependent R (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
⊢ ∃ (w : E → R), (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
have h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
Tactic: have h₁w : ∑ i ∈ s, w i = 0 := by simp [w, Finset.inter_eq_right.2, *]
-- 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
s t₁ t₂ : Finset E
hs : AffineIndependent R (P := E) (ι := ↥s) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
⊢ ∃ (w : E → R), (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
have hs₁ : ∀ x ∈ s, w x = 0
Tactic: replace hs := hs.eq_zero_of_sum_eq_zero_subtype h₁w <| by
    simp only [w, sub_smul, zero_smul, ite_smul, Finset.sum_sub_distrib, ← Finset.sum_filter, h₃w₁,
      Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht₁, Finset.inter_eq_right.2 ht₂, h₃w₂,
      sub_self]
Cleared hypotheses: hs
-- 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
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
⊢ ∃ (w : E → R), (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
have ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
Tactic: have ht (x) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂) : w₁ x = 0 := by
    simpa [w, hx₁, hx₂] using hs _ (ht₁ hx₁)
-- 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
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
⊢ ∃ (w : E → R), (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
have refine_1 : ∀ y ∈ t₁ ∩ t₂, 0 ≤ w₁ y
Tactic: refine ⟨w₁, ?_, ?_, ?_⟩
-- 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
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
refine_1 : ∀ y ∈ t₁ ∩ t₂, 0 ≤ w₁ y
⊢ ∃ (w : E → R), (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
have refine_2 : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w₁ y) 1
Tactic: refine ⟨w₁, ?_, ?_, ?_⟩
-- 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
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
refine_1 : ∀ y ∈ t₁ ∩ t₂, 0 ≤ w₁ y
refine_2 : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w₁ y) 1
⊢ ∃ (w : E → R), (∀ y ∈ t₁ ∩ t₂, 0 ≤ w y) ∧ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w y) 1 ∧ ∑ y ∈ t₁ ∩ t₂, w y • y = x
have refine_3 : ∑ y ∈ t₁ ∩ t₂, w₁ y • y = x
Tactic: refine ⟨w₁, ?_, ?_, ?_⟩
-- 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
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
⊢ ∀ y ∈ t₁ ∩ t₂, 0 ≤ w₁ y
have refine_1 : ∀ y ∈ t₁, y ∈ t₂ → 0 ≤ w₁ y
Tactic: simp only [and_imp, Finset.mem_inter]
-- 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
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
⊢ Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁ ∩ t₂, w₁ y) 1
have refine_2 : ∀ x ∈ t₁, x ∉ t₁ ∩ t₂ → w₁ x = 0
Tactic: rwa [sum_subset inter_subset_left]
-- 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
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x_1 : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x_1
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x_1
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
x : E
⊢ x ∈ t₁ → x ∉ t₁ ∩ t₂ → w₁ x = 0
have refine_2 : ∀ (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
Tactic: simp_intro hx₁ hx₂
-- 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
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
⊢ ∑ y ∈ t₁ ∩ t₂, w₁ y • y = x
have refine_3 : ∀ x ∈ t₁, x ∉ t₁ ∩ t₂ → w₁ x • x = 0
Tactic: rwa [sum_subset inter_subset_left]
-- 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
s t₁ t₂ : Finset E
ht₁ : t₁ ⊆ s
ht₂ : t₂ ⊆ s
x_1 : E
w₁ : E → R
h₁w₁ : ∀ y ∈ t₁, 0 ≤ w₁ y
h₂w₁ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₁, w₁ y) 1
h₃w₁ : ∑ y ∈ t₁, w₁ y • y = x_1
w₂ : E → R
h₂w₂ : Eq.{u_1 + 1} (α := R) (∑ y ∈ t₂, w₂ y) 1
h₃w₂ : ∑ y ∈ t₂, w₂ y • y = x_1
w : (x : E) → R := fun (x : E) ↦ (if x ∈ t₁ then w₁ x else 0) - if x ∈ t₂ then w₂ x else 0
h₁w : Eq.{u_1 + 1} (α := R) (∑ i ∈ s, w i) 0
hs : ∀ x ∈ s, w x = 0
ht : ∀ (x : E) (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0
x : E
⊢ x ∈ t₁ → x ∉ t₁ ∩ t₂ → w₁ x • x = 0
have refine_3 : ∀ (hx₁ : x ∈ t₁) (hx₂ : x ∉ t₂), w₁ x = 0 ∨ x = 0
Tactic: simp_intro hx₁ hx₂