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 𝕜).toOrderHom ↑(image p s)
⊢ p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' ↑s)

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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
⊢ x ∈ s
𝕜 : 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 𝕜).toOrderHom ↑(image p s) → x ∈ s
refine' ⟨fun hc s x hx => hc s x _, fun h s x hx => _⟩
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
hp : Injective p
⊢ x ∈ s
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
⊢ x ∈ s
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 _
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ⋃ (t : Finset E) (_ : ↑t ⊆ p '' s), ↑(convexHull 𝕜).toOrderHom ↑t
hp : Injective p
⊢ x ∈ s
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
hp : Injective p
⊢ x ∈ s
rw [convexHull_eq_union_convexHull_finite_subsets] at hx
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
hx : ∃ i i_1, p x ∈ ↑(convexHull 𝕜).toOrderHom ↑i
⊢ x ∈ s
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ⋃ (t : Finset E) (_ : ↑t ⊆ p '' s), ↑(convexHull 𝕜).toOrderHom ↑t
hp : Injective p
⊢ x ∈ s
simp_rw [Set.mem_iUnion] at hx
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom ↑t
⊢ x ∈ s
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
hx : ∃ i i_1, p x ∈ ↑(convexHull 𝕜).toOrderHom ↑i
⊢ x ∈ s
obtain ⟨t, ht, hx⟩ := hx
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom ↑t
⊢ p x ∈ p '' s
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom ↑t
⊢ x ∈ s
rw [← hp.mem_set_image]
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom ↑t
⊢ p x ∈ ↑t
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom ↑t
⊢ p x ∈ p '' s
refine' ht _
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom ↑t
⊢ x ∈ preimage t p (_ : Set.InjOn p (p ⁻¹' ↑t))
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom ↑t
⊢ p x ∈ ↑t
suffices x ∈ t.preimage p (hp.injOn _) by rwa [mem_preimage, ← mem_coe] at this
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom ↑t
⊢ p x ∈ ↑(convexHull 𝕜).toOrderHom ↑(image p (preimage t p (_ : Set.InjOn p (p ⁻¹' ↑t))))
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom ↑t
⊢ x ∈ preimage t p (_ : Set.InjOn p (p ⁻¹' ↑t))
refine' h _ x _
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom ↑t
⊢ ∀ (x : E), x ∈ t → x ∈ Set.range p
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom ↑t
⊢ p x ∈ ↑(convexHull 𝕜).toOrderHom ↑(image p (preimage t p (_ : Set.InjOn p (p ⁻¹' ↑t))))
rwa [t.image_preimage p (hp.injOn _), filter_true_of_mem]
no goals
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 𝕜).toOrderHom ↑(image p s)
⊢ p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' ↑s)
rwa [Finset.coe_image] at hx
𝕜 : 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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
a b : ι
hab : p a = p b
⊢ a = b
𝕜 : 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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
⊢ Injective p
rintro a b hab
𝕜 : 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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
a b : ι
hab : p a = p b
⊢ a ∈ {b}
𝕜 : 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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
a b : ι
hab : p a = p b
⊢ a = b
rw [← mem_singleton]
𝕜 : 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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
a b : ι
hab : p a = p b
⊢ p a ∈ ↑(convexHull 𝕜).toOrderHom ↑(image p {b})
𝕜 : 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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
a b : ι
hab : p a = p b
⊢ a ∈ {b}
refine' h {b} a _
𝕜 : 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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
a b : ι
hab : p a = p b
⊢ p b ∈ {p b}
𝕜 : 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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
a b : ι
hab : p a = p b
⊢ p a ∈ ↑(convexHull 𝕜).toOrderHom ↑(image p {b})
rw [hab, image_singleton, coe_singleton, convexHull_singleton]
no goals
𝕜 : 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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
a b : ι
hab : p a = p b
⊢ p b ∈ {p b}
exact Set.mem_singleton _
no goals
𝕜 : 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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom ↑t
this : x ∈ preimage t p (_ : Set.InjOn p (p ⁻¹' ↑t))
⊢ p x ∈ ↑t
rwa [mem_preimage, ← mem_coe] at this
no goals
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 𝕜).toOrderHom ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom ↑t
⊢ ∀ (x : E), x ∈ t → x ∈ Set.range p
exact fun y hy => s.image_subset_range p (ht <| mem_coe.2 hy)