sorry
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
hx₁₂ : segment 𝕜 x₁ x₂ ⊆ (convexHull 𝕜) s
⊢ x₁ ∈ (convexHull 𝕜) (s \ {x}) ∧ x₂ ∈ (convexHull 𝕜) (s \ {x})
no goals