awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ sConvexComb w ∈ ⋃₀ S
have inr : ∀ (s : Set X) (hsS : s ∈ S) (hws : (↑w.weights.support : Set X) ⊆ 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
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ sConvexComb w ∈ f ⁻¹' s
have simp : iConvexComb w f ∈ s
Tactic: simp only [mem_preimage, hf.map_sConvexComb, sConvexComb_map]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ IsConvexSet R (f ⁻¹' s)
have rintro : ∀ ⦃w : StdSimplex R X⦄ (hw : (↑w.weights.support : Set X) ⊆ f ⁻¹' s), sConvexComb w ∈ 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
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ IsConvexSet R (f ⁻¹' s)
have rintro₁ : ∀ ⦃w : StdSimplex R X⦄ (hw : (↑w.weights.support : Set X) ⊆ f ⁻¹' s), iConvexComb w 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
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ sConvexComb w ∈ f '' s
have 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
Tactic: obtain ⟨u, hus, hfu, huw⟩ := Finset.exists_subset_injOn_image_eq_of_surjOn _ _ hw
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ 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)
have simp : LE.le.{u_3} (α := R) (0 : R) (if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0 : R)
Tactic: simp
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ LE.le.{u_3} (α := R) (0 : R) (if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0 : R)
have isTrue : x ∈ u → LE.le.{u_3} (α := R) (0 : R) ((w.weights : (a : Y) → R) (f x) : R)
Tactic: split
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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)
⊢ LE.le.{u_3} (α := R) (0 : R) (if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0 : R)
have isFalse : x ∉ u → LE.le.{u_3} (α := R) 0 0
Tactic: split
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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)
    (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
have simp : Eq.{u_3 + 1} (α := R) (∑ x ∈ w.weights.support, (w.weights : (a : Y) → R) x) 1
Tactic: simp only [implies_true, sum_onFinset, Finset.sum_ite_mem, Finset.inter_self,
        ← Finset.sum_image hfu, huw]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ (↑(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
have grw₁ : s ⊆ s
Tactic: grw [support_onFinset_subset, hus]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ sConvexComb w ∈ f '' s
have 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) sorry, nonneg := sorry,
        total := sorry : StdSimplex R X }) =
  sConvexComb w
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], ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ 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
have 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) sorry, nonneg := sorry,
        total := sorry : StdSimplex R X }) =
  sConvexComb w
Tactic: rw [hf.map_sConvexComb]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ 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
have e_f : StdSimplex.map f
    { weights := onFinset u (fun (x : X) ↦ if x ∈ u then (w.weights : (a : Y) → R) (f x) else 0) sorry, nonneg := sorry,
      total := sorry } =
  w
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ 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
have 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) sorry,
                nonneg := sorry, total := sorry }) :
          (a : Y) → R)
        y :
      R)
    ((w.weights : (a : Y) → R) y : R)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ 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)
have 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) sorry, nonneg := sorry,
              total := sorry }) :
        (a : Y) → R)
      y :
    R)
  ((w.weights : (a : Y) → R) y : R)
Tactic: rw [StdSimplex.weights_map]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ 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)
have 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) sorry,
                nonneg := sorry, total := sorry }) :
          (a : Y) → R)
        y :
      R)
    ((w.weights : (a : Y) → R) y : R)
Tactic: by_cases hy : y ∈ w.weights.support
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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)
⊢ 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)
have 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) sorry,
                nonneg := sorry, total := sorry }) :
          (a : Y) → R)
        y :
      R)
    ((w.weights : (a : Y) → R) y : R)
Tactic: by_cases hy : y ∈ w.weights.support
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (hypothesis)
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)
    ((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)
have hy₁ : ∃ a ∈ u, f a = y
Tactic: rw [← huw, Finset.mem_image] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ 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)
have 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) sorry,
                nonneg := sorry, total := sorry }) :
          (a : Y) → R)
        (f x) :
      R)
    ((w.weights : (a : Y) → R) (f x) : R)
Tactic: obtain ⟨x, hx, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
            (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)
have 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) sorry : (a : X) → R) x : R)
Tactic: convert mapDomain_apply' _ _ support_onFinset_subset hfu hx
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ 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)
have 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
Tactic: simp [← huw] at ⊢ hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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)
    ((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)
have neg : Eq.{u_3 + 1} (α := R) (0 : R) ((w.weights : (a : Y) → R) y : R)
Tactic: rw [mapDomain_of_not_mem_image_support (by simp [← huw] at ⊢ hy; tauto)]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ IsConvexSet R (f '' s)
have rintro : ∀ ⦃w : StdSimplex R Y⦄ (hw : (↑w.weights.support : Set Y) ⊆ f '' s), sConvexComb w ∈ 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
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ IsConvexSet R (f '' s)
have 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
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
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ IsConvexSet R (f '' s)
have 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) sorry, nonneg := sorry,
          total := sorry : StdSimplex R X }) =
    sConvexComb w
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