-- Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
theorem iInter_halfSpaces_eq (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) :
    ⋂ l : E →L[𝕜] 𝕜, { x | ∃ y ∈ s, re (l x) ≤ re (l y) } = s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : E →L[𝕜] 𝕜), ∃ y ∈ s, re (i x) ≤ re (i y)}
h : x ∉ s
⊢ False

Tactic:
obtain ⟨l, s, hlA, hl⟩ := geometric_hahn_banach_closed_point (𝕜 := 𝕜) hs₁ hs₂ h

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s✝ : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
x : E
hx : x ∈ {x | ∀ (i : E →L[𝕜] 𝕜), ∃ y ∈ s✝, re (i x) ≤ re (i y)}
h : x ∉ s✝
l : E →L[𝕜] 𝕜
s : ℝ
hlA : ∀ a ∈ s✝, re (l a) < s
hl : s < re (l x)
⊢ False

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ {x | ∀ (i : E →L[𝕜] 𝕜), ∃ y ∈ s, re (i x) ≤ re (i y)} = s

Tactic:
refine Set.Subset.antisymm (fun x hx => ?_) fun x hx l => ⟨x, hx, le_rfl⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : E →L[𝕜] 𝕜), ∃ y ∈ s, re (i x) ≤ re (i y)}
⊢ x ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ ⋂ l, {x | ∃ y ∈ s, re (l x) ≤ re (l y)} = s

Tactic:
rw [Set.iInter_setOf]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ {x | ∀ (i : E →L[𝕜] 𝕜), ∃ y ∈ s, re (i x) ≤ re (i y)} = s

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s✝ : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
x : E
hx : x ∈ {x | ∀ (i : E →L[𝕜] 𝕜), ∃ y ∈ s✝, re (i x) ≤ re (i y)}
h : x ∉ s✝
l : E →L[𝕜] 𝕜
s : ℝ
hlA : ∀ a ∈ s✝, re (l a) < s
hl : s < re (l x)
⊢ False

Tactic:
obtain ⟨y, hy, hxy⟩ := hx l

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s✝ : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
x : E
hx : x ∈ {x | ∀ (i : E →L[𝕜] 𝕜), ∃ y ∈ s✝, re (i x) ≤ re (i y)}
h : x ∉ s✝
l : E →L[𝕜] 𝕜
s : ℝ
hlA : ∀ a ∈ s✝, re (l a) < s
hl : s < re (l x)
y : E
hy : y ∈ s✝
hxy : re (l x) ≤ re (l y)
⊢ False

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : E →L[𝕜] 𝕜), ∃ y ∈ s, re (i x) ≤ re (i y)}
⊢ x ∈ s

Tactic:
by_contra h

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : E →L[𝕜] 𝕜), ∃ y ∈ s, re (i x) ≤ re (i y)}
h : x ∉ s
⊢ False

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s✝ : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
x : E
hx : x ∈ {x | ∀ (i : E →L[𝕜] 𝕜), ∃ y ∈ s✝, re (i x) ≤ re (i y)}
h : x ∉ s✝
l : E →L[𝕜] 𝕜
s : ℝ
hlA : ∀ a ∈ s✝, re (l a) < s
hl : s < re (l x)
y : E
hy : y ∈ s✝
hxy : re (l x) ≤ re (l y)
⊢ False

Tactic:
exact ((hxy.trans_lt (hlA y hy)).trans hl).false

Result:
no goals