awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
Y : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : (↑w.weights.support : Set Y) ⊆ f '' s
u : Finset X
hus : (↑u : Set X) ⊆ s
hfu : InjOn f (↑u : Set X)
huw : Finset.image f u = w.weights.support
x : X
hx : x ∈ u
⊢ Eq.{u_3 + 1} (α := R) ((w.weights : (a : Y) → R) (f x) : R)
    ((onFinset u (fun (x : X) ↦ if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0) ⋯ : (a : X) → R) x : R)

Tactic:
(if_pos hx).symm

Premises used: if_pos, Eq.symm, ite
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
Y : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : (↑w.weights.support : Set Y) ⊆ f '' s
u : Finset X
hus : (↑u : Set X) ⊆ s
hfu : InjOn f (↑u : Set X)
huw : Finset.image f u = w.weights.support
x : X
hx : x ∈ u
⊢ Eq.{u_3 + 1} (α := R) ((w.weights : (a : Y) → R) (f x) : R)
    ((onFinset u (fun (x : X) ↦ if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0) ⋯ : (a : X) → R) x : R)

Tactic:
exact (if_pos hx).symm

Premises used: if_pos, Eq.symm
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
Y : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : (↑w.weights.support : Set Y) ⊆ f '' s
u : Finset X
hus : (↑u : Set X) ⊆ s
hfu : InjOn f (↑u : Set X)
huw : Finset.image f u = w.weights.support
y : Y
hy : y ∉ w.weights.support
simp :
  ∀ (hy : ∀ x ∈ u, ¬f x = y), ∀ x ∈ u, ¬Eq.{u_3 + 1} (α := R) ((w.weights : (a : Y) → R) (f x) : R) (0 : R) → ¬f x = y
⊢ y ∉
    f ''
      (↑(support.{u_5, u_3} (M := R)
            (StdSimplex.weights
              { weights := onFinset u (fun (x : X) ↦ if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0) ⋯,
                nonneg := ⋯, total := ⋯ : StdSimplex R X })) :
        Set X)

Tactic:
simp [← huw] at ⊢ hy
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
Y : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : (↑w.weights.support : Set Y) ⊆ f '' s
u : Finset X
hus : (↑u : Set X) ⊆ s
hfu : InjOn f (↑u : Set X)
huw : Finset.image f u = w.weights.support
y : Y
hy : ∀ x ∈ u, ¬f x = y
tauto tauto₁ tauto₂ tauto₃ tauto₄ :
  ∀ x ∈ u, ¬Eq.{u_3 + 1} (α := R) ((w.weights : (a : Y) → R) (f x) : R) (0 : R) → ¬f x = y
tauto₅ tauto₆ tauto₇ tauto₈ tauto₉ tauto₁₀ :
  ∀ x ∈ u, ¬Eq.{u_3 + 1} (α := R) ((w.weights : (a : Y) → R) (f x) : R) (0 : R) → f x = y → False
⊢ ∀ x ∈ u, ¬Eq.{u_3 + 1} (α := R) ((w.weights : (a : Y) → R) (f x) : R) (0 : R) → ¬f x = y

