awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing 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)
x : X
⊢ LE.le.{u_8} (α := K) ((0 : (a : X) → K) x : K) ((filter (fun (x : X) ↦ x ∈ s) w.weights : (a : X) → K) x : K)

Tactic:
simp [filter_apply, apply_ite]

Premises used: apply_ite, Finsupp.filter_apply
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing 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)
⊢ 0 ≤
    HSMul.hSMul (α := K) ((filter (fun (x : X) ↦ x ∈ s) w.weights).sum fun (x : X) (k : K) ↦ k)⁻¹
      (filter (fun (x : X) ↦ x ∈ s) w.weights)

Tactic:
exact smul_nonneg (inv_nonneg.2 restrict_nonneg_aux) fun _ ↦ by simp [filter_apply, apply_ite]

Premises used: Iff.mpr, smul_nonneg, inv_nonneg
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing 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)
⊢ 0 ≤
    HSMul.hSMul (α := K) ((filter (fun (x : X) ↦ x ∈ s) w.weights).sum fun (x : X) (k : K) ↦ k)⁻¹
      (filter (fun (x : X) ↦ x ∈ s) w.weights)

Tactic:
classical
    exact smul_nonneg (inv_nonneg.2 restrict_nonneg_aux) fun _ ↦ by simp [filter_apply, apply_ite]

Premises used: Iff.mpr, smul_nonneg, inv_nonneg
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing 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)
⊢ Eq (α := K)
    ((HSMul.hSMul (α := K) ((filter (fun (x : X) ↦ x ∈ s) w.weights).sum fun (x : X) (k : K) ↦ k)⁻¹
          (filter (fun (x : X) ↦ x ∈ s) w.weights)).sum
      fun (x : X) (r : K) ↦ r)
    1

Tactic:
simp [sum_smul_index, ← mul_sum, restrict_ne_zero_aux hs]

Premises used: Finsupp.sum_smul_index, _private.0.Convexity.StdSimplex.restrict_ne_zero_aux, Finsupp.mul_sum
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing 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)
⊢ Eq (α := K)
    ((HSMul.hSMul (α := K) ((filter (fun (x : X) ↦ x ∈ s) w.weights).sum fun (x : X) (k : K) ↦ k)⁻¹
          (filter (fun (x : X) ↦ x ∈ s) w.weights)).sum
      fun (x : X) (r : K) ↦ r)
    1

Tactic:
classical simp [sum_smul_index, ← mul_sum, restrict_ne_zero_aux hs]

Premises used: Finsupp.sum_smul_index, Finsupp.mul_sum
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
X : Type u_2
K : Type u_8
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing 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_3 : DecidablePred fun (x : X) ↦ x ∈ s
⊢ HSMul.hSMul (α := K) ((filter (fun (x : X) ↦ x ∈ s) w.weights).sum fun (x : X) (k : K) ↦ k)⁻¹
      (filter (fun (x : X) ↦ x ∈ s) w.weights) =
    HSMul.hSMul (α := K) ((filter (fun (x : X) ↦ x ∈ s) w.weights).sum fun (x : X) (k : K) ↦ k)⁻¹
      (filter (fun (x : X) ↦ x ∈ s) w.weights)

Tactic:
congr
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
⊢ ∀ i ∈ (filter (fun (x : X) ↦ x ∈ s) w.weights).support,
    LT.lt.{u_8} (α := K) (0 : K) ((filter (fun (x : X) ↦ x ∈ s) w.weights : (a : X) → K) i : K)

Tactic:
simp +contextual [lt_iff_le_and_ne, eq_comm]

Premises used: lt_iff_le_and_ne, eq_comm
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
⊢ filter (fun (x : X) ↦ x ∈ s) w.weights ≠ 0

Tactic:
simpa [ne_iff, filter_apply]

Premises used: Finsupp.filter_apply, Finsupp.ne_iff
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
⊢ 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'
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
⊢ Ne (α := K) ((filter (fun (x : X) ↦ x ∈ s) w.weights).sum fun (x : X) (k : K) ↦ k)⁻¹ 0

Tactic:
inv_ne_zero this

Premises used: inv_ne_zero
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
⊢ Ne (α := K) ((filter (fun (x : X) ↦ x ∈ s) w.weights).sum fun (_x : X) (k : K) ↦ k)⁻¹ 0

Tactic:
convert inv_ne_zero this

Premises used: inv_ne_zero
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
rw : (filter (fun (x : X) ↦ x ∈ s) w.weights).support = {x ∈ w.weights.support | x ∈ s}
⊢ (w.restrict s hs).weights.support = {x ∈ w.weights.support | x ∈ s}

Tactic:
rw [weights_restrict, support_smul_eq (by convert inv_ne_zero this)]

Premises used: Convexity.StdSimplex.weights_restrict, Finsupp.support_smul_eq
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
⊢ (filter (fun (x : X) ↦ x ∈ s) w.weights).support = {x ∈ w.weights.support | x ∈ s}

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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

