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 : 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
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
rw : s + (t * s' + t * t') = 1
rw₁ : s + t * (s' + t') = 1
rw₂ : s + t * 1 = 1
rw₃ : s + t = 1
rw₄ rw₅ : Eq.{u_1 + 1} (α := R) 1 1
⊢ s + t * s' + t * t' = 1

Tactic:
rw [add_assoc, ← mul_add, h', mul_one, h]

Premises used: add_assoc, mul_add, mul_one
-- 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
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
simp :
  convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
⊢ convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) =
    convexCombPair (s + t * s') (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃

Tactic:
simp only [add_comm s]

Premises used: add_comm
-- 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
h : s + t = 1
s' t' : R
hs' : 0 ≤ s'
ht' : 0 ≤ t'
h' : s' + t' = 1
s'' t'' : R
hs'' : 0 ≤ s''
ht'' : 0 ≤ t''
h'' : s'' + t'' = 1
H : s * t'' = t * s' * s''
m₁ m₂ m₃ : M
rw :
  convexCombPair t s ht hs ⋯ (convexCombPair s' t' hs' ht' h' m₂ m₃) m₁ =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
rw₁ :
  convexCombPair t s ht hs ⋯ (convexCombPair t' s' ht' hs' ⋯ m₃ m₂) m₁ =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
rw₂ :
  convexCombPair (t * t') (t * s' + s) ⋯ ⋯ ⋯ m₃ (convexCombPair t'' s'' ht'' hs'' ⋯ m₂ m₁) =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
rw₃ :
  convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair t'' s'' ht'' hs'' ⋯ m₂ m₁) m₃ =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
rw₄ rw₅ :
  convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' ⋯ m₁ m₂) m₃ =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
⊢ convexCombPair s t hs ht h m₁ (convexCombPair s' t' hs' ht' h' m₂ m₃) =
    convexCombPair (t * s' + s) (t * t') ⋯ ⋯ ⋯ (convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃

Tactic:
rw [convexCombPair_symm, convexCombPair_symm (x := m₂),
    convexCombPair_convexCombPair_assoc_left (hs'' := ht'') (ht'' := hs'')
      (h'' := (add_comm _ _).trans h'') (H := H),
    convexCombPair_symm, convexCombPair_symm (x := m₂)]

Premises used: Convexity.convexCombPair_convexCombPair_assoc_left, Convexity.convexCombPair_symm, add_comm, Eq.trans
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
simp :
  (iConvexComb f fun (i : I) ↦ iConvexComb (duple 0 1 hs ht h) ![e₁ i, e₂ i]) =
    iConvexComb (duple 0 1 hs ht h) ![iConvexComb f e₁, iConvexComb f e₂]
⊢ (iConvexComb f fun (x : I) ↦ convexCombPair s t hs ht h (e₁ x) (e₂ x)) =
    convexCombPair s t hs ht h (iConvexComb f e₁) (iConvexComb f e₂)

Tactic:
simp only [convexCombPair_def]

Premises used: Convexity.convexCombPair_def
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
⊢ Eq.{u_10 + 1} (α := M)
    (iConvexComb f fun (j : I) ↦ iConvexComb (duple 0 1 hs ht h) fun (i : Fin (Nat.succ 0).succ) ↦ ![e₁, e₂] i j)
    (iConvexComb (duple 0 1 hs ht h) fun (i : Fin (Nat.succ 0).succ) ↦ iConvexComb f (![e₁, e₂] i))

Tactic:
(iConvexComb_comm (.duple 0 1 hs ht h) f ![e₁, e₂]).symm

Premises used: Convexity.iConvexComb_comm, Convexity.StdSimplex.duple, Matrix.vecEmpty, OfNat.ofNat, Eq.symm, Matrix.vecCons
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
h₁ :
  ∀ (i : I),
    Ne.{u_9 + 1} (α := R) ((f.weights : (a : I) → R) i : R) (0 : R) →
      ∀ (j : Fin (Nat.succ 0).succ),
        Ne (α := R) ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) j : R) (0 : R) →
          ![e₁ i, e₂ i] j = ![e₁, e₂] j i
h₂ :
  ∀ (j : Fin (Nat.succ 0).succ),
    Ne (α := R) ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) j : R) (0 : R) →
      ![iConvexComb f e₁, iConvexComb f e₂] j = iConvexComb f (![e₁, e₂] j)
⊢ (iConvexComb f fun (i : I) ↦ iConvexComb (duple 0 1 hs ht h) ![e₁ i, e₂ i]) =
    iConvexComb (duple 0 1 hs ht h) ![iConvexComb f e₁, iConvexComb f e₂]

Tactic:
convert (iConvexComb_comm (.duple 0 1 hs ht h) f ![e₁, e₂]).symm with i _ j _ j

