awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hs : Set.Subsingleton (α := X) {x}
⊢ IsConvexSet R (X := X) {x}

Tactic:
simp
-- 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 t : Set X
hs : IsConvexSet R s
ht : IsConvexSet R t
⊢ IsConvexSet R (s ∩ t)

Tactic:
simp +contextual [IsConvexSet, hs.sConvexComb_mem, ht.sConvexComb_mem]

Premises used: Convexity.IsConvexSet.sConvexComb_mem, 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
S : Set (Set X)
hS : ∀ s ∈ S, IsConvexSet R s
⊢ IsConvexSet R (⋂₀ S)

Tactic:
simp +contextual [IsConvexSet, (hS _ _).sConvexComb_mem]

Premises used: Convexity.IsConvexSet.sConvexComb_mem, 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
ι : Sort u_7
s : ι → Set X
hs : ∀ (i : ι), IsConvexSet R (s i)
⊢ IsConvexSet.{u_3, u_5} R (X := X) (⋂ (i : ι), s i)

Tactic:
simp +contextual [IsConvexSet, (hs _).sConvexComb_mem]

Premises used: Convexity.IsConvexSet.sConvexComb_mem, 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
ι : Sort u_7
κ : ι → Sort u_8
s : (i : ι) → κ i → Set X
h : ∀ (i : ι) (j : κ i), IsConvexSet R (s i j)
⊢ IsConvexSet.{u_3, u_5} R (X := X) (⋂ (i : ι), ⋂ (j : κ i), s i j)

Tactic:
.iInter fun i ↦ .iInter <| h i

