-- Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
theorem separate_convex_open_set {s : Set E}
    (hs₀ : (0 : E) ∈ s) (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) {x₀ : E} (hx₀ : x₀ ∉ s) :
    ∃ f : E →L[𝕜] 𝕜, re (f x₀) = 1 ∧ ∀ x ∈ s, re (f x) < 1

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

Tactic:
simp only [re_extendTo𝕜'ₗ]

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

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

Tactic:
obtain ⟨g, hg⟩ := _root_.separate_convex_open_set hs₀ hs₁ hs₂ hx₀

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

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

Tactic:
use extendTo𝕜'ₗ g

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

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

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

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

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

Tactic:
exact hg

Result:
no goals