Tactic:
tauto
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
Y : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : (↑w.weights.support : Set Y) ⊆ f '' s
u : Finset X
hus : (↑u : Set X) ⊆ s
hfu : InjOn f (↑u : Set X)
huw : Finset.image f u = w.weights.support
y : Y
hy : y ∉ w.weights.support
neg : Eq.{u_3 + 1} (α := R) (0 : R) ((w.weights : (a : Y) → R) y : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((mapDomain f
            (StdSimplex.weights
              { weights := onFinset u (fun (x : X) ↦ if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0) ⋯,
                nonneg := ⋯, total := ⋯ }) :
          (a : Y) → R)
        y :
      R)
    ((w.weights : (a : Y) → R) y : R)

Tactic:
rw [mapDomain_of_not_mem_image_support (by simp [← huw] at ⊢ hy; tauto)]

Premises used: Finsupp.mapDomain_of_not_mem_image_support
-- Module: Mathlib.Geometry.Convex.Set
Goal:
R : Type u_3
X : Type u_5
Y : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
f : X → Y
s : Set X
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R Y
hw : (↑w.weights.support : Set Y) ⊆ f '' s
u : Finset X
hus : (↑u : Set X) ⊆ s
hfu : InjOn f (↑u : Set X)
huw : Finset.image f u = w.weights.support
y : Y
hy : y ∉ w.weights.support
⊢ Eq.{u_3 + 1} (α := R) (0 : R) ((w.weights : (a : Y) → R) y : R)

Tactic:
simp_all
-- Module: Mathlib.Geometry.Convex.Set
Goal:
ι : Type u_1
I : Type u_2
R : Type u_3
K : Type u_4
X : Type u_5
Y : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
f : X → Y
w_1 : StdSimplex R X
s_1 t : Set X
x y : X
s : Set X
hs : IsConvexSet R s
w : StdSimplex.{u_3, u_5} R (↑s : Type u_5)
⊢ ∀ (i : (↑s : Type u_5)), Ne.{u_3 + 1} (α := R) ((w.weights : (a : (↑s : Type u_5)) → R) i : R) (0 : R) → (↑i : X) ∈ s

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Set
Goal:
ι : Type u_1
I : Type u_2
R : Type u_3
K : Type u_4
X : Type u_5
Y : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
f : X → Y
w : StdSimplex R X
s_1 t : Set X
x_1 y : X
s : Set X
hs : IsConvexSet R s
x : (↑s : Type u_5)
⊢ (fun (w : StdSimplex.{u_3, u_5} R (↑s : Type u_5)) ↦
        Subtype.mk (p := fun (x : X) ↦ x ∈ s) (iConvexComb w (Subtype.val (p := fun (x : X) ↦ x ∈ s))) ⋯)
      (StdSimplex.single x) =
    x

Tactic:
simp
-- Module: Mathlib.Geometry.Convex.Set
Goal:
ι : Type u_1
I : Type u_2
R : Type u_3
K : Type u_4
X : Type u_5
Y : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
f : X → Y
w_1 : StdSimplex R X
s_1 t : Set X
x y : X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R (StdSimplex.{u_3, u_5} R (↑s : Type u_5))
a :
  Eq.{u_5 + 1} (α := X)
    (↑((fun (w : StdSimplex.{u_3, u_5} R (↑s : Type u_5)) ↦
            Subtype.mk (p := fun (x : X) ↦ x ∈ s) (iConvexComb w (Subtype.val (p := fun (x : X) ↦ x ∈ s))) ⋯)
          (StdSimplex.map
            (fun (w : StdSimplex.{u_3, u_5} R (↑s : Type u_5)) ↦
              Subtype.mk (p := fun (x : X) ↦ x ∈ s) (iConvexComb w (Subtype.val (p := fun (x : X) ↦ x ∈ s))) ⋯)
            w)) :
      X)
    (↑((fun (w : StdSimplex.{u_3, u_5} R (↑s : Type u_5)) ↦
            Subtype.mk (p := fun (x : X) ↦ x ∈ s) (iConvexComb w (Subtype.val (p := fun (x : X) ↦ x ∈ s))) ⋯)
          (sConvexComb w)) :
      X)
⊢ Eq.{u_5 + 1} (α := (↑s : Type u_5))
    ((fun (w : StdSimplex.{u_3, u_5} R (↑s : Type u_5)) ↦
        Subtype.mk (p := fun (x : X) ↦ x ∈ s) (iConvexComb w (Subtype.val (p := fun (x : X) ↦ x ∈ s))) ⋯)
      (StdSimplex.map
        (fun (w : StdSimplex.{u_3, u_5} R (↑s : Type u_5)) ↦
          Subtype.mk (p := fun (x : X) ↦ x ∈ s) (iConvexComb w (Subtype.val (p := fun (x : X) ↦ x ∈ s))) ⋯)
        w))
    ((fun (w : StdSimplex.{u_3, u_5} R (↑s : Type u_5)) ↦
        Subtype.mk (p := fun (x : X) ↦ x ∈ s) (iConvexComb w (Subtype.val (p := fun (x : X) ↦ x ∈ s))) ⋯)
      (sConvexComb w))

Tactic:
ext
-- Module: Mathlib.Geometry.Convex.Set
Goal:
ι : Type u_1
I : Type u_2
R : Type u_3
K : Type u_4
X : Type u_5
Y : Type u_6
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ConvexSpace R X
inst_4 : ConvexSpace R Y
f : X → Y
w_1 : StdSimplex R X
s_1 t : Set X
x y : X
s : Set X
hs : IsConvexSet R s
w : StdSimplex R (StdSimplex.{u_3, u_5} R (↑s : Type u_5))
⊢ Eq.{u_5 + 1} (α := X)
    (↑((fun (w : StdSimplex.{u_3, u_5} R (↑s : Type u_5)) ↦
            Subtype.mk (p := fun (x : X) ↦ x ∈ s) (iConvexComb w (Subtype.val (p := fun (x : X) ↦ x ∈ s))) ⋯)
          (StdSimplex.map
            (fun (w : StdSimplex.{u_3, u_5} R (↑s : Type u_5)) ↦
              Subtype.mk (p := fun (x : X) ↦ x ∈ s) (iConvexComb w (Subtype.val (p := fun (x : X) ↦ x ∈ s))) ⋯)
            w)) :
      X)
    (↑((fun (w : StdSimplex.{u_3, u_5} R (↑s : Type u_5)) ↦
            Subtype.mk (p := fun (x : X) ↦ x ∈ s) (iConvexComb w (Subtype.val (p := fun (x : X) ↦ x ∈ s))) ⋯)
          (sConvexComb w)) :
      X)

Tactic:
simp [iConvexComb_assoc]

Premises used: Convexity.iConvexComb_assoc
-- 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 : IsConvexSet R s
⊢ IsAffineMap.{u_3, u_5, u_5} R (M := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s))