Premises used: Convexity.iConvexComb_comm, Convexity.StdSimplex.duple, Matrix.vecEmpty, OfNat.ofNat, Eq.symm, Matrix.vecCons
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
i : I
h_1 : Ne.{u_9 + 1} (α := R) ((f.weights : (a : I) → R) i : R) (0 : R)
j : Fin (Nat.succ 0).succ
h_2 : Ne (α := R) ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) j : R) (0 : R)
h₁ :
  Ne (α := R)
      ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) :
        R)
      (0 : R) →
    ![e₁ i, e₂ i] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
      ![e₁, e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) i
h₂ :
  Ne (α := R)
      ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) :
        R)
      (0 : R) →
    ![e₁ i, e₂ i] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
      ![e₁, e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) i
⊢ ![e₁ i, e₂ i] j = ![e₁, e₂] j i

Tactic:
fin_cases j
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
i : I
h_1 : Ne.{u_9 + 1} (α := R) ((f.weights : (a : I) → R) i : R) (0 : R)
h_2 :
  Ne (α := R)
    ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) : R)
    (0 : R)
⊢ ![e₁ i, e₂ i] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    ![e₁, e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) i

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
i : I
h_1 : Ne.{u_9 + 1} (α := R) ((f.weights : (a : I) → R) i : R) (0 : R)
h_2 :
  Ne (α := R)
    ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) : R)
    (0 : R)
⊢ ![e₁ i, e₂ i] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    ![e₁, e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) i

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
j : Fin (Nat.succ 0).succ
h_1 : Ne (α := R) ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) j : R) (0 : R)
h₁ :
  Ne (α := R)
      ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) :
        R)
      (0 : R) →
    ![iConvexComb f e₁, iConvexComb f e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
      iConvexComb f (![e₁, e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩))
h₂ :
  Ne (α := R)
      ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) :
        R)
      (0 : R) →
    ![iConvexComb f e₁, iConvexComb f e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
      iConvexComb f (![e₁, e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩))
⊢ ![iConvexComb f e₁, iConvexComb f e₂] j = iConvexComb f (![e₁, e₂] j)

Tactic:
fin_cases j
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
h_1 :
  Ne (α := R)
    ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) : R)
    (0 : R)
⊢ ![iConvexComb f e₁, iConvexComb f e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    iConvexComb f (![e₁, e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩))

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
e₁ e₂ : I → M
h_1 :
  Ne (α := R)
    ((weights (duple 0 1 hs ht h) : (a : Fin (Nat.succ 0).succ) → R) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) : R)
    (0 : R)
⊢ ![iConvexComb f e₁, iConvexComb f e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ)) =
    iConvexComb f (![e₁, e₂] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩))

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
m : M
e : I → M
⊢ (iConvexComb f fun (x : I) ↦ convexCombPair s t hs ht h (e x) m) = convexCombPair s t hs ht h (iConvexComb f e) m

Tactic:
simpa using iConvexComb_convexCombPair_comm hs ht h f e (fun _ ↦ m)

Premises used: Convexity.iConvexComb_convexCombPair_comm
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_9
M : Type u_10
I : Type u_11
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
f : StdSimplex R I
m : M
e : I → M
⊢ (iConvexComb f fun (x : I) ↦ convexCombPair s t hs ht h m (e x)) = convexCombPair s t hs ht h m (iConvexComb f e)

Tactic:
simpa using iConvexComb_convexCombPair_comm hs ht h f (fun _ ↦ m) e

Premises used: Convexity.iConvexComb_convexCombPair_comm
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Defs
Goal:
R : Type u_9
M : Type u_10
inst : PartialOrder R
inst_1 : CommSemiring R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R M
s t : R
hs : 0 ≤ s
ht : 0 ≤ t
h : s + t = 1
m : M
f : StdSimplex R M
⊢ convexCombPair s t hs ht h m (sConvexComb f) = sConvexComb (map (convexCombPair s t hs ht h m) f)

Tactic:
simpa using (iConvexComb_convexCombPair_comm_right hs ht h f m id).symm

Premises used: id, Convexity.iConvexComb_convexCombPair_comm_right, Eq.symm
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M
inst_8 : AddSubmonoidClass F M
inst_9 : SMulMemClass F R M
⊢ ∀ (x : M), (Finsupp.sum (StdSimplex.weights (StdSimplex.single x)) fun (m : M) (r : R) ↦ r • m) = x

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M
inst_8 : AddSubmonoidClass F M
inst_9 : SMulMemClass F R M
⊢ ∀ (f : StdSimplex R (StdSimplex R M)),
    Eq (α := M)
      (Finsupp.sum
        (StdSimplex.weights (StdSimplex.map (fun (w : StdSimplex R M) ↦ w.weights.sum fun (m : M) (r : R) ↦ r • m) f))
        fun (m : M) (r : R) ↦ r • m)
      (f.join.weights.sum fun (m : M) (r : R) ↦ r • m)

