[GOAL]
𝕜 : 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
x✝ : Set.Nonempty ∅
w✝ : E
hx : w✝ ∈ ∅
⊢ ∃ l, ∅ = {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
[PROOFSTEP]
exfalso
[GOAL]
case h
𝕜 : 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
x✝ : Set.Nonempty ∅
w✝ : E
hx : w✝ ∈ ∅
⊢ False
[PROOFSTEP]
exact hx
[GOAL]
𝕜 : 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
hAB : IsExposed 𝕜 A B
⊢ B ⊆ A
[PROOFSTEP]
rintro x hx
[GOAL]
𝕜 : 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
hAB : IsExposed 𝕜 A B
x : E
hx : x ∈ B
⊢ x ∈ A
[PROOFSTEP]
obtain ⟨_, rfl⟩ := hAB ⟨x, hx⟩
[GOAL]
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 C : Set E
X : Finset E
x✝ x : E
w✝ : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑w✝ y ≤ ↑w✝ x}
hx : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑w✝ y ≤ ↑w✝ x}
⊢ x ∈ A
[PROOFSTEP]
exact hx.1
[GOAL]
𝕜 : 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
[PROOFSTEP]
rintro ⟨w, hw⟩
[GOAL]
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}
[PROOFSTEP]
obtain ⟨l, rfl⟩ := hC ⟨w, hw⟩
[GOAL]
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}
[PROOFSTEP]
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))⟩⟩
[GOAL]
𝕜 : 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
A B : Set E
hAB : IsExposed 𝕜 A B
hB : Set.Nonempty B
⊢ ∃ l a, B = {x | x ∈ A ∧ a ≤ ↑l x}
[PROOFSTEP]
obtain ⟨l, rfl⟩ := hAB hB
[GOAL]
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
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}
[PROOFSTEP]
obtain ⟨w, hw⟩ := hB
[GOAL]
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 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}
[PROOFSTEP]
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⟩⟩
[GOAL]
𝕜 : 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
inst✝ : Nontrivial 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
⊢ ∃ l a, B = {x | x ∈ A ∧ a ≤ ↑l x}
[PROOFSTEP]
obtain rfl | hB := B.eq_empty_or_nonempty
[GOAL]
case inl
𝕜 : 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
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∃ l a, ∅ = {x | x ∈ A ∧ a ≤ ↑l x}
[PROOFSTEP]
refine' ⟨0, 1, _⟩
[GOAL]
case inl
𝕜 : 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
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∅ = {x | x ∈ A ∧ 1 ≤ ↑0 x}
[PROOFSTEP]
rw [eq_comm, eq_empty_iff_forall_not_mem]
[GOAL]
case inl
𝕜 : 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
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∀ (x : E), ¬x ∈ {x | x ∈ A ∧ 1 ≤ ↑0 x}
[PROOFSTEP]
rintro x ⟨-, h⟩
[GOAL]
case inl.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
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
x : E
h : 1 ≤ ↑0 x
⊢ False
[PROOFSTEP]
rw [ContinuousLinearMap.zero_apply] at h
[GOAL]
case inl.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
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
x : E
h : 1 ≤ 0
⊢ False
[PROOFSTEP]
have : ¬(1 : 𝕜) ≤ 0 := not_le_of_lt zero_lt_one
[GOAL]
case inl.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
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
x : E
h : 1 ≤ 0
this : ¬1 ≤ 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case inr
𝕜 : 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
inst✝ : Nontrivial 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hB : Set.Nonempty B
⊢ ∃ l a, B = {x | x ∈ A ∧ a ≤ ↑l x}
[PROOFSTEP]
exact hAB.eq_inter_halfspace' hB
[GOAL]
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
A B C : Set E
hB : IsExposed 𝕜 A B
hC : IsExposed 𝕜 A C
⊢ IsExposed 𝕜 A (B ∩ C)
[PROOFSTEP]
rintro ⟨w, hwB, hwC⟩
[GOAL]
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✝ C✝ : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
A B C : Set E
hB : IsExposed 𝕜 A B
hC : IsExposed 𝕜 A C
w : E
hwB : w ∈ B
hwC : w ∈ C
⊢ ∃ l, B ∩ C = {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
[PROOFSTEP]
obtain ⟨l₁, rfl⟩ := hB ⟨w, hwB⟩
[GOAL]
case intro.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 C✝ : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
A C : Set E
hC : IsExposed 𝕜 A C
w : E
hwC : w ∈ C
l₁ : E →L[𝕜] 𝕜
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
⊢ ∃ l, {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x} ∩ C = {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
[PROOFSTEP]
obtain ⟨l₂, rfl⟩ := hC ⟨w, hwC⟩
[GOAL]
case intro.intro.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 C : Set E
X : Finset E
x : E
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : E →L[𝕜] 𝕜
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
l₂ : E →L[𝕜] 𝕜
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
⊢ ∃ l,
    {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x} ∩ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x} =
      {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
[PROOFSTEP]
refine' ⟨l₁ + l₂, Subset.antisymm _ _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : E →L[𝕜] 𝕜
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
l₂ : E →L[𝕜] 𝕜
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
⊢ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x} ∩ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x} ⊆
    {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑(l₁ + l₂) y ≤ ↑(l₁ + l₂) x}