Tactic:
letI : ConvexSpace R s := .subtype s hs
  ⟨fun _ ↦ rfl⟩

Premises used: Convexity.IsAffineMap.mk, 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
s : Set X
hs : IsConvexSet R s
w : StdSimplex.{u_3, u_5} R (↑s : Type u_5)
⊢ (↑(sConvexComb w) : X) = iConvexComb w (Subtype.val (p := fun (x : X) ↦ x ∈ s))

Tactic:
rfl

Premises used: Convexity.iConvexComb, rfl
-- Module: Mathlib.Geometry.Convex.Set
Goal:
I : Type u_2
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 I
f : I → (↑s : Type u_5)
⊢ (↑(iConvexComb w f) : X) = iConvexComb w fun (i : I) ↦ (↑(f i) : X)

Tactic:
letI : ConvexSpace R s := .subtype s hs
  (isAffineMap_subtypeVal ..).map_iConvexComb ..

Premises used: Convexity.isAffineMap_subtypeVal, Convexity.IsAffineMap.map_iConvexComb
-- 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 : IsConvexSet R s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x y : (↑s : Type u_5)
⊢ (↑(convexCombPair a b ha hb hab x y) : X) = convexCombPair a b ha hb hab (↑x : X) (↑y : X)

Tactic:
letI : ConvexSpace R s := .subtype s hs
  (isAffineMap_subtypeVal ..).map_convexCombPair ..

