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 𝕜).toOrderHom (p '' (s \ {i}))
⊢ False

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 𝕜).toOrderHom (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
⊢ i ∈ s
𝕜 : 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 𝕜).toOrderHom (p '' (s \ {i}))
refine' ⟨fun hc i s h => _, fun h s i hi => _⟩
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
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 𝕜).toOrderHom (p '' (s \ {i}))
⊢ False
rw [hc.mem_convexHull_iff] at h
no goals
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
exact h.2 (Set.mem_singleton _)
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 𝕜).toOrderHom (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
H : ¬i ∈ s
⊢ False
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 𝕜).toOrderHom (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
⊢ i ∈ s
by_contra H
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 𝕜).toOrderHom (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
H : ¬i ∈ s
⊢ p i ∈ ↑(convexHull 𝕜).toOrderHom (p '' (s \ {i}))
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 𝕜).toOrderHom (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
H : ¬i ∈ s
⊢ False
refine' h i s _
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 𝕜).toOrderHom (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
H : ¬i ∈ s
⊢ p i ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
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 𝕜).toOrderHom (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
H : ¬i ∈ s
⊢ p i ∈ ↑(convexHull 𝕜).toOrderHom (p '' (s \ {i}))
rw [Set.diff_singleton_eq_self H]
no goals
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 𝕜).toOrderHom (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
H : ¬i ∈ s
⊢ p i ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
exact hi