Tactic:
simp only [← support_weights_eq_singleton, support_weights_restrict, Set.mem_singleton_iff]

Premises used: Convexity.StdSimplex.support_weights_restrict, Convexity.StdSimplex.support_weights_eq_singleton, Set.mem_singleton_iff
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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)
h : ∀ (a : X), a ∈ {x_1 ∈ w.weights.support | x_1 = x} ↔ Membership.mem (γ := Finset X) {x} a
⊢ {x_1 ∈ w.weights.support | x_1 = x} = {x}

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
h : a = x → ¬Eq.{u_8 + 1} (α := K) ((w.weights : (a : X) → K) a : K) (0 : K)
⊢ a ∈ {x_1 ∈ w.weights.support | x_1 = x} ↔ Membership.mem (γ := Finset X) {x} a

Tactic:
simp only [Finset.mem_filter, mem_support_iff, ne_eq, Finset.mem_singleton, and_iff_right_iff_imp]

Premises used: Finsupp.mem_support_iff, Finset.mem_singleton, ne_eq, and_iff_right_iff_imp, Finset.mem_filter
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
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:
simpa using hx
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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)
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)
⊢ w.restrict {x} hx = single 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

Premises used: Finsupp.mem_support_iff, Finset.mem_singleton, Convexity.StdSimplex.support_weights_restrict, Convexity.StdSimplex.support_weights_eq_singleton, ne_eq, Set.mem_singleton_iff, and_iff_right_iff_imp, Finset.mem_filter, rfl
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
⊢ ∀ (x : StdSimplex R I), join (single x) = x

Tactic:
join_single

Premises used: _private.0.Convexity.StdSimplex.join_single
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
⊢ ∀ (x : StdSimplex R I), join (single x) = x

Tactic:
exact join_single

Premises used: _private.0.Convexity.StdSimplex.join_single
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
f : StdSimplex R (StdSimplex R (StdSimplex R I))
⊢ join (map (fun (σ : StdSimplex R (StdSimplex R I)) ↦ σ.join) f) = f.join.join

Tactic:
(join_join f).symm

Premises used: _private.0.Convexity.StdSimplex.join_join, Eq.symm
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
f : StdSimplex R (StdSimplex R (StdSimplex R I))
⊢ join (map (fun (σ : StdSimplex R (StdSimplex R I)) ↦ σ.join) f) = f.join.join

Tactic:
exact (join_join f).symm

Premises used: _private.0.Convexity.StdSimplex.join_join, Eq.symm
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
I : Type u_6
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
f : StdSimplex R (StdSimplex R I)
⊢ (sConvexComb f).weights = f.weights.sum fun (d : StdSimplex R I) (r : R) ↦ r • d.weights

Tactic:
StdSimplex.weights_join _

Premises used: Convexity.StdSimplex.weights_join
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
I : Type u_6
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
w : StdSimplex R I
f : I → StdSimplex R I
⊢ (iConvexComb w f).weights = w.weights.sum fun (i : I) (r : R) ↦ r • (f i).weights

Tactic:
simp [iConvexComb, sum_mapDomain_index, add_smul]