Premises used: Convexity.isAffineMap_subtypeVal, Convexity.IsAffineMap.map_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
Y : Type u_7
inst_4 : ConvexSpace R Y
t : Set Y
hs : IsConvexSet R s
ht : IsConvexSet R t
w : StdSimplex R (X × Y)
hw : (↑w.weights.support : Set (X × Y)) ⊆ s ×ˢ t
⊢ sConvexComb w ∈ s ×ˢ t

Tactic:
⟨hs ?_, ht ?_⟩

Premises used: Set.Mem, setOf, Set.prod, And.intro
-- 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
Y : Type u_7
inst_4 : ConvexSpace R Y
t : Set Y
hs : IsConvexSet R s
ht : IsConvexSet R t
w : StdSimplex R (X × Y)
hw : (↑w.weights.support : Set (X × Y)) ⊆ s ×ˢ t
refine_1 : (↑(StdSimplex.map Prod.fst w).weights.support : Set X) ⊆ s
refine_2 : (↑(StdSimplex.map Prod.snd w).weights.support : Set Y) ⊆ t
⊢ sConvexComb w ∈ s ×ˢ t

Tactic:
refine ⟨hs ?_, ht ?_⟩
-- 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
Y : Type u_7
inst_4 : ConvexSpace R Y
t : Set Y
hs : IsConvexSet R s
ht : IsConvexSet R t
w : StdSimplex R (X × Y)
hw : (↑w.weights.support : Set (X × Y)) ⊆ s ×ˢ t
refine_1 : (↑(mapDomain Prod.fst w.weights).support : Set X) ⊆ s
refine_1₁ : (↑(Finset.image Prod.fst w.weights.support) : Set X) ⊆ s
refine_1₂ : Prod.fst '' (↑w.weights.support : Set (X × Y)) ⊆ s
refine_1₃ : Prod.fst '' s ×ˢ t ⊆ s
refine_1₄ refine_1₅ : s ⊆ s
⊢ (↑(StdSimplex.map Prod.fst w).weights.support : Set X) ⊆ s

Tactic:
grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, fst_image_prod_subset]

Premises used: Finsupp.mapDomain_support, Convexity.StdSimplex.weights_map, Finset.coe_image, Set.fst_image_prod_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
Y : Type u_7
inst_4 : ConvexSpace R Y
t : Set Y
hs : IsConvexSet R s
ht : IsConvexSet R t
w : StdSimplex R (X × Y)
hw : (↑w.weights.support : Set (X × Y)) ⊆ s ×ˢ t
refine_2 : (↑(mapDomain Prod.snd w.weights).support : Set Y) ⊆ t
refine_2₁ : (↑(Finset.image Prod.snd w.weights.support) : Set Y) ⊆ t
refine_2₂ : Prod.snd '' (↑w.weights.support : Set (X × Y)) ⊆ t
refine_2₃ : Prod.snd '' s ×ˢ t ⊆ t
refine_2₄ refine_2₅ : t ⊆ t
⊢ (↑(StdSimplex.map Prod.snd w).weights.support : Set Y) ⊆ t

Tactic:
grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, snd_image_prod_subset]

Premises used: Set.snd_image_prod_subset, Finsupp.mapDomain_support, Convexity.StdSimplex.weights_map, Finset.coe_image
-- Module: Mathlib.Geometry.Convex.Set
Goal:
ι : Type u_1
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
X : ι → Type u_7
inst_3 : (i : ι) → ConvexSpace.{u_3, u_7} R (X i)
s : Set ι
t : (i : ι) → Set (X i)
ht : ∀ i ∈ s, IsConvexSet R (t i)
⊢ IsConvexSet R (s.pi (α := X) t)

Tactic:
fun w hw i hi ↦ ht i hi ?_

