awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
inl :
  ∀ (hs₁ : Convex.{0, u_2} ℝ (E := E) ∅) (hs₂ : IsOpen.{u_2} (X := E) ∅) (disj : Disjoint ∅ t),
    ∃ (f : StrongDual ℝ E) (u : ℝ),
      (∀ (a : E), Membership.mem (γ := Set E) ∅ a → (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
inr :
  ∀ (a₀ : E) (ha₀ : a₀ ∈ s),
    ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b

Tactic:
obtain rfl | ⟨a₀, ha₀⟩ := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
ht : Convex ℝ t
hs₁ : Convex.{0, u_2} ℝ (E := E) ∅
hs₂ : IsOpen.{u_2} (X := E) ∅
disj : Disjoint ∅ t
⊢ ∀ (a : E), Membership.mem (γ := Set E) ∅ a → LT.lt (α := ℝ) ((0 : (a : E) → ℝ) a : ℝ) (0 : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
ht : Convex ℝ t
hs₁ : Convex.{0, u_2} ℝ (E := E) ∅
hs₂ : IsOpen.{u_2} (X := E) ∅
disj : Disjoint ∅ t
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ),
    (∀ (a : E), Membership.mem (γ := Set E) ∅ a → (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b

Tactic:
exact ⟨0, 0, by simp, fun b _hb => le_rfl⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
inr :
  ∀ (ht : Convex.{0, u_2} ℝ (E := E) ∅) (disj : Disjoint s ∅),
    ∃ (f : StrongDual ℝ E) (u : ℝ),
      (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ (b : E), Membership.mem (γ := Set E) ∅ b → u ≤ (f : (a : E) → ℝ) b
inr₁ :
  ∀ (b₀ : E) (hb₀ : b₀ ∈ t),
    ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b

Tactic:
obtain rfl | ⟨b₀, hb₀⟩ := t.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht : Convex.{0, u_2} ℝ (E := E) ∅
disj : Disjoint s ∅
⊢ ∀ (b : E), Membership.mem (γ := Set E) ∅ b → LE.le (α := ℝ) (1 : ℝ) ((0 : (a : E) → ℝ) b : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht : Convex.{0, u_2} ℝ (E := E) ∅
disj : Disjoint s ∅
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ),
    (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ (b : E), Membership.mem (γ := Set E) ∅ b → u ≤ (f : (a : E) → ℝ) b

Tactic:
exact ⟨0, 1, fun a _ha => zero_lt_one, by simp⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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
simp_rw simp_rw₁ : x₀ +ᵥ a₀ - b₀ = 0
simp_rw₂ : (b₀ - a₀) +ᵥ a₀ - b₀ = 0
simp_rw₃ : b₀ - a₀ + (a₀ - b₀) = 0
simp_rw₄ : a₀ - a₀ = 0
⊢ Eq.{u_2 + 1} (α := E) ((fun (x : E) ↦ x₀ +ᵥ x) (a₀ - b₀)) 0

Tactic:
simp_rw [x₀, vadd_eq_add, sub_add_sub_cancel', sub_self]

Premises used: sub_self, sub_add_sub_cancel', vadd_eq_add
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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
⊢ 0 ∈ C

Tactic:
have : (0 : E) ∈ C :=
    ⟨a₀ - b₀, sub_mem_sub ha₀ hb₀, by simp_rw [x₀, vadd_eq_add, sub_add_sub_cancel', sub_self]⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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
⊢ Convex ℝ C

Tactic:
have : Convex ℝ C := (hs₁.sub ht).vadd _
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this : Convex ℝ C
hx₀ : x₀ ∈ C
⊢ x₀ + 0 ∈ C

Tactic:
rw [← add_zero x₀] at hx₀

Premises used: add_zero
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this : Convex ℝ C
hx₀ : x₀ + 0 ∈ C
⊢ False

Tactic:
disj.zero_notMem_sub_set (vadd_mem_vadd_set_iff.1 hx₀)

Premises used: Set.vadd_mem_vadd_set_iff, Iff.mp, Disjoint.zero_notMem_sub_set
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this : Convex ℝ C
hx₀ : x₀ + 0 ∈ C
⊢ False

Tactic:
exact disj.zero_notMem_sub_set (vadd_mem_vadd_set_iff.1 hx₀)

Premises used: Set.vadd_mem_vadd_set_iff, Iff.mp, Disjoint.zero_notMem_sub_set
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this : Convex ℝ C
⊢ x₀ ∉ C

Tactic:
have : x₀ ∉ C := by
    intro hx₀
    rw [← add_zero x₀] at hx₀
    exact disj.zero_notMem_sub_set (vadd_mem_vadd_set_iff.1 hx₀)
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this : x₀ ∉ C
inr :
  ∀ (f : StrongDual ℝ E) (hf₁ : Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ))
    (hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)),
    ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := separate_convex_open_set ‹0 ∈ C› ‹_› (hs₂.sub_right.vadd _) ‹x₀ ∉ C›

Premises used: separate_convex_open_set, IsOpen.sub_right, IsOpen.vadd
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
a : E
ha : a ∈ s
b : E
hb : b ∈ t
⊢ LT.lt (α := ℝ) ((f : (a : E) → ℝ) (x₀ + (a - b)) : ℝ) (1 : ℝ)

Tactic:
have := hf₂ (x₀ + (a - b)) (vadd_mem_vadd_set <| sub_mem_sub ha hb)
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this_3 : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
a : E
ha : a ∈ s
b : E
hb : b ∈ t
this : LT.lt (α := ℝ) ((f : (a : E) → ℝ) (x₀ + (a - b)) : ℝ) (1 : ℝ)
⊢ 1 + HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ) < 1

Tactic:
simp only [f.map_add, f.map_sub, hf₁] at this

Premises used: ContinuousLinearMap.map_sub, ContinuousLinearMap.map_add
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this_3 : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
a : E
ha : a ∈ s
b : E
hb : b ∈ t
this : 1 + HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ) < 1
linarith :
  LT.lt (α := ℝ) ((f : (a : E) → ℝ) b : ℝ) ((f : (a : E) → ℝ) a : ℝ) →
    1 + HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ) - 1 +
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : E) → ℝ) b : ℝ) ((f : (a : E) → ℝ) a : ℝ) =
      0