[PROOFSTEP]
rintro x ⟨⟨hxA, hxB⟩, ⟨-, hxC⟩⟩
[GOAL]
case intro.intro.intro.intro.refine'_1.intro.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 C : Set E
X : Finset E
x✝ : E
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : E →L[𝕜] 𝕜
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
l₂ : E →L[𝕜] 𝕜
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
x : E
hxA : x ∈ A
hxB : ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x
hxC : ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x
⊢ x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑(l₁ + l₂) y ≤ ↑(l₁ + l₂) x}
[PROOFSTEP]
exact ⟨hxA, fun z hz => add_le_add (hxB z hz) (hxC z hz)⟩
[GOAL]
case intro.intro.intro.intro.refine'_2
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : E →L[𝕜] 𝕜
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
l₂ : E →L[𝕜] 𝕜
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
⊢ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑(l₁ + l₂) y ≤ ↑(l₁ + l₂) x} ⊆
    {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x} ∩ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
[PROOFSTEP]
rintro x ⟨hxA, hx⟩
[GOAL]
case intro.intro.intro.intro.refine'_2.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
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : E →L[𝕜] 𝕜
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
l₂ : E →L[𝕜] 𝕜
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
x : E
hxA : x ∈ A
hx : ∀ (y : E), y ∈ A → ↑(l₁ + l₂) y ≤ ↑(l₁ + l₂) x
⊢ x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x} ∩ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
[PROOFSTEP]
refine' ⟨⟨hxA, fun y hy => _⟩, hxA, fun y hy => _⟩
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.refine'_1
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : E →L[𝕜] 𝕜
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
l₂ : E →L[𝕜] 𝕜
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
x : E
hxA : x ∈ A
hx : ∀ (y : E), y ∈ A → ↑(l₁ + l₂) y ≤ ↑(l₁ + l₂) x
y : E
hy : y ∈ A
⊢ ↑l₁ y ≤ ↑l₁ x
[PROOFSTEP]
exact (add_le_add_iff_right (l₂ x)).1 ((add_le_add (hwB.2 y hy) (hwC.2 x hxA)).trans (hx w hwB.1))
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.refine'_2
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : E →L[𝕜] 𝕜
hB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
hwB : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₁ y ≤ ↑l₁ x}
l₂ : E →L[𝕜] 𝕜
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
hwC : w ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l₂ y ≤ ↑l₂ x}
x : E
hxA : x ∈ A
hx : ∀ (y : E), y ∈ A → ↑(l₁ + l₂) y ≤ ↑(l₁ + l₂) x
y : E
hy : y ∈ A
⊢ ↑l₂ y ≤ ↑l₂ x
[PROOFSTEP]
exact (add_le_add_iff_left (l₁ x)).1 (le_trans (add_le_add (hwB.2 x hxA) (hwC.2 y hy)) (hx w hwB.1))
[GOAL]
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
F : Finset (Set E)
hF : Finset.Nonempty F
hAF : ∀ (B : Set E), B ∈ F → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (⋂₀ ↑F)
[PROOFSTEP]
induction F using Finset.induction with
| empty => exfalso; exact Finset.not_nonempty_empty hF
| @insert C F _ hF' =>
  rw [Finset.coe_insert, sInter_insert]
  obtain rfl | hFnemp := F.eq_empty_or_nonempty
  · rw [Finset.coe_empty, sInter_empty, inter_univ]
    exact hAF C (Finset.mem_singleton_self C)
  · exact (hAF C (Finset.mem_insert_self C F)).inter (hF' hFnemp fun B hB => hAF B (Finset.mem_insert_of_mem hB))
[GOAL]
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
F : Finset (Set E)
hF : Finset.Nonempty F
hAF : ∀ (B : Set E), B ∈ F → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (⋂₀ ↑F)
[PROOFSTEP]
induction F using Finset.induction with
| empty => exfalso; exact Finset.not_nonempty_empty hF
| @insert C F _ hF' =>
  rw [Finset.coe_insert, sInter_insert]
  obtain rfl | hFnemp := F.eq_empty_or_nonempty
  · rw [Finset.coe_empty, sInter_empty, inter_univ]
    exact hAF C (Finset.mem_singleton_self C)
  · exact (hAF C (Finset.mem_insert_self C F)).inter (hF' hFnemp fun B hB => hAF B (Finset.mem_insert_of_mem hB))
[GOAL]
case empty
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
hF : Finset.Nonempty ∅
hAF : ∀ (B : Set E), B ∈ ∅ → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (⋂₀ ↑∅)
[PROOFSTEP]

| empty => exfalso; exact Finset.not_nonempty_empty hF
[GOAL]
case empty
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
hF : Finset.Nonempty ∅
hAF : ∀ (B : Set E), B ∈ ∅ → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (⋂₀ ↑∅)
[PROOFSTEP]
exfalso
[GOAL]
case empty.h
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
hF : Finset.Nonempty ∅
hAF : ∀ (B : Set E), B ∈ ∅ → IsExposed 𝕜 A B
⊢ False
[PROOFSTEP]
exact Finset.not_nonempty_empty hF
[GOAL]
case insert
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
C : Set E
F : Finset (Set E)
a✝ : ¬C ∈ F
hF' : Finset.Nonempty F → (∀ (B : Set E), B ∈ F → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑F)
hF : Finset.Nonempty (insert C F)
hAF : ∀ (B : Set E), B ∈ insert C F → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (⋂₀ ↑(insert C F))
[PROOFSTEP]

| @insert C F _ hF' =>
  rw [Finset.coe_insert, sInter_insert]
  obtain rfl | hFnemp := F.eq_empty_or_nonempty
  · rw [Finset.coe_empty, sInter_empty, inter_univ]
    exact hAF C (Finset.mem_singleton_self C)
  · exact (hAF C (Finset.mem_insert_self C F)).inter (hF' hFnemp fun B hB => hAF B (Finset.mem_insert_of_mem hB))
[GOAL]
case insert
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
C : Set E
F : Finset (Set E)
a✝ : ¬C ∈ F
hF' : Finset.Nonempty F → (∀ (B : Set E), B ∈ F → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑F)
hF : Finset.Nonempty (insert C F)
hAF : ∀ (B : Set E), B ∈ insert C F → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (⋂₀ ↑(insert C F))
[PROOFSTEP]
rw [Finset.coe_insert, sInter_insert]
[GOAL]
case insert
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
C : Set E
F : Finset (Set E)
a✝ : ¬C ∈ F
hF' : Finset.Nonempty F → (∀ (B : Set E), B ∈ F → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑F)
hF : Finset.Nonempty (insert C F)
hAF : ∀ (B : Set E), B ∈ insert C F → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ ↑F)
[PROOFSTEP]
obtain rfl | hFnemp := F.eq_empty_or_nonempty
[GOAL]
case insert.inl
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
C : Set E
a✝ : ¬C ∈ ∅
hF' : Finset.Nonempty ∅ → (∀ (B : Set E), B ∈ ∅ → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑∅)
hF : Finset.Nonempty (insert C ∅)
hAF : ∀ (B : Set E), B ∈ insert C ∅ → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ ↑∅)
[PROOFSTEP]
rw [Finset.coe_empty, sInter_empty, inter_univ]
[GOAL]
case insert.inl
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
C : Set E
a✝ : ¬C ∈ ∅
hF' : Finset.Nonempty ∅ → (∀ (B : Set E), B ∈ ∅ → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑∅)
hF : Finset.Nonempty (insert C ∅)
hAF : ∀ (B : Set E), B ∈ insert C ∅ → IsExposed 𝕜 A B
⊢ IsExposed 𝕜 A C
[PROOFSTEP]
exact hAF C (Finset.mem_singleton_self C)
[GOAL]
case insert.inr
𝕜 : 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
inst✝ : ContinuousAdd 𝕜
C : Set E
F : Finset (Set E)
a✝ : ¬C ∈ F
hF' : Finset.Nonempty F → (∀ (B : Set E), B ∈ F → IsExposed 𝕜 A B) → IsExposed 𝕜 A (⋂₀ ↑F)
hF : Finset.Nonempty (insert C F)
hAF : ∀ (B : Set E), B ∈ insert C F → IsExposed 𝕜 A B
hFnemp : Finset.Nonempty F
⊢ IsExposed 𝕜 A (C ∩ ⋂₀ ↑F)
[PROOFSTEP]
exact (hAF C (Finset.mem_insert_self C F)).inter (hF' hFnemp fun B hB => hAF B (Finset.mem_insert_of_mem hB))
[GOAL]
𝕜 : 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
hCB : C ⊆ B
⊢ IsExposed 𝕜 (A ∩ B) C
[PROOFSTEP]
rintro ⟨w, hw⟩
[GOAL]
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
hCB : C ⊆ B
w : E
hw : w ∈ C
⊢ ∃ l, C = {x | x ∈ A ∩ B ∧ ∀ (y : E), y ∈ A ∩ B → ↑l y ≤ ↑l x}
[PROOFSTEP]
obtain ⟨l, rfl⟩ := hC ⟨w, hw⟩
[GOAL]
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 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 ∈ A ∩ B ∧ ∀ (y : E), y ∈ A ∩ B → ↑l_1 y ≤ ↑l_1 x}
[PROOFSTEP]
exact
  ⟨l,
    Subset.antisymm (fun x hx => ⟨⟨hx.1, hCB hx⟩, fun y hy => hx.2 y hy.1⟩) fun x ⟨⟨hxC, _⟩, hx⟩ =>
      ⟨hxC, fun y hy => (hw.2 y hy).trans (hx w ⟨hC.subset hw, hCB hw⟩)⟩⟩
[GOAL]
𝕜 : 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 𝕜 B C
hCA : C ⊆ A
⊢ IsExposed 𝕜 (A ∩ B) C
[PROOFSTEP]
rw [inter_comm]
[GOAL]
𝕜 : 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 𝕜 B C
hCA : C ⊆ A
⊢ IsExposed 𝕜 (B ∩ A) C
[PROOFSTEP]
exact hC.inter_left hCA
[GOAL]
𝕜 : 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
inst✝ : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
⊢ IsClosed B
[PROOFSTEP]
obtain rfl | hB := B.eq_empty_or_nonempty
[GOAL]
case inl
𝕜 : 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
inst✝ : OrderClosedTopology 𝕜
A : Set E
hA : IsClosed A
hAB : IsExposed 𝕜 A ∅
⊢ IsClosed ∅
[PROOFSTEP]
simp
[GOAL]
case inr
𝕜 : 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
inst✝ : OrderClosedTopology 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hA : IsClosed A
hB : Set.Nonempty B
⊢ IsClosed B
[PROOFSTEP]
obtain ⟨l, a, rfl⟩ := hAB.eq_inter_halfspace' hB
[GOAL]
case inr.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 C : Set E
X : Finset E
x : E
inst✝ : OrderClosedTopology 𝕜
A : Set E
hA : IsClosed A
l : E →L[𝕜] 𝕜
a : 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ a ≤ ↑l x}
hB : Set.Nonempty {x | x ∈ A ∧ a ≤ ↑l x}
⊢ IsClosed {x | x ∈ A ∧ a ≤ ↑l x}
[PROOFSTEP]
exact hA.isClosed_le continuousOn_const l.continuous.continuousOn
[GOAL]
𝕜 : 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
⊢ x ∈ exposedPoints 𝕜 A ↔ IsExposed 𝕜 A {x}
[PROOFSTEP]
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)⟩⟩
[GOAL]
case mpr
𝕜 : 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
⊢ IsExposed 𝕜 A {x} → x ∈ exposedPoints 𝕜 A
[PROOFSTEP]
rintro h
[GOAL]
case mpr
𝕜 : 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
h : IsExposed 𝕜 A {x}
⊢ x ∈ exposedPoints 𝕜 A
[PROOFSTEP]
obtain ⟨l, hl⟩ := h ⟨x, mem_singleton _⟩
[GOAL]
case mpr.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
h : IsExposed 𝕜 A {x}
l : E →L[𝕜] 𝕜
hl : {x} = {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
⊢ x ∈ exposedPoints 𝕜 A
[PROOFSTEP]
rw [eq_comm, eq_singleton_iff_unique_mem] at hl
[GOAL]
case mpr.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
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
[PROOFSTEP]
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⟩⟩⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hAB : IsExposed 𝕜 A B
hA : Convex 𝕜 A
⊢ Convex 𝕜 B
[PROOFSTEP]
obtain rfl | hB := B.eq_empty_or_nonempty
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
hA : Convex 𝕜 A
hAB : IsExposed 𝕜 A ∅
⊢ Convex 𝕜 ∅
[PROOFSTEP]
exact convex_empty
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hAB : IsExposed 𝕜 A B
hA : Convex 𝕜 A
hB : Set.Nonempty B
⊢ Convex 𝕜 B
[PROOFSTEP]
obtain ⟨l, rfl⟩ := hAB hB
[GOAL]
case inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
hA : Convex 𝕜 A
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}
⊢ Convex 𝕜 {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
[PROOFSTEP]
exact fun x₁ hx₁ x₂ hx₂ a b ha hb hab =>
  ⟨hA hx₁.1 hx₂.1 ha hb hab, fun y hy =>
    ((l.toLinearMap.concaveOn convex_univ).convex_ge _ ⟨mem_univ _, hx₁.2 y hy⟩ ⟨mem_univ _, hx₂.2 y hy⟩ ha hb hab).2⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hAB : IsExposed 𝕜 A B
⊢ IsExtreme 𝕜 A B
[PROOFSTEP]
refine' ⟨hAB.subset, fun x₁ hx₁A x₂ hx₂A x hxB hx => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hAB : IsExposed 𝕜 A B
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxB : x ∈ B
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ B ∧ x₂ ∈ B
[PROOFSTEP]
obtain ⟨l, rfl⟩ := hAB ⟨x, hxB⟩
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
⊢ x₁ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
[PROOFSTEP]
have hl : ConvexOn 𝕜 univ l := l.toLinearMap.convexOn convex_univ
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
⊢ x₁ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
[PROOFSTEP]
have hlx₁ := hxB.2 x₁ hx₁A
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
⊢ x₁ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
[PROOFSTEP]
have hlx₂ := hxB.2 x₂ hx₂A
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
⊢ x₁ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
[PROOFSTEP]
refine' ⟨⟨hx₁A, fun y hy => _⟩, ⟨hx₂A, fun y hy => _⟩⟩
[GOAL]
case intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
y : E
hy : y ∈ A
⊢ ↑l y ≤ ↑l x₁
[PROOFSTEP]
rw [hlx₁.antisymm (hl.le_left_of_right_le (mem_univ _) (mem_univ _) hx hlx₂)]
[GOAL]
case intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
y : E
hy : y ∈ A
⊢ ↑l y ≤ ↑l x
[PROOFSTEP]
exact hxB.2 y hy
[GOAL]
case intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
y : E
hy : y ∈ A
⊢ ↑l y ≤ ↑l x₂
[PROOFSTEP]
rw [hlx₂.antisymm (hl.le_right_of_left_le (mem_univ _) (mem_univ _) hx hlx₁)]
[GOAL]
case intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A C : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hx : x ∈ openSegment 𝕜 x₁ x₂
l : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hxB : x ∈ {x | x ∈ A ∧ ∀ (y : E), y ∈ A → ↑l y ≤ ↑l x}
hl : ConvexOn 𝕜 univ ↑l
hlx₁ : ↑l x₁ ≤ ↑l x
hlx₂ : ↑l x₂ ≤ ↑l x
y : E
hy : y ∈ A
⊢ ↑l y ≤ ↑l x
[PROOFSTEP]
exact hxB.2 y hy