Premises used: Set.Mem, setOf, Convexity.iConvexComb, Set.pi, Convexity.IsConvexSet
-- Module: Mathlib.Geometry.Convex.Set
Goal:
ι : Type u_1
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
X : ι → Type u_7
inst_3 : (i : ι) → ConvexSpace.{u_3, u_7} R (X i)
s : Set ι
t : (i : ι) → Set (X i)
ht : ∀ i ∈ s, IsConvexSet R (t i)
refine :
  ∀ (w : StdSimplex R ((i : ι) → X i)) (hw : (↑w.weights.support : Set ((i : ι) → X i)) ⊆ s.pi (α := X) t) (i : ι)
    (hi : i ∈ s), (↑(support (StdSimplex.weights (StdSimplex.map (fun (x : (i : ι) → X i) ↦ x i) w))) : Set (X i)) ⊆ t i
⊢ IsConvexSet R (s.pi (α := X) t)

Tactic:
refine fun w hw i hi ↦ ht i hi ?_
-- Module: Mathlib.Geometry.Convex.Set
Goal:
ι : Type u_1
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
X : ι → Type u_7
inst_3 : (i : ι) → ConvexSpace.{u_3, u_7} R (X i)
s : Set ι
t : (i : ι) → Set (X i)
ht : ∀ i ∈ s, IsConvexSet R (t i)
w : StdSimplex R ((i : ι) → X i)
hw : (↑w.weights.support : Set ((i : ι) → X i)) ⊆ s.pi (α := X) t
i : ι
hi : i ∈ s
grw : (↑(support (mapDomain (fun (x : (i : ι) → X i) ↦ x i) w.weights)) : Set (X i)) ⊆ t i
grw₁ : (↑(Finset.image (fun (x : (i : ι) → X i) ↦ x i) w.weights.support) : Set (X i)) ⊆ t i
grw₂ : (fun (x : (i : ι) → X i) ↦ x i) '' (↑w.weights.support : Set ((i : ι) → X i)) ⊆ t i
grw₃ : (fun (x : (i : ι) → X i) ↦ x i) '' s.pi (α := X) t ⊆ t i
grw₄ grw₅ : t i ⊆ t i
⊢ (↑(support (StdSimplex.weights (StdSimplex.map (fun (x : (i : ι) → X i) ↦ x i) w))) : Set (X i)) ⊆ t i

Tactic:
grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, eval_image_pi_subset hi]

Premises used: Set.eval_image_pi_subset, Finsupp.mapDomain_support, Convexity.StdSimplex.weights_map, Finset.coe_image
-- Module: Mathlib.Geometry.Convex.Set
Goal:
ι : Type u_1
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
X : ι → Type u_7
inst_3 : (i : ι) → ConvexSpace.{u_3, u_7} R (X i)
s : Set ι
t : (i : ι) → Set (X i)
ht : ∀ i ∈ s, IsConvexSet R (t i)
refine :
  ∀ (w : StdSimplex R ((i : ι) → X i)) (hw : (↑w.weights.support : Set ((i : ι) → X i)) ⊆ s.pi (α := X) t) (i : ι)
    (hi : i ∈ s), (↑(support (StdSimplex.weights (StdSimplex.map (fun (x : (i : ι) → X i) ↦ x i) w))) : Set (X i)) ⊆ t i
⊢ IsConvexSet R (s.pi (α := X) t)

Tactic:
classical
  refine fun w hw i hi ↦ ht i hi ?_
  grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, eval_image_pi_subset hi]

Premises used: Finsupp.mapDomain_support, Convexity.StdSimplex.weights_map, Finset.coe_image
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
w : StdSimplex K X
hw : (↑w.weights.support : Set X) ⊆ s
⊢ let t := w.weights.support;
  (↑t : Set X) ⊆ s

Tactic:
set t := w.weights.support with hsw

Premises used: Finsupp.support, Convexity.StdSimplex.weights
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
w : StdSimplex K X
hw : (↑w.weights.support : Set X) ⊆ s
hw₁ :
  let t := w.weights.support;
  (↑t : Set X) ⊆ s
⊢ let t := w.weights.support;
  t = w.weights.support

Tactic:
set t := w.weights.support with hsw

