awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M_1 : 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_1
inst_4 : Module R M_1
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M_1
inst_8 : AddSubmonoidClass F M_1
inst_9 : SMulMemClass F R M_1
inst_10 : ConvexSpace R M_1
inst_11 : IsModuleConvexSpace R M_1
ι : Type u_6
M : ι → Type u_7
inst_12 : (i : ι) → AddCommMonoid (M i)
inst_13 : (i : ι) → Module.{u_2, u_7} R (M i)
inst_14 : (i : ι) → ConvexSpace.{u_2, u_7} R (M i)
inst_15 : ∀ (i : ι), IsModuleConvexSpace.{u_2, u_7} R (M i)
w : StdSimplex R ((i : ι) → M i)
h : ∀ (x : ι), sConvexComb w x = w.weights.sum (fun (m : (i : ι) → M i) (r : R) ↦ r • m) x
⊢ sConvexComb w = w.weights.sum fun (m : (i : ι) → M i) (r : R) ↦ r • m

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
F : Type u_1
R : Type u_2
M_1 : 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_1
inst_4 : Module R M_1
inst_5 : AddCommMonoid N
inst_6 : Module R N
inst_7 : SetLike F M_1
inst_8 : AddSubmonoidClass F M_1
inst_9 : SMulMemClass F R M_1
inst_10 : ConvexSpace R M_1
inst_11 : IsModuleConvexSpace R M_1
ι : Type u_6
M : ι → Type u_7
inst_12 : (i : ι) → AddCommMonoid (M i)
inst_13 : (i : ι) → Module.{u_2, u_7} R (M i)
inst_14 : (i : ι) → ConvexSpace.{u_2, u_7} R (M i)
inst_15 : ∀ (i : ι), IsModuleConvexSpace.{u_2, u_7} R (M i)
w : StdSimplex R ((i : ι) → M i)
x : ι
⊢ sConvexComb w x = w.weights.sum (fun (m : (i : ι) → M i) (r : R) ↦ r • m) x

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
ι : Type u_6
w : StdSimplex R (ι →₀ M)
h :
  ∀ (a : ι),
    Eq.{u_3 + 1} (α := M) ((sConvexComb w : (a : ι) → M) a : M)
      ((w.weights.sum fun (m : ι →₀ M) (r : R) ↦ r • m : (a : ι) → M) a : M)
