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
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
⊢ 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.{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: 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
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
⊢ IsConvexSet R (f '' s)
have 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) sorry, nonneg := sorry,
        total := sorry } =
    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
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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} (α := (↑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))
have 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))) sorry)
        (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))) sorry)
          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))) sorry)
        (sConvexComb w)) :
    X)
Tactic: ext
-- 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 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
have refine_1 : (↑(StdSimplex.map Prod.fst w).weights.support : Set X) ⊆ s
Tactic: refine ⟨hs ?_, ht ?_⟩
-- 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 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
⊢ sConvexComb w ∈ s ×ˢ t
have refine_2 : (↑(StdSimplex.map Prod.snd w).weights.support : Set Y) ⊆ t
Tactic: refine ⟨hs ?_, ht ?_⟩
-- 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 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
⊢ (↑(StdSimplex.map Prod.fst w).weights.support : Set X) ⊆ s
have refine_1 : (↑(mapDomain Prod.fst w.weights).support : Set X) ⊆ s
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, fst_image_prod_subset]
-- 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 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
⊢ (↑(StdSimplex.map Prod.fst w).weights.support : Set X) ⊆ s
have refine_1₁ : (↑(Finset.image Prod.fst w.weights.support) : Set X) ⊆ s
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, fst_image_prod_subset]
-- 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 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
⊢ (↑(StdSimplex.map Prod.fst w).weights.support : Set X) ⊆ s
have refine_1₂ : Prod.fst '' (↑w.weights.support : Set (X × Y)) ⊆ s
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, fst_image_prod_subset]
-- 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 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
⊢ (↑(StdSimplex.map Prod.fst w).weights.support : Set X) ⊆ s
have refine_1₃ : Prod.fst '' s ×ˢ t ⊆ s
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, fst_image_prod_subset]
-- 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 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
⊢ (↑(StdSimplex.map Prod.fst w).weights.support : Set X) ⊆ s
have refine_1₄ : s ⊆ s
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, fst_image_prod_subset]
-- 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 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
⊢ (↑(StdSimplex.map Prod.snd w).weights.support : Set Y) ⊆ t
have refine_2 : (↑(mapDomain Prod.snd w.weights).support : Set Y) ⊆ t
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, snd_image_prod_subset]
-- 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 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
⊢ (↑(StdSimplex.map Prod.snd w).weights.support : Set Y) ⊆ t
have refine_2₁ : (↑(Finset.image Prod.snd w.weights.support) : Set Y) ⊆ t
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, snd_image_prod_subset]
-- 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 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
⊢ (↑(StdSimplex.map Prod.snd w).weights.support : Set Y) ⊆ t
have refine_2₂ : Prod.snd '' (↑w.weights.support : Set (X × Y)) ⊆ t
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, snd_image_prod_subset]
-- 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 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
⊢ (↑(StdSimplex.map Prod.snd w).weights.support : Set Y) ⊆ t
have refine_2₃ : Prod.snd '' s ×ˢ t ⊆ t
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, snd_image_prod_subset]
-- 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 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
⊢ (↑(StdSimplex.map Prod.snd w).weights.support : Set Y) ⊆ t
have refine_2₄ : t ⊆ t
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, snd_image_prod_subset]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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)
have 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
Tactic: refine fun w hw i hi ↦ ht i hi ?_
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ (↑(support (StdSimplex.weights (StdSimplex.map (fun (x : (i : ι) → X i) ↦ x i) w))) : Set (X i)) ⊆ t i
have grw : (↑(support (mapDomain (fun (x : (i : ι) → X i) ↦ x i) w.weights)) : Set (X i)) ⊆ t i
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, eval_image_pi_subset hi]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ (↑(support (StdSimplex.weights (StdSimplex.map (fun (x : (i : ι) → X i) ↦ x i) w))) : Set (X i)) ⊆ t i
have grw₁ : (↑(Finset.image (fun (x : (i : ι) → X i) ↦ x i) w.weights.support) : Set (X i)) ⊆ t i
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, eval_image_pi_subset hi]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ (↑(support (StdSimplex.weights (StdSimplex.map (fun (x : (i : ι) → X i) ↦ x i) w))) : Set (X i)) ⊆ t i
have grw₂ : (fun (x : (i : ι) → X i) ↦ x i) '' (↑w.weights.support : Set ((i : ι) → X i)) ⊆ t i
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, eval_image_pi_subset hi]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ (↑(support (StdSimplex.weights (StdSimplex.map (fun (x : (i : ι) → X i) ↦ x i) w))) : Set (X i)) ⊆ t i
have grw₃ : (fun (x : (i : ι) → X i) ↦ x i) '' s.pi (α := X) t ⊆ t i
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, eval_image_pi_subset hi]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ (↑(support (StdSimplex.weights (StdSimplex.map (fun (x : (i : ι) → X i) ↦ x i) w))) : Set (X i)) ⊆ t i
have grw₄ : t i ⊆ t i
Tactic: grw [StdSimplex.weights_map, mapDomain_support, Finset.coe_image, hw, eval_image_pi_subset hi]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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)
have 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
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]
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (hypothesis)
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
⊢ sConvexComb w ∈ s
have hsw : let t := w.weights.support;
t = w.weights.support
Tactic: set t := w.weights.support with hsw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (hypothesis)
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
⊢ sConvexComb w ∈ s
have ht : t.Nonempty
Tactic: have ht : t.Nonempty := w.support_weights_nonempty
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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
⊢ sConvexComb w ∈ s
have clear_value : ∀ (t : Finset X) (hw : (↑t : Set X) ⊆ s) (hsw : t = w.weights.support) (ht : t.Nonempty), sConvexComb w ∈ s
Tactic: clear_value t
Cleared hypotheses: t, hw, hsw, ht
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (hypothesis)
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
⊢ sConvexComb w ∈ s
have hwx : 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)
-- Lean 4 proof step from Mathlib.Geometry.Convex.Set (goal)
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)
have obtain : ∀ (y : X) (hy : y ∈ t), ∃ (y : X), y ≠ x ∧ Ne.{u_4 + 1} (α := K) ((w.weights : (a : X) → K) y : K) (0 : K)
Tactic: obtain ⟨y, hy⟩ := ht
Cleared hypotheses: ht