Premises used: Finsupp.support, Convexity.StdSimplex.weights
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
w : StdSimplex K X
t : Finset X := w.weights.support
hw : (↑t : Set X) ⊆ s
hsw : t = w.weights.support
⊢ t.Nonempty

Tactic:
have ht : t.Nonempty := w.support_weights_nonempty
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
w : StdSimplex K X
t : Finset X := w.weights.support
hw : (↑t : Set X) ⊆ s
hsw : t = w.weights.support
ht : t.Nonempty
clear_value :
  ∀ (t : Finset X) (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support) (ht : t.Nonempty), sConvexComb w ∈ s
⊢ sConvexComb w ∈ s

Tactic:
clear_value t
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t : Finset X
x : X
w : StdSimplex K X
hw : (↑{x} : Set X) ⊆ s
hsw : {x} = w.weights.support
⊢ sConvexComb w ∈ s

Tactic:
simp_all [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t_1 : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
w : StdSimplex K X
hw : (↑(Finset.cons x t hx) : Set X) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
⊢ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)

Tactic:
simpa using congr(x ∈ $hsw)
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t_1 : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
w : StdSimplex K X
hw : (↑(Finset.cons x t hx) : Set X) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
⊢ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)

Tactic:
have hwx : w.weights x ≠ 0 := by simpa using congr(x ∈ $hsw)
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t_1 : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
w : StdSimplex K X
hw : (↑(Finset.cons x t hx) : Set X) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)
obtain : ∀ (y : X) (hy : y ∈ t), ∃ (y : X), y ≠ x ∧ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) y : K) (0 : K)
⊢ ∃ (y : X), y ≠ x ∧ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) y : K) (0 : K)

Tactic:
obtain ⟨y, hy⟩ := ht
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t_1 : Finset X
x : X
t : Finset X
hx : x ∉ t
ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
w : StdSimplex K X
hw : (↑(Finset.cons x t hx) : Set X) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)
y : X
hy : y ∈ t
⊢ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) y : K) (0 : K)

Tactic:
simpa [hy] using congr(y ∈ $hsw)
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t_1 : Finset X
x : X
t : Finset X
hx : x ∉ t
ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
w : StdSimplex K X
hw : (↑(Finset.cons x t hx) : Set X) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)
y : X
hy : y ∈ t
⊢ ∃ (y : X), y ≠ x ∧ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) y : K) (0 : K)

Tactic:
exact ⟨y, ne_of_mem_of_not_mem hy hx, by simpa [hy] using congr(y ∈ $hsw)⟩
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t_1 : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
w : StdSimplex K X
hw : (↑(Finset.cons x t hx) : Set X) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)
⊢ ∃ (y : X), y ≠ x ∧ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) y : K) (0 : K)

Tactic:
have hwx' : ∃ y ≠ x, w.weights y ≠ 0 := by
    obtain ⟨y, hy⟩ := ht
    exact ⟨y, ne_of_mem_of_not_mem hy hx, by simpa [hy] using congr(y ∈ $hsw)⟩
-- Module: Mathlib.Geometry.Convex.Set
Goal:
K : Type u_4
X : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : ConvexSpace K X
s : Set X
hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, convexCombPair a b ha hb hab x y ∈ s
t_1 : Finset X
x : X
t : Finset X
hx : x ∉ t
ht : t.Nonempty
ih : ∀ ⦃w : StdSimplex K X⦄ (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support), sConvexComb w ∈ s
w : StdSimplex K X
hw : (↑(Finset.cons x t hx) : Set X) ⊆ s
hsw : Finset.cons x t hx = w.weights.support
hwx : Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x : K) (0 : K)
hwx' : ∃ (y : X), y ≠ x ∧ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) y : K) (0 : K)
⊢ ∃ (x_1 : X), Membership.mem (γ := Set X) {x} x_1 ∧ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) x_1 : K) (0 : K)

Tactic:
simpa