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
A : Set E
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hB : Set.Nonempty {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
⊢ ∃ l_1 a, {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} = {x | x ∈ A ∧ a ≤ ↑l_1 x}
𝕜 : 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
A B : Set E
hAB : IsExposed 𝕜 A B
hB : Set.Nonempty B
⊢ ∃ l a, B = {x | x ∈ A ∧ a ≤ ↑l x}
obtain ⟨l, rfl⟩ := hAB hB
case intro.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
A : Set E
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
w : E
hw : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
⊢ ∃ l_1 a, {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} = {x | x ∈ A ∧ a ≤ ↑l_1 x}
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
A : Set E
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hB : Set.Nonempty {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
⊢ ∃ l_1 a, {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} = {x | x ∈ A ∧ a ≤ ↑l_1 x}
obtain ⟨w, hw⟩ := hB
no goals
case intro.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
A : Set E
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
w : E
hw : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
⊢ ∃ l_1 a, {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} = {x | x ∈ A ∧ a ≤ ↑l_1 x}
exact ⟨l, l w, Subset.antisymm (fun x hx => ⟨hx.1, hx.2 w hw.1⟩) fun x hx =>
  ⟨hx.1, fun y hy => (hw.2 y hy).trans hx.2⟩⟩