Tactic:
simp [Finsupp.sum_mapDomain_index, add_smul, Finsupp.sum_sum_index, Finsupp.sum_smul_index,
      mul_smul, Finsupp.smul_sum]

Premises used: Finsupp.sum_smul_index, Finsupp.sum_mapDomain_index, add_smul, Finsupp.smul_sum, SemigroupAction.mul_smul, Finsupp.sum_sum_index
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M
inst_8 : AddSubmonoidClass F M
inst_9 : SMulMemClass F R M
⊢ IsModuleConvexSpace R R

Tactic:
.ofModule

Premises used: Convexity.IsModuleConvexSpace.ofModule
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
R : Type u_2
M : Type u_3
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : ConvexSpace R M
inst_6 : IsModuleConvexSpace R M
w : StdSimplex R I
f : I → M
⊢ iConvexComb w f = w.weights.sum fun (i : I) (r : R) ↦ r • f i

Tactic:
simp [iConvexComb, sConvexComb_eq_sum, Finsupp.sum_mapDomain_index, add_smul]

Premises used: Convexity.IsModuleConvexSpace.sConvexComb_eq_sum, Finsupp.sum_mapDomain_index, add_smul, Convexity.iConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : ConvexSpace R M
inst_6 : IsModuleConvexSpace R M
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x y : M
⊢ convexCombPair a b ha hb hab x y = a • x + b • y

Tactic:
simp [convexCombPair, sConvexComb_eq_sum, Finsupp.sum_add_index, add_smul]

Premises used: Convexity.IsModuleConvexSpace.sConvexComb_eq_sum, add_smul, Finsupp.sum_add_index, Convexity.convexCombPair
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : ConvexSpace R M
inst_6 : IsModuleConvexSpace R M
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x y : M
⊢ convexCombPair a b ha hb hab x y = a • x + b • y

Tactic:
classical simp [convexCombPair, sConvexComb_eq_sum, Finsupp.sum_add_index, add_smul]

Premises used: Convexity.IsModuleConvexSpace.sConvexComb_eq_sum, add_smul, Finsupp.sum_add_index, Convexity.convexCombPair
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : SetLike F M
inst_6 : AddSubmonoidClass F M
inst_7 : SMulMemClass F R M
inst_8 : ConvexSpace R M
inst_9 : IsModuleConvexSpace R M
S : F
⊢ IsConvexSet R (↑S : Set M)

Tactic:
.of_sConvexComb_mem fun w hw ↦ ?_

Premises used: Convexity.IsConvexSet.of_sConvexComb_mem
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : SetLike F M
inst_6 : AddSubmonoidClass F M
inst_7 : SMulMemClass F R M
inst_8 : ConvexSpace R M
inst_9 : IsModuleConvexSpace R M
S : F
refine : ∀ (w : StdSimplex R M) (hw : (↑w.weights.support : Set M) ⊆ (↑S : Set M)), sConvexComb w ∈ (↑S : Set M)
⊢ IsConvexSet R (↑S : Set M)

Tactic:
refine .of_sConvexComb_mem fun w hw ↦ ?_
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : SetLike F M
inst_6 : AddSubmonoidClass F M
inst_7 : SMulMemClass F R M
inst_8 : ConvexSpace R M
inst_9 : IsModuleConvexSpace R M
S : F
w : StdSimplex R M
hw : (↑w.weights.support : Set M) ⊆ (↑S : Set M)
rw : (w.weights.sum fun (m : M) (r : R) ↦ r • m) ∈ (↑S : Set M)
⊢ sConvexComb w ∈ (↑S : Set M)

Tactic:
rw [sConvexComb_eq_sum]

Premises used: Convexity.IsModuleConvexSpace.sConvexComb_eq_sum
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : SetLike F M
inst_6 : AddSubmonoidClass F M
inst_7 : SMulMemClass F R M
inst_8 : ConvexSpace R M
inst_9 : IsModuleConvexSpace R M
S : F
w : StdSimplex R M
hw : (↑w.weights.support : Set M) ⊆ (↑S : Set M)
m : M
hm : Ne.{u_2 + 1} (α := R) ((w.weights : (a : M) → R) m : R) (0 : R)
⊢ m ∈ (↑w.weights.support : Set M)

Tactic:
simpa
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : SetLike F M
inst_6 : AddSubmonoidClass F M
inst_7 : SMulMemClass F R M
inst_8 : ConvexSpace R M
inst_9 : IsModuleConvexSpace R M
S : F
w : StdSimplex R M
hw : (↑w.weights.support : Set M) ⊆ (↑S : Set M)
⊢ (w.weights.sum fun (m : M) (r : R) ↦ r • m) ∈ (↑S : Set M)

