[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s t : Set E
inst✝ : Subsingleton ι
p : ι → E
⊢ ConvexIndependent 𝕜 p
[PROOFSTEP]
intro s x hx
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s✝ t : Set E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜) (p '' s)
⊢ x ∈ s
[PROOFSTEP]
have : (convexHull 𝕜 (p '' s)).Nonempty := ⟨p x, hx⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s✝ t : Set E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜) (p '' s)
this : Set.Nonempty (↑(convexHull 𝕜) (p '' s))
⊢ x ∈ s
[PROOFSTEP]
rw [convexHull_nonempty_iff, Set.nonempty_image_iff] at this 
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s✝ t : Set E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜) (p '' s)
this : Set.Nonempty s
⊢ x ∈ s
[PROOFSTEP]
rwa [Subsingleton.mem_iff_nonempty]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ Injective p
[PROOFSTEP]
refine' fun i j hij => hc { j } i _
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ p i ∈ ↑(convexHull 𝕜) (p '' {j})
[PROOFSTEP]
rw [hij, Set.image_singleton, convexHull_singleton]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ p j ∈ {p j}
[PROOFSTEP]
exact Set.mem_singleton _
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ ConvexIndependent 𝕜 (p ∘ ↑f)
[PROOFSTEP]
intro s x hx
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Set E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ↑f) x ∈ ↑(convexHull 𝕜) (p ∘ ↑f '' s)
⊢ x ∈ s
[PROOFSTEP]
rw [← f.injective.mem_set_image]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Set E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ↑f) x ∈ ↑(convexHull 𝕜) (p ∘ ↑f '' s)
⊢ ↑f x ∈ ↑f '' s
[PROOFSTEP]
exact hc _ _ (by rwa [Set.image_image])
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Set E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ↑f) x ∈ ↑(convexHull 𝕜) (p ∘ ↑f '' s)
⊢ p (↑f x) ∈ ↑(convexHull 𝕜) (p '' (↑f '' s))
[PROOFSTEP]
rwa [Set.image_image]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ ConvexIndependent 𝕜 Subtype.val
[PROOFSTEP]
let f : Set.range p → ι := fun x => x.property.choose
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
⊢ ConvexIndependent 𝕜 Subtype.val
[PROOFSTEP]
have hf : ∀ x, p (f x) = x := fun x => x.property.choose_spec
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
⊢ ConvexIndependent 𝕜 Subtype.val
[PROOFSTEP]
let fe : Set.range p ↪ ι := ⟨f, fun x₁ x₂ he => Subtype.ext (hf x₁ ▸ hf x₂ ▸ he ▸ rfl)⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := (_ : ∀ (x₁ x₂ : ↑(Set.range p)), f x₁ = f x₂ → x₁ = x₂) }
⊢ ConvexIndependent 𝕜 Subtype.val
[PROOFSTEP]
convert hc.comp_embedding fe
[GOAL]
case h.e'_7
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := (_ : ∀ (x₁ x₂ : ↑(Set.range p)), f x₁ = f x₂ → x₁ = x₂) }
⊢ Subtype.val = p ∘ ↑fe
[PROOFSTEP]
ext
[GOAL]
case h.e'_7.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : ↑(Set.range p) → ι := fun x => Exists.choose (_ : ↑x ∈ Set.range p)
hf : ∀ (x : ↑(Set.range p)), p (f x) = ↑x
fe : ↑(Set.range p) ↪ ι := { toFun := f, inj' := (_ : ∀ (x₁ x₂ : ↑(Set.range p)), f x₁ = f x₂ → x₁ = x₂) }
x✝ : { x // x ∈ Set.range p }
⊢ ↑x✝ = (p ∘ ↑fe) x✝
[PROOFSTEP]
rw [Embedding.coeFn_mk, comp_apply, hf]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
⊢ ConvexIndependent 𝕜 p ↔ ∀ (i : ι) (s : Set ι), ¬p i ∈ ↑(convexHull 𝕜) (p '' (s \ {i}))
[PROOFSTEP]
refine' ⟨fun hc i s h => _, fun h s i hi => _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
i : ι
s : Set ι
h : p i ∈ ↑(convexHull 𝕜) (p '' (s \ {i}))
⊢ False
[PROOFSTEP]
rw [hc.mem_convexHull_iff] at h 
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
i : ι
s : Set ι
h : i ∈ s \ {i}
⊢ False
[PROOFSTEP]
exact h.2 (Set.mem_singleton _)
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Set E
p : ι → E
h : ∀ (i : ι) (s : Set ι), ¬p i ∈ ↑(convexHull 𝕜) (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ ↑(convexHull 𝕜) (p '' s)
⊢ i ∈ s
[PROOFSTEP]
by_contra H
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Set E
p : ι → E
h : ∀ (i : ι) (s : Set ι), ¬p i ∈ ↑(convexHull 𝕜) (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ ↑(convexHull 𝕜) (p '' s)
H : ¬i ∈ s
⊢ False
[PROOFSTEP]
refine' h i s _
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Set E
p : ι → E
h : ∀ (i : ι) (s : Set ι), ¬p i ∈ ↑(convexHull 𝕜) (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ ↑(convexHull 𝕜) (p '' s)
H : ¬i ∈ s
⊢ p i ∈ ↑(convexHull 𝕜) (p '' (s \ {i}))
[PROOFSTEP]
rw [Set.diff_singleton_eq_self H]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Set E
p : ι → E
h : ∀ (i : ι) (s : Set ι), ¬p i ∈ ↑(convexHull 𝕜) (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ ↑(convexHull 𝕜) (p '' s)
H : ¬i ∈ s
⊢ p i ∈ ↑(convexHull 𝕜) (p '' s)
[PROOFSTEP]
exact hi
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ ConvexIndependent 𝕜 Subtype.val ↔ ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜) t ⊆ t
[PROOFSTEP]
constructor
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ ConvexIndependent 𝕜 Subtype.val → ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜) t ⊆ t
[PROOFSTEP]
rintro hc t h x ⟨hxs, hxt⟩
[GOAL]
case mp.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ConvexIndependent 𝕜 Subtype.val
t : Set E
h : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜) t
⊢ x ∈ t
[PROOFSTEP]
refine' hc {x | ↑x ∈ t} ⟨x, hxs⟩ _
[GOAL]
case mp.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ConvexIndependent 𝕜 Subtype.val
t : Set E
h : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜) t
⊢ ↑{ val := x, property := hxs } ∈ ↑(convexHull 𝕜) (Subtype.val '' {x | ↑x ∈ t})
[PROOFSTEP]
rw [Subtype.coe_image_of_subset h]
[GOAL]
case mp.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ConvexIndependent 𝕜 Subtype.val
t : Set E
h : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜) t
⊢ ↑{ val := x, property := hxs } ∈ ↑(convexHull 𝕜) t
[PROOFSTEP]
exact hxt
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ (∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜) t ⊆ t) → ConvexIndependent 𝕜 Subtype.val
[PROOFSTEP]
intro hc t x h
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜) t ⊆ t
t : Set { x // x ∈ s }
x : { x // x ∈ s }
h : ↑x ∈ ↑(convexHull 𝕜) (Subtype.val '' t)
⊢ x ∈ t
[PROOFSTEP]
rw [← Subtype.coe_injective.mem_set_image]
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜) t ⊆ t
t : Set { x // x ∈ s }
x : { x // x ∈ s }
h : ↑x ∈ ↑(convexHull 𝕜) (Subtype.val '' t)
⊢ ↑x ∈ (fun a => ↑a) '' t
[PROOFSTEP]
exact hc (t.image ((↑) : s → E)) (Subtype.coe_image_subset s t) ⟨x.prop, h⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ ConvexIndependent 𝕜 Subtype.val ↔ ∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜) (s \ {x})
[PROOFSTEP]
rw [convexIndependent_set_iff_inter_convexHull_subset]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ (∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜) t ⊆ t) ↔ ∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜) (s \ {x})
[PROOFSTEP]
constructor
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ (∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜) t ⊆ t) → ∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜) (s \ {x})
[PROOFSTEP]
rintro hs x hxs hx
[GOAL]
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
hs : ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜) t ⊆ t
x : E
hxs : x ∈ s
hx : x ∈ ↑(convexHull 𝕜) (s \ {x})
⊢ False
[PROOFSTEP]
exact (hs _ (Set.diff_subset _ _) ⟨hxs, hx⟩).2 (Set.mem_singleton _)
[GOAL]
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ (∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜) (s \ {x})) → ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜) t ⊆ t
[PROOFSTEP]
rintro hs t ht x ⟨hxs, hxt⟩
[GOAL]
case mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hs : ∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜) (s \ {x})
t : Set E
ht : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜) t
⊢ x ∈ t
[PROOFSTEP]
by_contra h
[GOAL]
case mpr.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hs : ∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜) (s \ {x})
t : Set E
ht : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜) t
h : ¬x ∈ t
⊢ False
[PROOFSTEP]
exact hs _ hxs (convexHull_mono (Set.subset_diff_singleton ht h) hxt)
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
p : ι → E
⊢ ConvexIndependent 𝕜 p ↔ ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
[PROOFSTEP]
refine' ⟨fun hc s x hx => hc s x _, fun h s x hx => _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Finset ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜) ↑(image p s)
⊢ p x ∈ ↑(convexHull 𝕜) (p '' ↑s)
[PROOFSTEP]
rwa [Finset.coe_image] at hx 
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜) (p '' s)
⊢ x ∈ s
[PROOFSTEP]
have hp : Injective p := by
  rintro a b hab
  rw [← mem_singleton]
  refine' h { b } a _
  rw [hab, image_singleton, coe_singleton, convexHull_singleton]
  exact Set.mem_singleton _
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜) (p '' s)
⊢ Injective p
[PROOFSTEP]
rintro a b hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ a = b
[PROOFSTEP]
rw [← mem_singleton]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ a ∈ {b}
[PROOFSTEP]
refine' h { b } a _
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ p a ∈ ↑(convexHull 𝕜) ↑(image p {b})
[PROOFSTEP]
rw [hab, image_singleton, coe_singleton, convexHull_singleton]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ p b ∈ {p b}
[PROOFSTEP]
exact Set.mem_singleton _
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜) (p '' s)
hp : Injective p
⊢ x ∈ s
[PROOFSTEP]
rw [convexHull_eq_union_convexHull_finite_subsets] at hx 
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ⋃ (t : Finset E) (_ : ↑t ⊆ p '' s), ↑(convexHull 𝕜) ↑t
hp : Injective p
⊢ x ∈ s
[PROOFSTEP]
simp_rw [Set.mem_iUnion] at hx 
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
hx : ∃ i i_1, p x ∈ ↑(convexHull 𝕜) ↑i
⊢ x ∈ s
[PROOFSTEP]
obtain ⟨t, ht, hx⟩ := hx
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜) ↑t
⊢ x ∈ s
[PROOFSTEP]
rw [← hp.mem_set_image]
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜) ↑t
⊢ p x ∈ p '' s
[PROOFSTEP]
refine' ht _
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜) ↑t
⊢ p x ∈ ↑t
[PROOFSTEP]
suffices x ∈ t.preimage p (hp.injOn _) by rwa [mem_preimage, ← mem_coe] at this 
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜) ↑t
this : x ∈ preimage t p (_ : Set.InjOn p (p ⁻¹' ↑t))
⊢ p x ∈ ↑t
[PROOFSTEP]
rwa [mem_preimage, ← mem_coe] at this 
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜) ↑t
⊢ x ∈ preimage t p (_ : Set.InjOn p (p ⁻¹' ↑t))
[PROOFSTEP]
refine' h _ x _
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜) ↑t
⊢ p x ∈ ↑(convexHull 𝕜) ↑(image p (preimage t p (_ : Set.InjOn p (p ⁻¹' ↑t))))
[PROOFSTEP]
rwa [t.image_preimage p (hp.injOn _), filter_true_of_mem]
[GOAL]
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ : Set E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ ↑(convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜) ↑t
⊢ ∀ (x : E), x ∈ t → x ∈ Set.range p
[PROOFSTEP]
exact fun y hy => s.image_subset_range p (ht <| mem_coe.2 hy)
