awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ∑ i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i : R) (id i -ᵥ y) =
    s • (x -ᵥ y)
have e_a : ∑ x_1 ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
    HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) x_1 : R) (x_1 -ᵥ y) =
  s • (x -ᵥ y)
Tactic: simp only [id]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ∑ x_1 ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R)
        ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) x_1 : R) (x_1 -ᵥ y) =
    s • (x -ᵥ y)
have e_a : ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).sum fun (p : P) (w : R) ↦ w • (p -ᵥ y)) =
  s • (x -ᵥ y)
Tactic: change (Finsupp.single x s + Finsupp.single y t).sum (fun p w => w • (p -ᵥ y)) = _
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ ((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).sum fun (p : P) (w : R) ↦ w • (p -ᵥ y)) =
    s • (x -ᵥ y)
have e_a : s • (x -ᵥ y) + t • (y -ᵥ y) = s • (x -ᵥ y)
Tactic: rw [Finsupp.sum_add_index (by simp) (fun _ a b => by simp [add_smul]),
    Finsupp.sum_single_index (by simp), Finsupp.sum_single_index (by simp)]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
⊢ (Finset.affineCombination R (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support id :
        (a : P → R) → P)
      (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) =
    s • (x -ᵥ y) +ᵥ y
have Use : HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
    (((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support.weightedVSubOfPoint id y :
          (a : P → R) → V)
        (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) :
      V)
    y =
  s • (x -ᵥ y) +ᵥ y
Tactic: classical
  -- Use weighted subtraction with base point y
  rw [Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ id (b := y)]
  swap
  · -- Prove sum of weights equals 1
    trans (Finsupp.single x s + Finsupp.single y t).sum fun _ r => r
    · apply Finset.sum_congr rfl
      intro i _
      simp only [Finsupp.coe_add, Pi.add_apply]
    · rw [Finsupp.sum_add_index (by simp) (by simp), Finsupp.sum_single_index (by simp),
        Finsupp.sum_single_index (by simp), h]
  -- Now simplify the weighted subtraction
  congr 1
  rw [Finset.weightedVSubOfPoint_apply]
  simp only [id]
  -- Convert to Finsupp.sum
  change (Finsupp.single x s + Finsupp.single y t).sum (fun p w => w • (p -ᵥ y)) = _
  rw [Finsupp.sum_add_index (by simp) (fun _ a b => by simp [add_smul]),
    Finsupp.sum_single_index (by simp), Finsupp.sum_single_index (by simp)]
  simp [vsub_self]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.AffineSpace (goal)
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : AffineSpace V P
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : P
Use :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      (((HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support.weightedVSubOfPoint id y :
            (a : P → R) → V)
          (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) :
        V)
      y =
    s • (x -ᵥ y) +ᵥ y
⊢ (Finset.affineCombination R (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support id :
        (a : P → R) → P)
      (⇑(HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)) : (a : P) → R) =
    s • (x -ᵥ y) +ᵥ y
have Use₁ : Eq.{u_1 + 1} (α := R)
  (∑ i ∈ (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t)).support,
    (HAdd.hAdd (α := P →₀ R) (Finsupp.single x s) (Finsupp.single y t) : (a : P) → R) i)
  1
Tactic: classical
  -- Use weighted subtraction with base point y
  rw [Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ id (b := y)]
  swap
  · -- Prove sum of weights equals 1
    trans (Finsupp.single x s + Finsupp.single y t).sum fun _ r => r
    · apply Finset.sum_congr rfl
      intro i _
      simp only [Finsupp.coe_add, Pi.add_apply]
    · rw [Finsupp.sum_add_index (by simp) (by simp), Finsupp.sum_single_index (by simp),
        Finsupp.sum_single_index (by simp), h]
  -- Now simplify the weighted subtraction
  congr 1
  rw [Finset.weightedVSubOfPoint_apply]
  simp only [id]
  -- Convert to Finsupp.sum
  change (Finsupp.single x s + Finsupp.single y t).sum (fun p w => w • (p -ᵥ y)) = _
  rw [Finsupp.sum_add_index (by simp) (fun _ a b => by simp [add_smul]),
    Finsupp.sum_single_index (by simp), Finsupp.sum_single_index (by simp)]
  simp [vsub_self]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
f g : StdSimplex R M
⊢ f.weights = g.weights ↔ f = g
have mk : ∀ (weights : M →₀ R) (nonneg : 0 ≤ weights) (total : Eq (α := R) (weights.sum fun (x : M) (r : R) ↦ r) 1),
  { weights := weights, nonneg := nonneg, total := total : StdSimplex R M }.weights = g.weights ↔
    { weights := weights, nonneg := nonneg, total := total : StdSimplex R M } = g
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
g : StdSimplex R M
weights : M →₀ R
nonneg : 0 ≤ weights
total : Eq (α := R) (weights.sum fun (x : M) (r : R) ↦ r) 1
⊢ { weights := weights, nonneg := nonneg, total := total : StdSimplex R M }.weights = g.weights ↔
    { weights := weights, nonneg := nonneg, total := total : StdSimplex R M } = g
have mk : ∀ (weights_1 : M →₀ R) (nonneg_1 : 0 ≤ weights_1) (total_1 : Eq (α := R) (weights_1.sum fun (x : M) (r : R) ↦ r) 1),
  { weights := weights, nonneg := nonneg, total := total : StdSimplex R M }.weights =
      { weights := weights_1, nonneg := nonneg_1, total := total_1 : StdSimplex R M }.weights ↔
    { weights := weights, nonneg := nonneg, total := total : StdSimplex R M } =
      { weights := weights_1, nonneg := nonneg_1, total := total_1 }
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
⊢ w.weights.support = {x} → w = single x
have rw : (∃ (b : R), b ≠ 0 ∧ w.weights = Finsupp.single x b) → w = single x
Tactic: rw [support_eq_singleton']
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
a : R
ha : a ≠ 0
hwa : w.weights = Finsupp.single x a
⊢ w = single x
have a₁ : w.weights = weights (single x)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
a : R
ha : a ≠ 0
hwa : w.weights = Finsupp.single x a
⊢ w.weights = weights (single x)
have a₁ : Eq (α := M →₀ R) (Finsupp.single x a) (Finsupp.single x 1)
Tactic: simp only [hwa, weights_single]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
a : R
ha : a ≠ 0
hwa : w.weights = Finsupp.single x a
⊢ Eq (α := M →₀ R) (Finsupp.single x a) (Finsupp.single x 1)
have a₁ : a = 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
⊢ w.weights.support = {x} → w = single x
have rw : (∃ (b : R), b ≠ 0 ∧ w.weights = Finsupp.single x b) → w = single x
Tactic: classical
    rw [support_eq_singleton']
    rintro ⟨a, ha, hwa⟩
    ext : 1
    simp only [hwa, weights_single]
    congr
    simpa [hwa] using w.total
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
rw rw₁ rw₂ : (∃ (b : R), b ≠ 0 ∧ w.weights = Finsupp.single x b) → w = single x
⊢ w.weights.support = {x} → w = single x
have rw₃ : ∀ (a : R) (ha : a ≠ 0) (hwa : w.weights = Finsupp.single x a), w = single x
Tactic: classical
    rw [support_eq_singleton']
    rintro ⟨a, ha, hwa⟩
    ext : 1
    simp only [hwa, weights_single]
    congr
    simpa [hwa] using w.total
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
rw rw₁ rw₂ : (∃ (b : R), b ≠ 0 ∧ w.weights = Finsupp.single x b) → w = single x
rw₃ : ∀ (a : R) (ha : a ≠ 0) (hwa : w.weights = Finsupp.single x a), w = single x
⊢ w.weights.support = {x} → w = single x
have a : ∀ (a : R) (ha : a ≠ 0) (hwa : w.weights = Finsupp.single x a), w.weights = weights (single x)
Tactic: classical
    rw [support_eq_singleton']
    rintro ⟨a, ha, hwa⟩
    ext : 1
    simp only [hwa, weights_single]
    congr
    simpa [hwa] using w.total
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
rw rw₁ rw₂ : (∃ (b : R), b ≠ 0 ∧ w.weights = Finsupp.single x b) → w = single x
rw₃ : ∀ (a : R) (ha : a ≠ 0) (hwa : w.weights = Finsupp.single x a), w = single x
a : ∀ (a : R) (ha : a ≠ 0) (hwa : w.weights = Finsupp.single x a), w.weights = weights (single x)
⊢ w.weights.support = {x} → w = single x
have a₁ : ∀ (a : R) (ha : a ≠ 0) (hwa : w.weights = Finsupp.single x a),
  Eq (α := M →₀ R) (Finsupp.single x a) (Finsupp.single x 1)
Tactic: classical
    rw [support_eq_singleton']
    rintro ⟨a, ha, hwa⟩
    ext : 1
    simp only [hwa, weights_single]
    congr
    simpa [hwa] using w.total
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
w : StdSimplex R M
x : M
inst_2 : IsStrictOrderedRing R
rw rw₁ rw₂ : (∃ (b : R), b ≠ 0 ∧ w.weights = Finsupp.single x b) → w = single x
rw₃ : ∀ (a : R) (ha : a ≠ 0) (hwa : w.weights = Finsupp.single x a), w = single x
a : ∀ (a : R) (ha : a ≠ 0) (hwa : w.weights = Finsupp.single x a), w.weights = weights (single x)
a₁ :
  ∀ (a : R) (ha : a ≠ 0) (hwa : w.weights = Finsupp.single x a),
    Eq (α := M →₀ R) (Finsupp.single x a) (Finsupp.single x 1)
⊢ w.weights.support = {x} → w = single x
have a₂ : ∀ (a : R) (ha : a ≠ 0) (hwa : w.weights = Finsupp.single x a), a = 1
Tactic: classical
    rw [support_eq_singleton']
    rintro ⟨a, ha, hwa⟩
    ext : 1
    simp only [hwa, weights_single]
    congr
    simpa [hwa] using w.total
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
f : StdSimplex R M
x : N
⊢ map (fun (x_1 : M) ↦ x) f = single x
have a : ∀ (a : N),
  Eq.{u + 1} (α := R) ((weights (map (fun (x_1 : M) ↦ x) f) : (a : N) → R) a : R)
    ((weights (single x) : (a : N) → R) a : R)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
f : StdSimplex R M
x a : N
⊢ Eq.{u + 1} (α := R) ((weights (map (fun (x_1 : M) ↦ x) f) : (a : N) → R) a : R)
    ((weights (single x) : (a : N) → R) a : R)
have pos : x = a →
  Eq.{u + 1} (α := R) ((weights (map (fun (x_1 : M) ↦ x) f) : (a : N) → R) a : R)
    ((weights (single x) : (a : N) → R) a : R)
Tactic: by_cases x = a
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
f : StdSimplex R M
x a : N
pos :
  x = a →
    Eq.{u + 1} (α := R) ((weights (map (fun (x_1 : M) ↦ x) f) : (a : N) → R) a : R)
      ((weights (single x) : (a : N) → R) a : R)
⊢ Eq.{u + 1} (α := R) ((weights (map (fun (x_1 : M) ↦ x) f) : (a : N) → R) a : R)
    ((weights (single x) : (a : N) → R) a : R)
have neg : ¬x = a →
  Eq.{u + 1} (α := R) ((weights (map (fun (x_1 : M) ↦ x) f) : (a : N) → R) a : R)
    ((weights (single x) : (a : N) → R) a : R)
Tactic: by_cases x = a
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
x : M
f : M → N
⊢ Eq (α := StdSimplex R N) (map f (single x)) (single (f x))
have a : ∀ (a : N),
  Eq.{u + 1} (α := R) ((weights (map f (single x)) : (a : N) → R) a : R) ((weights (single (f x)) : (a : N) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
x y : M
f : M → N
⊢ map f (duple x y hs ht h) = duple (f x) (f y) hs ht h
have a : ∀ (a : N),
  Eq.{u + 1} (α := R) (((map f (duple x y hs ht h)).weights : (a : N) → R) a : R)
    (((duple (f x) (f y) hs ht h).weights : (a : N) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
inst_2 : IsStrictOrderedRing R
f : StdSimplex R M
⊢ map id f = f
have a : ∀ (a : M), Eq.{u + 1} (α := R) (((map id f).weights : (a : M) → R) a : R) ((f.weights : (a : M) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
P : Type u_11
inst_2 : IsStrictOrderedRing R
f : StdSimplex R M
g₁ : M → N
g₂ : N → P
⊢ map (g₂ ∘ g₁) f = map g₂ (map g₁ f)
have a : ∀ (a : P),
  Eq.{u + 1} (α := R) (((map (g₂ ∘ g₁) f).weights : (a : P) → R) a : R)
    (((map g₂ (map g₁ f)).weights : (a : P) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
inst_2 : IsStrictOrderedRing R
f : StdSimplex R (StdSimplex R (StdSimplex R M))
⊢ f.join.join = join (map (fun (x : StdSimplex R (StdSimplex R M)) ↦ x.join) f)
have a : f.join.join.weights = weights (join (map (fun (x : StdSimplex R (StdSimplex R M)) ↦ x.join) f))
Tactic: ext1
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
N : Type u_10
inst_2 : IsStrictOrderedRing R
f : StdSimplex R (StdSimplex R M)
g : M → N
⊢ map g f.join = join (map (fun (x : StdSimplex R M) ↦ map g x) f)
have a : (map g f.join).weights = weights (join (map (fun (x : StdSimplex R M) ↦ map g x) f))
Tactic: ext1
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
R : Type u
inst : PartialOrder R
inst_1 : Semiring R
M : Type u_9
inst_2 : IsStrictOrderedRing R
x : StdSimplex R M
⊢ join (single x) = x
have a : ∀ (a : M), Eq.{u + 1} (α := R) (((join (single x)).weights : (a : M) → R) a : R) ((x.weights : (a : M) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (hypothesis)
Goal:
X : Type u_2
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : IsDomain K
w : StdSimplex K X
s : Set X
hs : ∃ x ∈ s, Ne.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)
inst_4 : DecidablePred fun (x : X) ↦ x ∈ s
⊢ (w.restrict s hs).weights.support = {x ∈ w.weights.support | x ∈ s}
have this : Ne (α := K) ((filter (fun (x : X) ↦ x ∈ s) w.weights).sum fun (x : X) (k : K) ↦ k) 0
Tactic: have : (w.weights.filter (· ∈ s)).sum (fun x k ↦ k) ≠ 0 :=
    (sum_pos (by simp +contextual [lt_iff_le_and_ne, eq_comm]) <| by
      simpa [ne_iff, filter_apply]).ne'
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
X : Type u_2
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : IsDomain K
w : StdSimplex K X
s : Set X
hs : ∃ x ∈ s, Ne.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)
inst_4 : DecidablePred fun (x : X) ↦ x ∈ s
this : Ne (α := K) ((filter (fun (x : X) ↦ x ∈ s) w.weights).sum fun (x : X) (k : K) ↦ k) 0
⊢ (w.restrict s hs).weights.support = {x ∈ w.weights.support | x ∈ s}
have rw : (filter (fun (x : X) ↦ x ∈ s) w.weights).support = {x ∈ w.weights.support | x ∈ s}
Tactic: rw [weights_restrict, support_smul_eq (by convert inv_ne_zero this)]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
X : Type u_2
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : IsDomain K
w : StdSimplex K X
x : X
hx :
  ∃ (x_1 : X), Membership.mem (γ := Set X) {x} x_1 ∧ Ne.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) x_1 : K) (0 : K)
⊢ w.restrict {x} hx = single x
have simp : {x_1 ∈ w.weights.support | x_1 = x} = {x}
Tactic: simp only [← support_weights_eq_singleton, support_weights_restrict, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
X : Type u_2
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : IsDomain K
w : StdSimplex K X
x : X
hx :
  ∃ (x_1 : X), Membership.mem (γ := Set X) {x} x_1 ∧ Ne.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) x_1 : K) (0 : K)
⊢ {x_1 ∈ w.weights.support | x_1 = x} = {x}
have h : ∀ (a : X), a ∈ {x_1 ∈ w.weights.support | x_1 = x} ↔ Membership.mem (γ := Finset X) {x} a
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
X : Type u_2
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : IsDomain K
w : StdSimplex K X
x : X
hx :
  ∃ (x_1 : X), Membership.mem (γ := Set X) {x} x_1 ∧ Ne.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) x_1 : K) (0 : K)
a : X
⊢ a ∈ {x_1 ∈ w.weights.support | x_1 = x} ↔ Membership.mem (γ := Finset X) {x} a
have h : a = x → ¬Eq.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) a : K) (0 : K)
Tactic: simp only [Finset.mem_filter, mem_support_iff, ne_eq, Finset.mem_singleton, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
X : Type u_2
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : IsDomain K
w : StdSimplex K X
x : X
hx :
  ∃ (x_1 : X), Membership.mem (γ := Set X) {x} x_1 ∧ Ne.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) x_1 : K) (0 : K)
⊢ w.restrict {x} hx = single x
have simp : {x_1 ∈ w.weights.support | x_1 = x} = {x}
Tactic: classical
  simp only [← support_weights_eq_singleton, support_weights_restrict, Set.mem_singleton_iff]
  ext
  simp only [Finset.mem_filter, mem_support_iff, ne_eq, Finset.mem_singleton, and_iff_right_iff_imp]
  rintro rfl
  simpa using hx
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
X : Type u_2
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : IsDomain K
w : StdSimplex K X
x : X
hx :
  ∃ (x_1 : X), Membership.mem (γ := Set X) {x} x_1 ∧ Ne.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) x_1 : K) (0 : K)
simp : {x_1 ∈ w.weights.support | x_1 = x} = {x}
⊢ w.restrict {x} hx = single x
have h : ∀ (a : X), a ∈ {x_1 ∈ w.weights.support | x_1 = x} ↔ Membership.mem (γ := Finset X) {x} a
Tactic: classical
  simp only [← support_weights_eq_singleton, support_weights_restrict, Set.mem_singleton_iff]
  ext
  simp only [Finset.mem_filter, mem_support_iff, ne_eq, Finset.mem_singleton, and_iff_right_iff_imp]
  rintro rfl
  simpa using hx
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
X : Type u_2
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : IsDomain K
w : StdSimplex K X
x : X
hx :
  ∃ (x_1 : X), Membership.mem (γ := Set X) {x} x_1 ∧ Ne.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) x_1 : K) (0 : K)
simp : {x_1 ∈ w.weights.support | x_1 = x} = {x}
h : ∀ (a : X), a ∈ {x_1 ∈ w.weights.support | x_1 = x} ↔ Membership.mem (γ := Finset X) {x} a
⊢ w.restrict {x} hx = single x
have h₁ : ∀ (a : X), a = x → ¬Eq.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) a : K) (0 : K)
Tactic: classical
  simp only [← support_weights_eq_singleton, support_weights_restrict, Set.mem_singleton_iff]
  ext
  simp only [Finset.mem_filter, mem_support_iff, ne_eq, Finset.mem_singleton, and_iff_right_iff_imp]
  rintro rfl
  simpa using hx
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
X : Type u_2
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : IsDomain K
w : StdSimplex K X
x : X
hx :
  ∃ (x_1 : X), Membership.mem (γ := Set X) {x} x_1 ∧ Ne.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) x_1 : K) (0 : K)
