Theorem: Convex.frontier_extreme_to_closure (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
hAconv : Convex 𝕜 s
⊢ IsExtreme 𝕜 (closure s) (frontier s)
Tactic:
use frontier_subset_closure
State after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hAconv : Convex 𝕜 s
⊢ ∀ ⦃x₁ : E⦄,
    x₁ ∈ closure s →
      ∀ ⦃x₂ : E⦄,
        x₂ ∈ closure s → ∀ ⦃x : E⦄, x ∈ frontier s → x ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ frontier s ∧ x₂ ∈ frontier s

State before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x : E
hAconv : Convex 𝕜 s
⊢ ∀ ⦃x₁ : E⦄,
    x₁ ∈ closure s →
      ∀ ⦃x₂ : E⦄,
        x₂ ∈ closure s → ∀ ⦃x : E⦄, x ∈ frontier s → x ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ frontier s ∧ x₂ ∈ frontier s
Tactic:
sorry
State after:
no goals