⊢ sConvexComb w = w.weights.sum fun (m : ι →₀ M) (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
ι : Type u_6
w : StdSimplex R (ι →₀ M)
a : ι
⊢ Eq.{u_3 + 1} (α := M) ((sConvexComb w : (a : ι) → M) a : M)
    ((w.weights.sum fun (m : ι →₀ M) (r : R) ↦ r • m : (a : ι) → M) a : M)

Tactic:
simp [Finsupp.sum]

Premises used: Finsupp.sum
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Module
Goal:
R : Type u_2
I : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
s : StdSimplex R (StdSimplex R I)
⊢ (sConvexComb s).weights = sConvexComb (map weights s)

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

Premises used: Convexity.IsModuleConvexSpace.sConvexComb_eq_sum, Finsupp.sum_mapDomain_index, add_smul
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
X : Type u_3
Y : Type u_4
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
⊢ ∀ (x : X × Y), (fun (w : StdSimplex R (X × Y)) ↦ (iConvexComb w fst, iConvexComb w snd)) (StdSimplex.single x) = x

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
X : Type u_3
Y : Type u_4
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
⊢ ∀ (f : StdSimplex R (StdSimplex R (X × Y))),
    Eq (α := X × Y)
      ((fun (w : StdSimplex R (X × Y)) ↦ (iConvexComb w fst, iConvexComb w snd))
        (StdSimplex.map (fun (w : StdSimplex R (X × Y)) ↦ (iConvexComb w fst, iConvexComb w snd)) f))
      ((fun (w : StdSimplex R (X × Y)) ↦ (iConvexComb w fst, iConvexComb w snd)) (sConvexComb f))

Tactic:
simp [iConvexComb_assoc]

Premises used: Convexity.iConvexComb_assoc
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
X : Type u_3
Y : Type u_4
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
w : StdSimplex R (X × Y)
⊢ (sConvexComb w).1 = iConvexComb w fst

Tactic:
rfl

Premises used: Convexity.iConvexComb, rfl
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
X : Type u_3
Y : Type u_4
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
w : StdSimplex R (X × Y)
⊢ (sConvexComb w).2 = iConvexComb w snd

Tactic:
rfl

Premises used: Convexity.iConvexComb, rfl
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
X : Type u_3
Y : Type u_4
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
w : StdSimplex R I
f : I → X × Y
⊢ (iConvexComb w f).1 = iConvexComb w fun (i : I) ↦ (f i).1

Tactic:
isAffineMap_fst.map_iConvexComb ..

Premises used: Prod.isAffineMap_fst, Convexity.IsAffineMap.map_iConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
X : Type u_3
Y : Type u_4
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
w : StdSimplex R I
f : I → X × Y
⊢ (iConvexComb w f).2 = iConvexComb w fun (i : I) ↦ (f i).2

Tactic:
isAffineMap_snd.map_iConvexComb ..

Premises used: Convexity.IsAffineMap.map_iConvexComb, Prod.isAffineMap_snd
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
X : Type u_3
Y : Type u_4
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x y : X × Y
⊢ (convexCombPair a b ha hb hab x y).1 = convexCombPair a b ha hb hab x.1 y.1

Tactic:
isAffineMap_fst.map_convexCombPair ..

Premises used: Convexity.IsAffineMap.map_convexCombPair, Prod.isAffineMap_fst
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
X : Type u_3
Y : Type u_4
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x y : X × Y
⊢ (convexCombPair a b ha hb hab x y).2 = convexCombPair a b ha hb hab x.2 y.2

Tactic:
isAffineMap_snd.map_convexCombPair ..

Premises used: Convexity.IsAffineMap.map_convexCombPair, Prod.isAffineMap_snd
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : ι → Type u_4
inst_3 : (i : ι) → ConvexSpace.{u_2, u_4} R (X i)
i : ι
⊢ ∀ (x : (i : ι) → X i),
    (fun (w : StdSimplex R ((i : ι) → X i)) (i : ι) ↦ (iConvexComb w fun (x : (i : ι) → X i) ↦ x i : X i))
        (StdSimplex.single x) =
      x

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : ι → Type u_4
inst_3 : (i : ι) → ConvexSpace.{u_2, u_4} R (X i)
i : ι
⊢ ∀ (f : StdSimplex R (StdSimplex R ((i : ι) → X i))),
    Eq (α := (i : ι) → X i)
      ((fun (w : StdSimplex R ((i : ι) → X i)) (i : ι) ↦ (iConvexComb w fun (x : (i : ι) → X i) ↦ x i : X i))
        (StdSimplex.map (fun (w : StdSimplex R ((i : ι) → X i)) (i : ι) ↦ iConvexComb w fun (x : (i : ι) → X i) ↦ x i)
          f))
      ((fun (w : StdSimplex R ((i : ι) → X i)) (i : ι) ↦ (iConvexComb w fun (x : (i : ι) → X i) ↦ x i : X i))
        (sConvexComb f))

Tactic:
simp [iConvexComb_assoc]

Premises used: Convexity.iConvexComb_assoc
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : ι → Type u_4
inst_3 : (i : ι) → ConvexSpace.{u_2, u_4} R (X i)
w : StdSimplex R ((i : ι) → X i)
i : ι
⊢ sConvexComb w i = iConvexComb w fun (x : (i : ι) → X i) ↦ x i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : ι → Type u_4
inst_3 : (i : ι) → ConvexSpace.{u_2, u_4} R (X i)
w : StdSimplex R I
f : I → (i : ι) → X i
i : ι
⊢ iConvexComb w f i = iConvexComb w fun (j : I) ↦ f j i

Tactic:
isAffineMap_eval.map_iConvexComb ..

Premises used: Convexity.IsAffineMap.map_iConvexComb, Pi.isAffineMap_eval
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : ι → Type u_4
inst_3 : (i : ι) → ConvexSpace.{u_2, u_4} R (X i)
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
f g : (i : ι) → X i
i : ι
⊢ convexCombPair a b ha hb hab f g i = convexCombPair a b ha hb hab (f i) (g i)

Tactic:
isAffineMap_eval.map_convexCombPair ..

Premises used: Convexity.IsAffineMap.map_convexCombPair, Pi.isAffineMap_eval
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
i : ι
w : StdSimplex R (ι →₀ X)
refine :
  ∀ (a : ι),
    Ne.{u_4 + 1} (α := X) ((fun (i : ι) ↦ (iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i : X)) a) 0 →
      a ∈ w.weights.support.biUnion support
⊢ ι →₀ X

Tactic:
refine .onFinset (w.weights.support.biUnion Finsupp.support) (fun i ↦ w.iConvexComb (· i)) ?_
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
i_1 : ι
w : StdSimplex R (ι →₀ X)
i : ι
hi : Ne.{u_4 + 1} (α := X) ((fun (i : ι) ↦ (iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i : X)) i) 0
contrapose! :
  ∀ (hi : i ∉ w.weights.support.biUnion support),
    Eq.{u_4 + 1} (α := X) (iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) 0
⊢ i ∈ w.weights.support.biUnion support

Tactic:
contrapose! hi
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
i_1 : ι
w : StdSimplex R (ι →₀ X)
i : ι
hi : i ∉ w.weights.support.biUnion support
⊢ Eq.{u_4 + 1} (α := X) (iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) 0

Tactic:
simp_all
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
i : ι
w : StdSimplex R (ι →₀ X)
refine refine₁ :
  ∀ (i : ι)
    (hi : Ne.{u_4 + 1} (α := X) ((fun (i : ι) ↦ (iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i : X)) i) 0),
    i ∈ w.weights.support.biUnion support
refine₂ :
  ∀ (i : ι) (hi : i ∉ w.weights.support.biUnion support),
    Eq.{u_4 + 1} (α := X) (iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) 0
⊢ ι →₀ X

Tactic:
classical
    refine .onFinset (w.weights.support.biUnion Finsupp.support) (fun i ↦ w.iConvexComb (· i)) ?_
    rintro i hi
    contrapose! hi
    simp_all
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
i : ι
⊢ ∀ (x : ι →₀ X),
    (fun (w : StdSimplex R (ι →₀ X)) ↦
          (onFinset (w.weights.support.biUnion support)
              (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) ⋯ :
            ι →₀ X))
        (StdSimplex.single x) =
      x

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
i : ι
w : StdSimplex R (StdSimplex R (ι →₀ X))
h :
  ∀ (a : ι),
    Eq.{u_4 + 1} (α := X)
      (((fun (w : StdSimplex R (ι →₀ X)) ↦
                (onFinset (w.weights.support.biUnion support)
                    (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) ⋯ :
                  ι →₀ X))
              (StdSimplex.map
                (fun (w : StdSimplex R (ι →₀ X)) ↦
                  onFinset (w.weights.support.biUnion support)
                    (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) ⋯)
                w) :
            (a : ι) → X)
          a :
        X)
      (((fun (w : StdSimplex R (ι →₀ X)) ↦
                (onFinset (w.weights.support.biUnion support)
                    (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) ⋯ :
                  ι →₀ X))
              (sConvexComb w) :
            (a : ι) → X)
          a :
        X)
⊢ Eq (α := ι →₀ X)
    ((fun (w : StdSimplex R (ι →₀ X)) ↦
        (onFinset (w.weights.support.biUnion support)
            (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) ⋯ :
          ι →₀ X))
      (StdSimplex.map
        (fun (w : StdSimplex R (ι →₀ X)) ↦
          onFinset (w.weights.support.biUnion support)
            (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) ⋯)
        w))
    ((fun (w : StdSimplex R (ι →₀ X)) ↦
        (onFinset (w.weights.support.biUnion support)
            (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) ⋯ :
          ι →₀ X))
      (sConvexComb w))

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
i : ι
w : StdSimplex R (StdSimplex R (ι →₀ X))
a : ι
⊢ Eq.{u_4 + 1} (α := X)
    (((fun (w : StdSimplex R (ι →₀ X)) ↦
              (onFinset (w.weights.support.biUnion support)
                  (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) ⋯ :
                ι →₀ X))
            (StdSimplex.map
              (fun (w : StdSimplex R (ι →₀ X)) ↦
                onFinset (w.weights.support.biUnion support)
                  (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) ⋯)
              w) :
          (a : ι) → X)
        a :
      X)
    (((fun (w : StdSimplex R (ι →₀ X)) ↦
              (onFinset (w.weights.support.biUnion support)
                  (fun (i : ι) ↦ iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i) ⋯ :
                ι →₀ X))
            (sConvexComb w) :
          (a : ι) → X)
        a :
      X)

Tactic:
simp [iConvexComb_assoc]

Premises used: Convexity.iConvexComb_assoc
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
w : StdSimplex R (ι →₀ X)
i : ι
⊢ Eq.{u_4 + 1} (α := X) ((sConvexComb w : (a : ι) → X) i : X) (iConvexComb w fun (x : ι →₀ X) ↦ (x : (a : ι) → X) i : X)

Tactic:
rfl

Premises used: Convexity.iConvexComb, rfl
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
I : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
w : StdSimplex R I
f : I → ι →₀ X
i : ι
⊢ Eq.{u_4 + 1} (α := X) ((iConvexComb w f : (a : ι) → X) i : X) (iConvexComb w fun (j : I) ↦ (f j : (a : ι) → X) i : X)

Tactic:
isAffineMap_eval.map_iConvexComb ..

Premises used: Finsupp.isAffineMap_eval, Convexity.IsAffineMap.map_iConvexComb
-- Module: Mathlib.Geometry.Convex.ConvexSpace.Prod
Goal:
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
ι : Type u_3
X : Type u_4
inst_3 : Zero X
inst_4 : ConvexSpace R X
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
f g : ι →₀ X
i : ι
⊢ Eq.{u_4 + 1} (α := X) ((convexCombPair a b ha hb hab f g : (a : ι) → X) i : X)
    (convexCombPair a b ha hb hab ((f : (a : ι) → X) i) ((g : (a : ι) → X) i) : X)

Tactic:
isAffineMap_eval.map_convexCombPair ..

Premises used: Convexity.IsAffineMap.map_convexCombPair, Finsupp.isAffineMap_eval
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
hs : ∀ (w : StdSimplex R X), (↑w.weights.support : Set X) ⊆ s → sConvexComb w ∈ s
⊢ IsConvexSet R s

Tactic:
hs

Premises used: Convexity.IsConvexSet
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
w : StdSimplex R X
s : Set X
hs : IsConvexSet R s
hw : (↑w.weights.support : Set X) ⊆ s
⊢ sConvexComb w ∈ s

Tactic:
hs hw
-- Module: Mathlib.Geometry.Convex.Set
Goal:
ι : Type u_1
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R ι
f : ι → X
hf : ∀ (i : ι), Ne.{u_3 + 1} (α := R) ((w.weights : (a : ι) → R) i : R) (0 : R) → f i ∈ s
⊢ iConvexComb w f ∈ s

Tactic:
hs ?_

Premises used: Set.Mem, Convexity.iConvexComb
-- Module: Mathlib.Geometry.Convex.Set
Goal:
ι : Type u_1
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R ι
f : ι → X
hf : ∀ (i : ι), Ne.{u_3 + 1} (α := R) ((w.weights : (a : ι) → R) i : R) (0 : R) → f i ∈ s
refine : (↑(StdSimplex.map f w).weights.support : Set X) ⊆ s
⊢ iConvexComb w f ∈ s

Tactic:
refine hs ?_
-- Module: Mathlib.Geometry.Convex.Set
Goal:
ι : Type u_1
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R ι
f : ι → X
hf : ∀ (i : ι), Ne.{u_3 + 1} (α := R) ((w.weights : (a : ι) → R) i : R) (0 : R) → f i ∈ s
grw : (↑(Finset.image f w.weights.support) : Set X) ⊆ s
⊢ (↑(StdSimplex.map f w).weights.support : Set X) ⊆ s

Tactic:
grw [StdSimplex.weights_map, mapDomain_support]

Premises used: Finsupp.mapDomain_support, Convexity.StdSimplex.weights_map
-- Module: Mathlib.Geometry.Convex.Set
Goal:
ι : Type u_1
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R ι
f : ι → X
hf : ∀ (i : ι), Ne.{u_3 + 1} (α := R) ((w.weights : (a : ι) → R) i : R) (0 : R) → f i ∈ s
⊢ (↑(Finset.image f w.weights.support) : Set X) ⊆ s

Tactic:
simpa [subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.Geometry.Convex.Set
Goal:
ι : Type u_1
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R ι
f : ι → X
hf : ∀ (i : ι), Ne.{u_3 + 1} (α := R) ((w.weights : (a : ι) → R) i : R) (0 : R) → f i ∈ s
refine : (↑(StdSimplex.map f w).weights.support : Set X) ⊆ s
refine₁ : (↑(Finset.image f w.weights.support) : Set X) ⊆ s
⊢ iConvexComb w f ∈ s

Tactic:
classical
  refine hs ?_
  grw [StdSimplex.weights_map, mapDomain_support]
  simpa [subset_def]

Premises used: Set.subset_def, Finsupp.mapDomain_support, Convexity.StdSimplex.weights_map
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
x y : X
hs : IsConvexSet R s
hx : x ∈ s
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ convexCombPair a b ha hb hab x y ∈ s

Tactic:
hs.sConvexComb_mem ?_

Premises used: Set.Mem, Convexity.IsConvexSet.sConvexComb_mem, Convexity.convexCombPair
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
x y : X
hs : IsConvexSet R s
hx : x ∈ s
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine : (↑(StdSimplex.duple x y ha hb hab).weights.support : Set X) ⊆ s
⊢ convexCombPair a b ha hb hab x y ∈ s

Tactic:
refine hs.sConvexComb_mem ?_

Premises used: Convexity.IsConvexSet.sConvexComb_mem
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
x y : X
hs : IsConvexSet R s
hx : x ∈ s
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
grw : (↑({x} ∪ {y}) : Set X) ⊆ s
⊢ (↑(StdSimplex.duple x y ha hb hab).weights.support : Set X) ⊆ s

Tactic:
grw [StdSimplex.weights_duple, support_add, support_single_subset, support_single_subset]

Premises used: Convexity.StdSimplex.weights_duple, Finsupp.support_add, Finsupp.support_single_subset
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
x y : X
hs : IsConvexSet R s
hx : x ∈ s
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (↑({x} ∪ {y}) : Set X) ⊆ s

Tactic:
simp [*, insert_subset_iff]

Premises used: Set.insert_subset_iff
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
x y : X
hs : IsConvexSet R s
hx : x ∈ s
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine : (↑(StdSimplex.duple x y ha hb hab).weights.support : Set X) ⊆ s
refine₁ : (↑({x} ∪ {y}) : Set X) ⊆ s
⊢ convexCombPair a b ha hb hab x y ∈ s

Tactic:
classical
  refine hs.sConvexComb_mem ?_
  grw [StdSimplex.weights_duple, support_add, support_single_subset, support_single_subset]
  simp [*, insert_subset_iff]

Premises used: Convexity.StdSimplex.weights_duple, Convexity.IsConvexSet.sConvexComb_mem, Set.insert_subset_iff, Finsupp.support_add, Finsupp.support_single_subset
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
⊢ IsConvexSet.{u_3, u_5} R (X := X) ∅

Tactic:
simp [IsConvexSet]

Premises used: Convexity.IsConvexSet
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
⊢ IsConvexSet.{u_3, u_5} R (X := X) univ

Tactic:
simp [IsConvexSet]

Premises used: Convexity.IsConvexSet
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
x : X
⊢ IsConvexSet R (X := X) {x}

Tactic:
simp [IsConvexSet, -subset_singleton_iff, Finset.coe_subset_singleton]

Premises used: Set.subset_singleton_iff, Convexity.IsConvexSet, Finset.coe_subset_singleton
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
s : Set X
hs : s.Subsingleton
inl : ∀ (hs : Set.Subsingleton.{u_5} (α := X) ∅), IsConvexSet.{u_3, u_5} R (X := X) ∅
inr : ∀ (x : X) (hs : Set.Subsingleton (α := X) {x}), IsConvexSet R (X := X) {x}
⊢ IsConvexSet R s

Tactic:
obtain rfl | ⟨x, rfl⟩ := hs.eq_empty_or_singleton

Premises used: Set.Subsingleton.eq_empty_or_singleton, rfl
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
hs : Set.Subsingleton.{u_5} (α := X) ∅
⊢ IsConvexSet.{u_3, u_5} R (X := X) ∅

Tactic:
simp