Tactic:
exact AddSubmonoidClass.finsuppSum_mem _ _ _ fun m hm ↦ SMulMemClass.smul_mem _ <| hw <| by simpa

Premises used: SMulMemClass.smul_mem, AddSubmonoidClass.finsuppSum_mem
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : SetLike F M
inst_6 : AddSubmonoidClass F M
inst_7 : SMulMemClass F R M
inst_8 : ConvexSpace R M
inst_9 : IsModuleConvexSpace R M
S : F
w : StdSimplex.{u_2, u_3} R ↥S
⊢ (↑(sConvexComb w) : M) = iConvexComb w (Subtype.val (p := fun (x : M) ↦ x ∈ S))

Tactic:
rfl

Premises used: Convexity.iConvexComb, rfl
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : SetLike F M
inst_6 : AddSubmonoidClass F M
inst_7 : SMulMemClass F R M
inst_8 : ConvexSpace R M
inst_9 : IsModuleConvexSpace R M
S : F
w : StdSimplex R I
f : I → ↥S
⊢ (↑(iConvexComb w f) : M) = iConvexComb w fun (i : I) ↦ (↑(f i) : M)

Tactic:
subtypeVal_iConvexComb ..

Premises used: Convexity.subtypeVal_iConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : SetLike F M
inst_6 : AddSubmonoidClass F M
inst_7 : SMulMemClass F R M
inst_8 : ConvexSpace R M
inst_9 : IsModuleConvexSpace R M
S : F
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x y : ↥S
⊢ (↑(convexCombPair a b ha hb hab x y) : M) = convexCombPair a b ha hb hab (↑x : M) (↑y : M)

Tactic:
subtypeVal_convexCombPair ..

Premises used: Convexity.subtypeVal_convexCombPair
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M
inst_8 : AddSubmonoidClass F M
inst_9 : SMulMemClass F R M
inst_10 : ConvexSpace R M
inst_11 : IsModuleConvexSpace R M
S : F
w : StdSimplex.{u_2, u_3} R ↥S
a : (↑(sConvexComb w) : M) = (↑(w.weights.sum fun (m : ↥S) (r : R) ↦ r • m) : M)
⊢ sConvexComb w = w.weights.sum fun (m : ↥S) (r : R) ↦ r • m

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M
inst_8 : AddSubmonoidClass F M
inst_9 : SMulMemClass F R M
inst_10 : ConvexSpace R M
inst_11 : IsModuleConvexSpace R M
S : F
w : StdSimplex.{u_2, u_3} R ↥S
⊢ (↑(sConvexComb w) : M) = (↑(w.weights.sum fun (m : ↥S) (r : R) ↦ r • m) : M)

Tactic:
simp [Finsupp.sum]

Premises used: Finsupp.sum
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M
inst_8 : AddSubmonoidClass F M
inst_9 : SMulMemClass F R M
inst_10 : ConvexSpace R M
inst_11 : IsModuleConvexSpace R M
inst_12 : ConvexSpace R N
inst_13 : IsModuleConvexSpace R N
w : StdSimplex R (M × N)
fst : (sConvexComb w).1 = (w.weights.sum fun (m : M × N) (r : R) ↦ r • m).1
snd : (sConvexComb w).2 = (w.weights.sum fun (m : M × N) (r : R) ↦ r • m).2
⊢ sConvexComb w = w.weights.sum fun (m : M × N) (r : R) ↦ r • m

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M
inst_8 : AddSubmonoidClass F M
inst_9 : SMulMemClass F R M
inst_10 : ConvexSpace R M
inst_11 : IsModuleConvexSpace R M
inst_12 : ConvexSpace R N
inst_13 : IsModuleConvexSpace R N
w : StdSimplex R (M × N)
⊢ (sConvexComb w).1 = (w.weights.sum fun (m : M × N) (r : R) ↦ r • m).1

Tactic:
simp [Finsupp.sum, Prod.fst_sum, Prod.snd_sum]

Premises used: Finsupp.sum, Prod.snd_sum, Prod.fst_sum
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M
inst_8 : AddSubmonoidClass F M
inst_9 : SMulMemClass F R M
inst_10 : ConvexSpace R M
inst_11 : IsModuleConvexSpace R M
inst_12 : ConvexSpace R N
inst_13 : IsModuleConvexSpace R N
w : StdSimplex R (M × N)
⊢ (sConvexComb w).2 = (w.weights.sum fun (m : M × N) (r : R) ↦ r • m).2

Tactic:
simp [Finsupp.sum, Prod.fst_sum, Prod.snd_sum]

Premises used: Finsupp.sum, Prod.snd_sum, Prod.fst_sum