𝕜 : Type u_2
E : Type u_1
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C : Set E
X : Finset E
x : E
⊢ IsExposed 𝕜 A {x} → x ∈ exposedPoints 𝕜 A
𝕜 : Type u_2
E : Type u_1
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C : Set E
X : Finset E
x : E
⊢ x ∈ exposedPoints 𝕜 A ↔ IsExposed 𝕜 A {x}
use fun ⟨hxA, l, hl⟩ _ =>
  ⟨l,
    Eq.symm <|
      eq_singleton_iff_unique_mem.2
        ⟨⟨hxA, fun y hy => (hl y hy).1⟩, fun z hz => (hl z hz.1).2 (hz.2 x hxA)⟩⟩
𝕜 : Type u_2
E : Type u_1
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C : Set E
X : Finset E
x : E
h : IsExposed 𝕜 A {x}
⊢ x ∈ exposedPoints 𝕜 A
𝕜 : Type u_2
E : Type u_1
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C : Set E
X : Finset E
x : E
⊢ IsExposed 𝕜 A {x} → x ∈ exposedPoints 𝕜 A
rintro h
case intro
𝕜 : Type u_2
E : Type u_1
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
l✝ : E →L[𝕜] 𝕜
A B C : Set E
X : Finset E
x : E
h : IsExposed 𝕜 A {x}
l : E →L[𝕜] 𝕜
hl : {x} = {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
⊢ x ∈ exposedPoints 𝕜 A
𝕜 : Type u_2
E : Type u_1
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
l : E →L[𝕜] 𝕜
A B C : Set E
X : Finset E
x : E
h : IsExposed 𝕜 A {x}
⊢ x ∈ exposedPoints 𝕜 A
obtain ⟨l, hl⟩ := h ⟨x, mem_singleton _⟩
case intro
𝕜 : Type u_2
E : Type u_1
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
l✝ : E →L[𝕜] 𝕜
A B C : Set E
X : Finset E
x : E
h : IsExposed 𝕜 A {x}
l : E →L[𝕜] 𝕜
hl :
  x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ∧
    ∀ (x_1 : E), x_1 ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} → x_1 = x
⊢ x ∈ exposedPoints 𝕜 A
case intro
𝕜 : Type u_2
E : Type u_1
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
l✝ : E →L[𝕜] 𝕜
A B C : Set E
X : Finset E
x : E
h : IsExposed 𝕜 A {x}
l : E →L[𝕜] 𝕜
hl : {x} = {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
⊢ x ∈ exposedPoints 𝕜 A
rw [eq_comm, eq_singleton_iff_unique_mem] at hl
no goals
case intro
𝕜 : Type u_2
E : Type u_1
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
l✝ : E →L[𝕜] 𝕜
A B C : Set E
X : Finset E
x : E
h : IsExposed 𝕜 A {x}
l : E →L[𝕜] 𝕜
hl :
  x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ∧
    ∀ (x_1 : E), x_1 ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} → x_1 = x
⊢ x ∈ exposedPoints 𝕜 A
exact
  ⟨hl.1.1, l, fun y hy =>
    ⟨hl.1.2 y hy, fun hxy => hl.2 y ⟨hy, fun z hz => (hl.1.2 z hz).trans hxy⟩⟩⟩