-- 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
rintro : ∀ ⦃w : StdSimplex R Y⦄ (hw : (↑w.weights.support : Set Y) ⊆ f '' s), sConvexComb w ∈ f '' s
rintro₁ :
  ∀ ⦃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), sConvexComb w ∈ f '' s
rintro₂ :
  ∀ ⦃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),
    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
rintro₃ :
  ∀ ⦃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),
    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
e_f :
  ∀ ⦃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),
    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
e_f₁ :
  ∀ ⦃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),
    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)
e_f₂ :
  ∀ ⦃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),
    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)
pos :
  ∀ ⦃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)
      ((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 neg₁ :
  ∀ ⦃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)
      ((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)
⊢ IsConvexSet R (f '' s)

Tactic:
classical
  rintro w hw
  obtain ⟨u, hus, hfu, huw⟩ := Finset.exists_subset_injOn_image_eq_of_surjOn _ _ hw
  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], ?_⟩
  rw [hf.map_sConvexComb]
  congr
  ext y
  rw [StdSimplex.weights_map]
  by_cases hy : y ∈ w.weights.support
  · rw [← huw, Finset.mem_image] at hy
    obtain ⟨x, hx, rfl⟩ := hy
    convert mapDomain_apply' _ _ support_onFinset_subset hfu hx
    exact (if_pos hx).symm
  · rw [mapDomain_of_not_mem_image_support (by simp [← huw] at ⊢ hy; tauto)]
    simp_all

Premises used: Finset.mem_image, Convexity.StdSimplex.weights_map, Finsupp.mapDomain_of_not_mem_image_support, Convexity.IsAffineMap.map_sConvexComb, rfl