-- Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
theorem geometric_hahn_banach_open_point (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) (disj : x ∉ s) :
    ∃ f : E →L[𝕜] 𝕜, ∀ a ∈ s, re (f a) < re (f x)

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
x : E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
this : ContinuousSMul ℝ E
f : E →L[ℝ] ℝ
h : ∀ a ∈ s, f a < f x
⊢ ∃ f, ∀ a ∈ s, re (f a) < re (f x)

Tactic:
use extendTo𝕜'ₗ f

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
x : E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
this : ContinuousSMul ℝ E
f : E →L[ℝ] ℝ
h : ∀ a ∈ s, f a < f x
⊢ ∀ a ∈ s, re ((extendTo𝕜'ₗ f) a) < re ((extendTo𝕜'ₗ f) x)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
x : E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
this : ContinuousSMul ℝ E
⊢ ∃ f, ∀ a ∈ s, re (f a) < re (f x)

Tactic:
obtain ⟨f, h⟩ := _root_.geometric_hahn_banach_open_point hs₁ hs₂ disj

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
x : E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
this : ContinuousSMul ℝ E
f : E →L[ℝ] ℝ
h : ∀ a ∈ s, f a < f x
⊢ ∃ f, ∀ a ∈ s, re (f a) < re (f x)

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
x : E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
this : ContinuousSMul ℝ E
f : E →L[ℝ] ℝ
h : ∀ a ∈ s, f a < f x
⊢ ∀ a ∈ s, f a < f x

Tactic:
exact fun a a_1 ↦ h a a_1

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
x : E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
⊢ ∃ f, ∀ a ∈ s, re (f a) < re (f x)

Tactic:
have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
x : E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
this : ContinuousSMul ℝ E
⊢ ∃ f, ∀ a ∈ s, re (f a) < re (f x)

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
x : E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
this : ContinuousSMul ℝ E
f : E →L[ℝ] ℝ
h : ∀ a ∈ s, f a < f x
⊢ ∀ a ∈ s, re ((extendTo𝕜'ₗ f) a) < re ((extendTo𝕜'ₗ f) x)

Tactic:
simp only [re_extendTo𝕜'ₗ]

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
s : Set E
x : E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
this : ContinuousSMul ℝ E
f : E →L[ℝ] ℝ
h : ∀ a ∈ s, f a < f x
⊢ ∀ a ∈ s, f a < f x