Premises used: Convexity.IsConvexSet.iInter
-- 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 (Set X)
hS : DirectedOn (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) S
hS' : ∀ s ∈ S, IsConvexSet R s
inl :
  ∀ (hS : DirectedOn (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) ∅)
    (hS' : ∀ (s : Set X), Membership.mem (γ := Set (Set X)) ∅ s → IsConvexSet R s),
    IsConvexSet.{u_3, u_5} R (X := X) (⋃₀ ∅)
inr : ∀ (hS'' : S.Nonempty), IsConvexSet R (⋃₀ S)
⊢ IsConvexSet R (⋃₀ S)

Tactic:
obtain rfl | hS'' := S.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, 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 : DirectedOn (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) ∅
hS' : ∀ (s : Set X), Membership.mem (γ := Set (Set X)) ∅ s → IsConvexSet R s
⊢ IsConvexSet.{u_3, u_5} R (X := X) (⋃₀ ∅)

Tactic:
simp
-- 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 (Set X)
hS : DirectedOn (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) S
hS' : ∀ s ∈ S, IsConvexSet R s
hS'' : S.Nonempty
w : StdSimplex R X
hw : (↑w.weights.support : Set X) ⊆ ⋃₀ S
inr : ∀ (s : Set X) (hsS : s ∈ S) (hws : (↑w.weights.support : Set X) ⊆ s), sConvexComb w ∈ ⋃₀ S
⊢ sConvexComb w ∈ ⋃₀ S

Tactic:
obtain ⟨s, hsS, hws⟩ :=
    hS.exists_mem_subset_of_finite_of_subset_sUnion hS'' w.weights.support.finite_toSet hw

Premises used: Finsupp.support, Convexity.StdSimplex.weights, DirectedOn.exists_mem_subset_of_finite_of_subset_sUnion, Finset.finite_toSet
-- 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 (Set X)
hS : DirectedOn (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) S
hS' : ∀ s ∈ S, IsConvexSet R s
hS'' : S.Nonempty
w : StdSimplex R X
hw : (↑w.weights.support : Set X) ⊆ ⋃₀ S
s : Set X
hsS : s ∈ S
hws : (↑w.weights.support : Set X) ⊆ s
⊢ sConvexComb w ∈ ⋃₀ S

Tactic:
mem_sUnion_of_mem (hS' s hsS hws) hsS

Premises used: Set.mem_sUnion_of_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 (Set X)
hS : DirectedOn (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) S
hS' : ∀ s ∈ S, IsConvexSet R s
hS'' : S.Nonempty
w : StdSimplex R X
hw : (↑w.weights.support : Set X) ⊆ ⋃₀ S
s : Set X
hsS : s ∈ S
hws : (↑w.weights.support : Set X) ⊆ s
⊢ sConvexComb w ∈ ⋃₀ S

Tactic:
exact mem_sUnion_of_mem (hS' s hsS hws) hsS

Premises used: Set.mem_sUnion_of_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
ι : Sort u_7
s : ι → Set X
hs : Directed (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) s
hs' : ∀ (i : ι), IsConvexSet R (s i)
⊢ ∀ (s_1 : Set X), Membership.mem (γ := Set (Set X)) (range fun (i : ι) ↦ s i) s_1 → IsConvexSet R s_1

Tactic:
simpa
-- 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 Y
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R X
hw : (↑w.weights.support : Set X) ⊆ f ⁻¹' s
simp : iConvexComb w f ∈ s
⊢ sConvexComb w ∈ f ⁻¹' s

Tactic:
simp only [mem_preimage, hf.map_sConvexComb, sConvexComb_map]

Premises used: Convexity.sConvexComb_map, Convexity.IsAffineMap.map_sConvexComb, Set.mem_preimage
-- 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 Y
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R X
hw : (↑w.weights.support : Set X) ⊆ f ⁻¹' s
x : X
hx : Ne.{u_3 + 1} (α := R) ((w.weights : (a : X) → R) x : R) (0 : R)
⊢ x ∈ (↑w.weights.support : Set X)

Tactic:
simpa
-- 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 Y
hf : IsAffineMap R f
hs : IsConvexSet R s
w : StdSimplex R X
hw : (↑w.weights.support : Set X) ⊆ f ⁻¹' s
⊢ iConvexComb w f ∈ s

Tactic:
exact hs.iConvexComb_mem fun x hx ↦ hw <| by simpa

Premises used: Convexity.IsConvexSet.iConvexComb_mem
-- 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 Y
hf : IsAffineMap R f
hs : IsConvexSet R s
rintro : ∀ ⦃w : StdSimplex R X⦄ (hw : (↑w.weights.support : Set X) ⊆ f ⁻¹' s), sConvexComb w ∈ f ⁻¹' s
rintro₁ : ∀ ⦃w : StdSimplex R X⦄ (hw : (↑w.weights.support : Set X) ⊆ f ⁻¹' s), iConvexComb w f ∈ s
⊢ IsConvexSet R (f ⁻¹' s)

Tactic:
classical
  rintro w hw
  simp only [mem_preimage, hf.map_sConvexComb, sConvexComb_map]
  exact hs.iConvexComb_mem fun x hx ↦ hw <| by simpa

Premises used: Convexity.sConvexComb_map, Convexity.IsAffineMap.map_sConvexComb, Set.mem_preimage
-- 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
obtain :
  ∀ (u : Finset X) (hus : (↑u : Set X) ⊆ s) (hfu : InjOn f (↑u : Set X)) (huw : Finset.image f u = w.weights.support),
    sConvexComb w ∈ f '' s
⊢ sConvexComb w ∈ f '' s

Tactic:
obtain ⟨u, hus, hfu, huw⟩ := Finset.exists_subset_injOn_image_eq_of_surjOn _ _ hw

Premises used: Finset.exists_subset_injOn_image_eq_of_surjOn
-- 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
⊢ ∀ (a : X),
    Ne.{u_3 + 1} (α := R) ((fun (x : X) ↦ (if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0 : R)) a) 0 → a ∈ u

Tactic:
simp +contextual
-- 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
simp : LE.le.{u_3} (α := R) (0 : R) (if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0 : R)
⊢ LE.le.{u_3} (α := R) ((0 : (a : X) → R) 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:
simp
-- 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
isTrue : x ∈ u → LE.le.{u_3} (α := R) (0 : R) ((w.weights : (a : Y) → R) (f x) : R)
isFalse : x ∉ u → LE.le.{u_3} (α := R) 0 0
⊢ LE.le.{u_3} (α := R) (0 : R) (if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0 : R)

Tactic:
split
-- 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
h : x ∈ u
⊢ LE.le.{u_3} (α := R) (0 : R) ((w.weights : (a : Y) → R) (f x) : R)

Tactic:
simp
-- 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
h : x ∉ u
⊢ LE.le.{u_3} (α := R) 0 0

Tactic:
simp
-- 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
simp : Eq.{u_3 + 1} (α := R) (∑ x ∈ w.weights.support, (w.weights : (a : Y) → R) x) 1
⊢ Eq.{u_3 + 1} (α := R)
    (sum (onFinset u (fun (x : X) ↦ if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0) ⋯) fun (x : X) (r : R) ↦ r) 1

Tactic:
simp only [implies_true, sum_onFinset, Finset.sum_ite_mem, Finset.inter_self,
        ← Finset.sum_image hfu, huw]

Premises used: Finset.sum_ite_mem, Finset.inter_self, Finsupp.sum_onFinset, Finset.sum_image, implies_true
-- 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
⊢ Eq.{u_3 + 1} (α := R) (∑ x ∈ w.weights.support, (w.weights : (a : Y) → R) x) 1

Tactic:
w.total

Premises used: Finsupp.sum, Convexity.StdSimplex.total
-- 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
⊢ Eq.{u_3 + 1} (α := R) (∑ x ∈ w.weights.support, (w.weights : (a : Y) → R) x) 1

Tactic:
exact w.total

Premises used: Convexity.StdSimplex.total
-- 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
grw : (↑u : Set X) ⊆ s
grw₁ grw₂ : s ⊆ s
⊢ (↑(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) ⊆
    s

Tactic:
grw [support_onFinset_subset, hus]

Premises used: Finsupp.support_onFinset_subset
-- 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
refine :
  f
      (sConvexComb.{u_3, u_5} (R := R)
        { weights := onFinset u (fun (x : X) ↦ if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0) ⋯, nonneg := ⋯,
          total := ⋯ : StdSimplex R X }) =
    sConvexComb w
⊢ sConvexComb w ∈ f '' s

Tactic:
refine ⟨sConvexComb {
      weights := .onFinset u (fun x ↦ if x ∈ u then w.weights (f x) else 0) <| by simp +contextual
      nonneg x := by simp; split <;> simp
      total := by
        simp only [implies_true, sum_onFinset, Finset.sum_ite_mem, Finset.inter_self,
        ← Finset.sum_image hfu, huw]
        exact w.total
    }, hs.sConvexComb_mem <| by grw [support_onFinset_subset, hus], ?_⟩
-- 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
rw :
  sConvexComb.{u_3, u_6} (R := R)
      (StdSimplex.map f
        { weights := onFinset u (fun (x : X) ↦ if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0) ⋯, nonneg := ⋯,
          total := ⋯ : StdSimplex R X }) =
    sConvexComb w
⊢ f
      (sConvexComb.{u_3, u_5} (R := R)
        { weights := onFinset u (fun (x : X) ↦ if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0) ⋯, nonneg := ⋯,
          total := ⋯ : StdSimplex R X }) =
    sConvexComb w

Tactic:
rw [hf.map_sConvexComb]

Premises used: Convexity.IsAffineMap.map_sConvexComb
-- 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
e_f :
  StdSimplex.map f
      { weights := onFinset u (fun (x : X) ↦ if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0) ⋯, nonneg := ⋯,
        total := ⋯ } =
    w
⊢ sConvexComb.{u_3, u_6} (R := R)
      (StdSimplex.map f
        { weights := onFinset u (fun (x : X) ↦ if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0) ⋯, nonneg := ⋯,
          total := ⋯ : StdSimplex R X }) =
    sConvexComb w

Tactic:
congr
-- 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
e_f :
  ∀ (y : Y),
    Eq.{u_3 + 1} (α := R)
      ((StdSimplex.weights
              (StdSimplex.map f
                { 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)
⊢ StdSimplex.map f
      { weights := onFinset u (fun (x : X) ↦ if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0) ⋯, nonneg := ⋯,
        total := ⋯ } =
    w

Tactic:
ext y
-- 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
e_f :
  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)
⊢ Eq.{u_3 + 1} (α := R)
    ((StdSimplex.weights
            (StdSimplex.map f
              { 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 [StdSimplex.weights_map]

Premises used: Convexity.StdSimplex.weights_map
-- 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
pos :
  ∀ (hy : y ∈ w.weights.support),
    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)
neg :
  ∀ (hy : y ∉ w.weights.support),
    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)
⊢ 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:
by_cases hy : y ∈ w.weights.support

Premises used: Finsupp.support, Convexity.StdSimplex.weights
-- 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
⊢ ∃ a ∈ u, f a = y

Tactic:
rw [← huw, Finset.mem_image] at hy

Premises used: Finset.mem_image
-- 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 : ∃ a ∈ u, f a = y
pos :
  ∀ (x : X) (hx : x ∈ u),
    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)
          (f x) :
        R)
      ((w.weights : (a : Y) → R) (f x) : 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:
obtain ⟨x, hx, rfl⟩ := hy

Premises used: rfl
-- 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)
    ((mapDomain f (onFinset u (fun (x : X) ↦ if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0) ⋯) : (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:
mapDomain_apply' _ _ support_onFinset_subset hfu hx

Premises used: Finsupp.support_onFinset_subset, Finsupp.mapDomain_apply'
-- 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
h :
  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)
⊢ 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)
        (f x) :
      R)
    ((w.weights : (a : Y) → R) (f x) : R)

Tactic:
convert mapDomain_apply' _ _ support_onFinset_subset hfu hx

Premises used: Finsupp.support_onFinset_subset, Finsupp.mapDomain_apply'