case intro
𝕜 : Type u_1
E : Type u_2
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
hC : IsExposed 𝕜 A C
hBA : B ⊆ A
hCB : C ⊆ B
w : E
hw : w ∈ C
⊢ ∃ l, C = {x | x ∈ B ∧ ∀ (y : E), y ∈ B → ↑l y ≤ ↑l x}
𝕜 : Type u_1
E : Type u_2
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
hC : IsExposed 𝕜 A C
hBA : B ⊆ A
hCB : C ⊆ B
⊢ IsExposed 𝕜 B C
rintro ⟨w, hw⟩
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
l✝ : E →L[𝕜] 𝕜
A B : Set E
X : Finset E
x : E
hBA : B ⊆ A
w : E
l : E →L[𝕜] 𝕜
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hCB : {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ⊆ B
hw : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
⊢ ∃ l_1, {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} = {x | x ∈ B ∧ ∀ (y : E), y ∈ B → ↑l_1 y ≤ ↑l_1 x}
case intro
𝕜 : Type u_1
E : Type u_2
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
hC : IsExposed 𝕜 A C
hBA : B ⊆ A
hCB : C ⊆ B
w : E
hw : w ∈ C
⊢ ∃ l, C = {x | x ∈ B ∧ ∀ (y : E), y ∈ B → ↑l y ≤ ↑l x}
obtain ⟨l, rfl⟩ := hC ⟨w, hw⟩
no goals
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
l✝ : E →L[𝕜] 𝕜
A B : Set E
X : Finset E
x : E
hBA : B ⊆ A
w : E
l : E →L[𝕜] 𝕜
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hCB : {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ⊆ B
hw : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
⊢ ∃ l_1, {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} = {x | x ∈ B ∧ ∀ (y : E), y ∈ B → ↑l_1 y ≤ ↑l_1 x}
exact ⟨l, Subset.antisymm (fun x hx => ⟨hCB hx, fun y hy => hx.2 y (hBA hy)⟩) fun x hx =>
  ⟨hBA hx.1, fun y hy => (hw.2 y hy).trans (hx.2 w (hCB hw))⟩⟩