⊢ LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
⊢ ∀ a ∈ s, ∀ b ∈ t, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ)

Tactic:
have forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b := by
    intro a ha b hb
    have := hf₂ (x₀ + (a - b)) (vadd_mem_vadd_set <| sub_mem_sub ha hb)
    simp only [f.map_add, f.map_sub, hf₁] at this
    linarith
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
forall_le : ∀ a ∈ s, ∀ b ∈ t, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ)
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b

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

Premises used: And.intro, Exists.intro, Iff.mp, Set.image, Set.image_subset_iff, DFunLike.coe, InfSet.sInf
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
forall_le : ∀ a ∈ s, ∀ b ∈ t, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ)
inr : Subset (α := Set ℝ) ((⇑f : (a : E) → ℝ) '' s) (Iio (sInf ((⇑f : (a : E) → ℝ) '' t)))
inr₁ : ∀ (b : E) (hb : b ∈ t), LE.le (α := ℝ) (sInf ((⇑f : (a : E) → ℝ) '' t) : ℝ) ((f : (a : E) → ℝ) b : ℝ)
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b

Tactic:
refine ⟨f, sInf (f '' t), image_subset_iff.1 (?_ : f '' s ⊆ Iio (sInf (f '' t))), fun b hb => ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
forall_le : ∀ a ∈ s, ∀ b ∈ t, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ)
inr : Subset (α := Set ℝ) ((⇑f : (a : E) → ℝ) '' s) (interior (Iic (sInf ((⇑f : (a : E) → ℝ) '' t))))
⊢ Subset (α := Set ℝ) ((⇑f : (a : E) → ℝ) '' s) (Iio (sInf ((⇑f : (a : E) → ℝ) '' t)))

Tactic:
rw [← interior_Iic]

Premises used: interior_Iic
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
forall_le : ∀ a ∈ s, ∀ b ∈ t, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ)
⊢ Subset (α := Set ℝ) ((⇑f : (a : E) → ℝ) '' s) (interior (Iic (sInf ((⇑f : (a : E) → ℝ) '' t))))

Tactic:
interior_maximal (image_subset_iff.2 fun a ha => ?_) (f.isOpenMap_of_ne_zero ?_ _ hs₂)

Premises used: Iff.mpr, interior_maximal, Set.image_subset_iff, ContinuousLinearMap.isOpenMap_of_ne_zero
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
forall_le : ∀ a ∈ s, ∀ b ∈ t, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ)
inr :
  ∀ (a : E) (ha : a ∈ s),
    Membership.mem (γ := Set E) (preimage (β := ℝ) (⇑f : (a : E) → ℝ) (Iic (sInf ((⇑f : (a : E) → ℝ) '' t)))) a
inr₁ : f ≠ 0
⊢ Subset (α := Set ℝ) ((⇑f : (a : E) → ℝ) '' s) (interior (Iic (sInf ((⇑f : (a : E) → ℝ) '' t))))

Tactic:
refine interior_maximal (image_subset_iff.2 fun a ha => ?_) (f.isOpenMap_of_ne_zero ?_ _ hs₂)

Premises used: Iff.mpr, interior_maximal, Set.image_subset_iff, ContinuousLinearMap.isOpenMap_of_ne_zero
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
forall_le : ∀ a ∈ s, ∀ b ∈ t, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ)
a : E
ha : a ∈ s
⊢ Membership.mem (γ := Set E) (preimage (β := ℝ) (⇑f : (a : E) → ℝ) (Iic (sInf ((⇑f : (a : E) → ℝ) '' t)))) a

Tactic:
le_csInf (Nonempty.image _ ⟨_, hb₀⟩) (forall_mem_image.2 <| forall_le _ ha)