Premises used: Finsupp.sum_mapDomain_index, add_smul, Convexity.iConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
I : Type u_6
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
w w' : StdSimplex R I
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
hst : s + t = 1
⊢ (convexCombPair s t hs ht hst w w').weights = s • w.weights + t • w'.weights

Tactic:
simp [convexCombPair, sum_add_index, add_smul]

Premises used: add_smul, Finsupp.sum_add_index, Convexity.convexCombPair
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
I : Type u_6
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
w w' : StdSimplex R I
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
hst : s + t = 1
⊢ (convexCombPair s t hs ht hst w w').weights = s • w.weights + t • w'.weights

Tactic:
classical simp [convexCombPair, sum_add_index, add_smul]

Premises used: add_smul, Finsupp.sum_add_index, Convexity.convexCombPair
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
I : Type u_6
J : Type u_7
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
s : StdSimplex R (StdSimplex R I)
f : I → J
⊢ map f (sConvexComb s) = sConvexComb (map (map f) s)

Tactic:
StdSimplex.map_join s f

Premises used: _private.0.Convexity.StdSimplex.map_join
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
inst_6 : Semifield K
inst_7 : LinearOrder K
inst_8 : 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_9 : DecidablePred fun (x : I) ↦ x ∈ s
⊢ LE.le (α := K) 0 ((filter (fun (x : I) ↦ x ∈ s) w.weights).sum fun (_x : I) (k : K) ↦ k)

Tactic:
restrict_nonneg_aux

Premises used: _private.0.Convexity.StdSimplex.restrict_nonneg_aux
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
inst_6 : Semifield K
inst_7 : LinearOrder K
inst_8 : 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_9 : DecidablePred fun (x : I) ↦ x ∈ s
⊢ LE.le (α := K) 0 ((filter (fun (x : I) ↦ x ∈ s) w.weights).sum fun (_x : I) (k : K) ↦ k)

Tactic:
exact restrict_nonneg_aux

Premises used: _private.0.Convexity.StdSimplex.restrict_nonneg_aux
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
inst_6 : Semifield K
inst_7 : LinearOrder K
inst_8 : 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_9 : DecidablePred fun (x : I) ↦ x ∈ s
⊢ LE.le (α := K) 0 ((filter (fun (x : I) ↦ x ∉ s) w.weights).sum fun (_x : I) (k : K) ↦ k)

Tactic:
restrict_nonneg_aux

Premises used: _private.0.Convexity.StdSimplex.restrict_nonneg_aux
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
inst_6 : Semifield K
inst_7 : LinearOrder K
inst_8 : 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_9 : DecidablePred fun (x : I) ↦ x ∈ s
⊢ LE.le (α := K) 0 ((filter (fun (x : I) ↦ x ∉ s) w.weights).sum fun (_x : I) (k : K) ↦ k)

Tactic:
exact restrict_nonneg_aux

Premises used: _private.0.Convexity.StdSimplex.restrict_nonneg_aux
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
X : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
I : Type u_6
J : Type u_7
K : Type u_8
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
inst_6 : Semifield K
inst_7 : LinearOrder K
inst_8 : 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_9 : DecidablePred fun (x : I) ↦ x ∈ s
⊢ HAdd.hAdd (α := K) ((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) =
    1

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
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) ⋯ ⋯ ⋯ (w.restrict s hs)
        (w.restrict sᶜ hs')).weights =
    w.weights
⊢ 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

Tactic:
ext : 1
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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
⊢ ∃ x ∉ s, Ne.{u_8 + 1} (α := K) ((w.weights : (a : I) → K) x : K) (0 : K)

Tactic:
simp only [Set.mem_compl_iff] at hs'

Premises used: Set.mem_compl_iff
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
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'_1 : ∃ x ∈ sᶜ, Ne.{u_8 + 1} (α := K) ((w.weights : (a : I) → K) x : K) (0 : K)
inst_3 : DecidablePred fun (x : I) ↦ x ∈ s
hs' : ∃ x ∉ s, Ne.{u_8 + 1} (α := K) ((w.weights : (a : I) → K) x : K) (0 : K)
⊢ (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'_1)).weights =
    w.weights

Tactic:
simp [weights_restrict, smul_inv_smul₀, restrict_ne_zero_aux, hs, hs']

Premises used: smul_inv_smul₀, Convexity.StdSimplex.weights_restrict, _private.0.Convexity.StdSimplex.restrict_ne_zero_aux
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
f : StdSimplex R (StdSimplex R M)
⊢ sConvexComb (sConvexComb f) = sConvexComb (map sConvexComb f)

Tactic:
(ConvexSpace.assoc f).symm

Premises used: Convexity.ConvexSpace.assoc, Eq.symm
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
hst : s + t = 1
w w' : StdSimplex R M
⊢ sConvexComb (convexCombPair s t hs ht hst w w') = convexCombPair s t hs ht hst (sConvexComb w) (sConvexComb w')

Tactic:
simp [convexCombPair, sConvexComb_sConvexComb]

Premises used: Convexity.convexCombPair, Convexity.sConvexComb_sConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s : StdSimplex R M
⊢ id (sConvexComb s) = sConvexComb (map id s)

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
inst_4 : ConvexSpace R N
inst_5 : ConvexSpace R P
g : N → P
hg : IsAffineMap R g
f : M → N
hf : IsAffineMap R f
s : StdSimplex R M
⊢ (g ∘ f) (sConvexComb s) = sConvexComb (map (g ∘ f) s)

Tactic:
simp [StdSimplex.map_comp, hf.map_sConvexComb, hg.map_sConvexComb]

Premises used: Convexity.StdSimplex.map_comp, Convexity.IsAffineMap.map_sConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
I : Type u_6
J : Type u_7
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
f : I → J
⊢ IsAffineMap R (M := StdSimplex R I) (map f)

Tactic:
⟨(map_sConvexComb · f)⟩

Premises used: Convexity.IsAffineMap.mk, Convexity.StdSimplex.map_sConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
I : Type u_6
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
w : StdSimplex R I
f : I → M
⊢ sConvexComb (map f w) = iConvexComb w f

Tactic:
rfl

Premises used: Convexity.iConvexComb, rfl
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_1
M : Type u_3
I : Type u_6
inst : PartialOrder R
inst_1 : Semiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s : StdSimplex R I
m : M
⊢ (iConvexComb s fun (x : I) ↦ m) = m

Tactic:
simp [iConvexComb]

Premises used: Convexity.iConvexComb