simp : {x_1 ∈ w.weights.support | x_1 = x} = {x}
h : ∀ (a : X), a ∈ {x_1 ∈ w.weights.support | x_1 = x} ↔ Membership.mem (γ := Finset X) {x} a
h₁ : ∀ (a : X), a = x → ¬Eq.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) a : K) (0 : K)
⊢ w.restrict {x} hx = single x
have h₂ : ∀ (a : X)
  (hx : ∃ (x : X), Membership.mem (γ := Set X) {a} x ∧ Ne.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)),
  ¬Eq.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) a : K) (0 : K)
Tactic: classical
  simp only [← support_weights_eq_singleton, support_weights_restrict, Set.mem_singleton_iff]
  ext
  simp only [Finset.mem_filter, mem_support_iff, ne_eq, Finset.mem_singleton, and_iff_right_iff_imp]
  rintro rfl
  simpa using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Geometry.Convex.ConvexSpace.Defs (goal)
Goal:
I : Type u_6
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
w : StdSimplex K I
s : Set I
hs : ∃ x ∈ s, Ne.{u_8 + 1} (α := K) ((w.weights : (a : I) → K) x : K) (0 : K)
hs' : ∃ x ∈ sᶜ, Ne.{u_8 + 1} (α := K) ((w.weights : (a : I) → K) x : K) (0 : K)
inst_3 : DecidablePred fun (x : I) ↦ x ∈ s
⊢ convexCombPair ((filter (fun (x : I) ↦ x ∈ s) w.weights).sum fun (_x : I) (k : K) ↦ k)
      ((filter (fun (x : I) ↦ x ∉ s) w.weights).sum fun (_x : I) (k : K) ↦ k) ⋯ ⋯ ⋯ (w.restrict s hs)
      (w.restrict sᶜ hs') =
    w
have a : (convexCombPair ((filter (fun (x : I) ↦ x ∈ s) w.weights).sum fun (_x : I) (k : K) ↦ k)
      ((filter (fun (x : I) ↦ x ∉ s) w.weights).sum fun (_x : I) (k : K) ↦ k) sorry sorry sorry (w.restrict s hs)
      (w.restrict sᶜ hs')).weights =
  w.weights
Tactic: ext : 1