-- Mathlib/Analysis/Convex/Exposed.lean
theorem eq_inter_halfSpace [Nontrivial 𝕜] {A B : Set E} (hAB : IsExposed 𝕜 A B) :
    ∃ l : E →L[𝕜] 𝕜, ∃ a, B = { x ∈ A | a ≤ l x }

Proof state:
case inl.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
x : E
h : 1 ≤ 0
⊢ False

Tactic:
have : ¬(1 : 𝕜) ≤ 0 := not_le_of_lt zero_lt_one

Result:
case inl.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
x : E
h : 1 ≤ 0
this : ¬1 ≤ 0
⊢ False

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
⊢ ∃ l a, B = {x | x ∈ A ∧ a ≤ l x}

Tactic:
obtain rfl | hB := B.eq_empty_or_nonempty

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∃ l a, ∅ = {x | x ∈ A ∧ a ≤ l x}

case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hB : B.Nonempty
⊢ ∃ l a, B = {x | x ∈ A ∧ a ≤ l x}

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∃ l a, ∅ = {x | x ∈ A ∧ a ≤ l x}

Tactic:
refine ⟨0, 1, ?_⟩

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∅ = {x | x ∈ A ∧ 1 ≤ 0 x}

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∀ (x : E), x ∉ {x | x ∈ A ∧ 1 ≤ 0 x}

Tactic:
rintro x ⟨-, h⟩

Result:
case inl.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
x : E
h : 1 ≤ 0 x
⊢ False

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
hB : B.Nonempty
⊢ ∃ l a, B = {x | x ∈ A ∧ a ≤ l x}

Tactic:
exact hAB.eq_inter_halfSpace' hB

Result:
no goals

Proof state:
case inl.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
x : E
h : 1 ≤ 0
this : ¬1 ≤ 0
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case inl.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
x : E
h : 1 ≤ 0 x
⊢ False

Tactic:
rw [ContinuousLinearMap.zero_apply] at h

Result:
case inl.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
x : E
h : 1 ≤ 0
⊢ False

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∅ = {x | x ∈ A ∧ 1 ≤ 0 x}

Tactic:
rw [eq_comm, eq_empty_iff_forall_not_mem]

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∀ (x : E), x ∉ {x | x ∈ A ∧ 1 ≤ 0 x}