-- Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
theorem geometric_hahn_banach_open (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) (ht : Convex ℝ t)
    (disj : Disjoint s t) : ∃ (f : E →L[ℝ] ℝ) (u : ℝ), (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b

Proof state:
case inr.intro.inr.intro.intro.intro.refine_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : x₀ ∉ C
f : E →L[ℝ] ℝ
hf₁ : f x₀ = 1
hf₂ : ∀ x ∈ C, f x < 1
this : f b₀ = f a₀ + 1
forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b
⊢ ⇑f '' s ⊆ Iio (sInf (⇑f '' t))

Tactic:
rw [← interior_Iic]

Result:
case inr.intro.inr.intro.intro.intro.refine_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : x₀ ∉ C
f : E →L[ℝ] ℝ
hf₁ : f x₀ = 1
hf₂ : ∀ x ∈ C, f x < 1
this : f b₀ = f a₀ + 1
forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b
⊢ ⇑f '' s ⊆ interior (Iic (sInf (⇑f '' t)))

Proof state:
case inr.intro.inl
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht : Convex ℝ ∅
disj : Disjoint s ∅
⊢ ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ ∅, u ≤ f b

Tactic:
exact ⟨0, 1, fun a _ha => zero_lt_one, by simp⟩

Result:
no goals

Proof state:
case inr.intro.inr.intro.intro.intro
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : x₀ ∉ C
f : E →L[ℝ] ℝ
hf₁ : f x₀ = 1
hf₂ : ∀ x ∈ C, f x < 1
this : f b₀ = f a₀ + 1
forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b
⊢ ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b

Tactic:
refine ⟨f, sInf (f '' t), image_subset_iff.1 (?_ : f '' s ⊆ Iio (sInf (f '' t))), fun b hb => ?_⟩

Result:
case inr.intro.inr.intro.intro.intro.refine_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : x₀ ∉ C
f : E →L[ℝ] ℝ
hf₁ : f x₀ = 1
hf₂ : ∀ x ∈ C, f x < 1
this : f b₀ = f a₀ + 1
forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b
⊢ ⇑f '' s ⊆ Iio (sInf (⇑f '' t))

case inr.intro.inr.intro.intro.intro.refine_2
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : x₀ ∉ C
f : E →L[ℝ] ℝ
hf₁ : f x₀ = 1
hf₂ : ∀ x ∈ C, f x < 1
this : f b₀ = f a₀ + 1
forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b
b : E
hb : b ∈ t
⊢ sInf (⇑f '' t) ≤ f b

Proof state:
case inr.intro.inr.intro
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
this✝ : 0 ∈ C
this : Convex ℝ C
⊢ ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b

Tactic:
have : x₀ ∉ C := by
  intro hx₀
  rw [← add_zero x₀] at hx₀
  exact disj.zero_not_mem_sub_set (vadd_mem_vadd_set_iff.1 hx₀)

Result:
case inr.intro.inr.intro
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ s - t
this✝¹ : 0 ∈ C
this✝ : Convex ℝ C
this : x₀ ∉ C
⊢ ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b