Theorem: inter_frontier_self_inter_convexHull_extreme (LeanCamCombi/Mathlib/Analysis/Convex/Extreme.lean)

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
⊢ IsExtreme 𝕜 (closure s) (closure s ∩ frontier ((convexHull 𝕜) s))
Tactic:
refine' ⟨inter_subset_left, fun x₁ hx₁A x₂ hx₂A x hxs hx => ⟨⟨hx₁A, _⟩, hx₂A, _⟩⟩
State after:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ x₁ : E
hx₁A : x₁ ∈ closure s
x₂ : E
hx₂A : x₂ ∈ closure s
x : E
hxs : x ∈ closure s ∩ frontier ((convexHull 𝕜) s)
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ frontier ((convexHull 𝕜) s)

case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ x₁ : E
hx₁A : x₁ ∈ closure s
x₂ : E
hx₂A : x₂ ∈ closure s
x : E
hxs : x ∈ closure s ∩ frontier ((convexHull 𝕜) s)
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₂ ∈ frontier ((convexHull 𝕜) s)

State before:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ x₁ : E
hx₁A : x₁ ∈ closure s
x₂ : E
hx₂A : x₂ ∈ closure s
x : E
hxs : x ∈ closure s ∩ frontier ((convexHull 𝕜) s)
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ frontier ((convexHull 𝕜) s)

case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ x₁ : E
hx₁A : x₁ ∈ closure s
x₂ : E
hx₂A : x₂ ∈ closure s
x : E
hxs : x ∈ closure s ∩ frontier ((convexHull 𝕜) s)
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₂ ∈ frontier ((convexHull 𝕜) s)
Tactic:
sorry
State after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ x₁ : E
hx₁A : x₁ ∈ closure s
x₂ : E
hx₂A : x₂ ∈ closure s
x : E
hxs : x ∈ closure s ∩ frontier ((convexHull 𝕜) s)
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₂ ∈ frontier ((convexHull 𝕜) s)

State before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ x₁ : E
hx₁A : x₁ ∈ closure s
x₂ : E
hx₂A : x₂ ∈ closure s
x : E
hxs : x ∈ closure s ∩ frontier ((convexHull 𝕜) s)
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₂ ∈ frontier ((convexHull 𝕜) s)
Tactic:
sorry
State after:
no goals