Premises used: Iff.mpr, Set.Mem, le_csInf, setOf, Set.preimage, Set.Nonempty.image, Exists.intro, Set.Iic, Set.forall_mem_image
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
forall_le : ∀ a ∈ s, ∀ b ∈ t, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ)
a : E
ha : a ∈ s
⊢ Membership.mem (γ := Set E) (preimage (β := ℝ) (⇑f : (a : E) → ℝ) (Iic (sInf ((⇑f : (a : E) → ℝ) '' t)))) a

Tactic:
exact le_csInf (Nonempty.image _ ⟨_, hb₀⟩) (forall_mem_image.2 <| forall_le _ ha)

Premises used: Iff.mpr, le_csInf, Set.Nonempty.image, Exists.intro, Set.forall_mem_image
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this : x₀ ∉ C
hf₁ : Eq (α := ℝ) ((0 : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((0 : (a : E) → ℝ) x : ℝ) (1 : ℝ)
forall_le : ∀ a ∈ s, ∀ b ∈ t, LE.le (α := ℝ) ((0 : (a : E) → ℝ) a : ℝ) ((0 : (a : E) → ℝ) b : ℝ)
⊢ False

Tactic:
simp at hf₁
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
forall_le : ∀ a ∈ s, ∀ b ∈ t, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ)
b : E
hb : b ∈ t
⊢ LE.le (α := ℝ) (sInf ((⇑f : (a : E) → ℝ) '' t) : ℝ) ((f : (a : E) → ℝ) b : ℝ)

Tactic:
csInf_le ⟨f a₀, forall_mem_image.2 <| forall_le _ ha₀⟩ (mem_image_of_mem _ hb)

Premises used: Iff.mpr, Set.mem_image_of_mem, Exists.intro, csInf_le, DFunLike.coe, Set.forall_mem_image
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : 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_1 : 0 ∈ C
this_2 : Convex ℝ C
this : x₀ ∉ C
f : StrongDual ℝ E
hf₁ : Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hf₂ : ∀ x ∈ C, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
forall_le : ∀ a ∈ s, ∀ b ∈ t, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ)
b : E
hb : b ∈ t
⊢ LE.le (α := ℝ) (sInf ((⇑f : (a : E) → ℝ) '' t) : ℝ) ((f : (a : E) → ℝ) b : ℝ)

Tactic:
exact csInf_le ⟨f a₀, forall_mem_image.2 <| forall_le _ ha₀⟩ (mem_image_of_mem _ hb)

Premises used: Iff.mpr, Set.mem_image_of_mem, Exists.intro, csInf_le, DFunLike.coe, Set.forall_mem_image
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s : Set E
x : E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
disj : x ∉ s
⊢ ∃ (f : StrongDual ℝ E), ∀ a ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)

Tactic:
let ⟨f, _s, hs, hx⟩ :=
    geometric_hahn_banach_open hs₁ hs₂ (convex_singleton x) (disjoint_singleton_right.2 disj)
  ⟨f, fun a ha => lt_of_lt_of_le (hs a ha) (hx x (mem_singleton _))⟩

Premises used: geometric_hahn_banach_open, Iff.mpr, Set.mem_singleton, Set.disjoint_singleton_right, convex_singleton, Exists, Exists.intro, _private.0.geometric_hahn_banach_open_point.match_1, lt_of_lt_of_le
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
t : Set E
x : E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
ht₁ : Convex ℝ t
ht₂ : IsOpen t
disj : x ∉ t
f : StrongDual ℝ E
hf : ∀ a ∈ t, LT.lt (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)
⊢ ∀ b ∈ t, LT.lt (α := ℝ) ((-f : (a : E) → ℝ) x : ℝ) ((-f : (a : E) → ℝ) b : ℝ)

Tactic:
simpa
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
inl :
  ∀ (hs₁ : Convex.{0, u_2} ℝ (E := E) ∅) (hs₂ : IsOpen.{u_2} (X := E) ∅) (disj : Disjoint ∅ t),
    ∃ (f : StrongDual ℝ E) (u : ℝ),
      (∀ (a : E), Membership.mem (γ := Set E) ∅ a → (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b
inr :
  ∀ (a₀ : E) (ha₀ : a₀ ∈ s),
    ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b

Tactic:
obtain rfl | ⟨a₀, ha₀⟩ := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
ht₁ : Convex ℝ t
ht₃ : IsOpen t
hs₁ : Convex.{0, u_2} ℝ (E := E) ∅
hs₂ : IsOpen.{u_2} (X := E) ∅
disj : Disjoint ∅ t
⊢ ∀ (a : E), Membership.mem (γ := Set E) ∅ a → LT.lt (α := ℝ) ((0 : (a : E) → ℝ) a : ℝ) (-1 : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.Separation
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
ht₁ : Convex ℝ t
ht₃ : IsOpen t
hs₁ : Convex.{0, u_2} ℝ (E := E) ∅
hs₂ : IsOpen.{u_2} (X := E) ∅
disj : Disjoint ∅ t
b : E
_hb : b ∈ t
⊢ LT.lt (α := ℝ) (-1 : ℝ) ((0 : (a : E) → ℝ) b : ℝ)

Tactic:
simp