awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b
have 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
Tactic: obtain rfl | ⟨a₀, ha₀⟩ := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs₁, hs₂, disj
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b
have inr : ∀ (a₀ : E) (ha₀ : a₀ ∈ s),
  ∃ (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
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
a₀ : E
ha₀ : a₀ ∈ s
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b
have inr : ∀ (ht₁ : Convex.{0, u_2} ℝ (E := E) ∅) (ht₃ : IsOpen.{u_2} (X := 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: obtain rfl | ⟨b₀, hb₀⟩ := t.eq_empty_or_nonempty
Cleared hypotheses: t, ht₁, ht₃, disj
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
a₀ : E
ha₀ : a₀ ∈ s
inr :
  ∀ (ht₁ : Convex.{0, u_2} ℝ (E := E) ∅) (ht₃ : IsOpen.{u_2} (X := 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
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b
have inr₁ : ∀ (b₀ : E) (hb₀ : b₀ ∈ t),
  ∃ (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
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b
have inr : ∀ (f : StrongDual ℝ E) (s_1 : ℝ) (hf₁ : ∀ a ∈ s, (f : (a : E) → ℝ) a < s_1) (hf₂ : ∀ b ∈ t, s_1 ≤ (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, s, hf₁, hf₂⟩ := geometric_hahn_banach_open hs₁ hs₂ ht₁ disj
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsOpen s_1
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s_1 t
a₀ : E
ha₀ : a₀ ∈ s_1
b₀ : E
hb₀ : b₀ ∈ t
f : StrongDual ℝ E
s : ℝ
hf₁ : ∀ a ∈ s_1, (f : (a : E) → ℝ) a < s
hf₂ : ∀ b ∈ t, s ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s_1, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u < (f : (a : E) → ℝ) b
have inr : (⇑f : (a : E) → ℝ) '' t ⊆ Ioi s
Tactic: refine ⟨f, s, hf₁, image_subset_iff.1 (?_ : f '' t ⊆ Ioi s)⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsOpen s_1
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s_1 t
a₀ : E
ha₀ : a₀ ∈ s_1
b₀ : E
hb₀ : b₀ ∈ t
f : StrongDual ℝ E
s : ℝ
hf₁ : ∀ a ∈ s_1, (f : (a : E) → ℝ) a < s
hf₂ : ∀ b ∈ t, s ≤ (f : (a : E) → ℝ) b
⊢ (⇑f : (a : E) → ℝ) '' t ⊆ Ioi s
have inr : (⇑f : (a : E) → ℝ) '' t ⊆ interior (Ici s)
Tactic: rw [← interior_Ici]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
s_1 t : Set E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s_1
hs₂ : IsOpen s_1
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s_1 t
a₀ : E
ha₀ : a₀ ∈ s_1
b₀ : E
hb₀ : b₀ ∈ t
f : StrongDual ℝ E
s : ℝ
hf₁ : ∀ a ∈ s_1, (f : (a : E) → ℝ) a < s
hf₂ : ∀ b ∈ t, s ≤ (f : (a : E) → ℝ) b
⊢ (⇑f : (a : E) → ℝ) '' t ⊆ interior (Ici s)
have inr : f ≠ 0
Tactic: refine interior_maximal (image_subset_iff.2 hf₂) (f.isOpenMap_of_ne_zero ?_ _ ht₃)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), f ≠ 0 ∧ (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
have obtain : ∀ (f : StrongDual ℝ E) (u : ℝ) (hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u)
  (hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b),
  ∃ (f : StrongDual ℝ E) (u : ℝ), f ≠ 0 ∧ (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
Tactic: obtain ⟨f, u, hfA, hfB⟩ :=
    geometric_hahn_banach_open hs.interior isOpen_interior ht hst
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), f ≠ 0 ∧ (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
have refine_1 : f ≠ 0
Tactic: refine ⟨f, u, ?_, fun a ha ↦ ?_, hfB⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
refine_1 : f ≠ 0
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), f ≠ 0 ∧ (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
have refine_2 : ∀ (a : E) (ha : a ∈ s), (f : (a : E) → ℝ) a ≤ u
Tactic: refine ⟨f, u, ?_, fun a ha ↦ ?_, hfB⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
⊢ f ≠ 0
have refine_1 : ∀ (a : E) (ha : a ∈ interior s), f ≠ 0
Tactic: obtain ⟨a, ha⟩ := hsint
Cleared hypotheses: hsint
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
ht : Convex ℝ t
hst : Disjoint (interior s) t
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
a : E
ha : a ∈ interior s
⊢ f ≠ 0
have refine_1 : ∀ (b : E) (hb : b ∈ t), f ≠ 0
Tactic: obtain ⟨b, hb⟩ := htne
Cleared hypotheses: htne
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (hypothesis)
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
ht : Convex ℝ t
hst : Disjoint (interior s) t
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
a : E
ha : a ∈ interior s
b : E
hb : b ∈ t
hzero : f = 0
⊢ False
have ha' : 0 < u
Tactic: have ha' : (0 : ℝ) < u := by simpa [hzero] using hfA a ha
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (hypothesis)
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
ht : Convex ℝ t
hst : Disjoint (interior s) t
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
a : E
ha : a ∈ interior s
b : E
hb : b ∈ t
hzero : f = 0
ha' : 0 < u
⊢ False
have hb' : u ≤ 0
Tactic: have hb' : u ≤ (0 : ℝ) := by simpa [hzero] using hfB b hb
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
ht : Convex ℝ t
hst : Disjoint (interior s) t
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
a : E
ha : a ∈ interior s
b : E
hb : b ∈ t
hzero : f = 0
ha' : 0 < u
hb' : u ≤ 0
⊢ False
have linarith : 0 - u + (u - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
f : StrongDual ℝ E
u : ℝ
hfA : ∀ a ∈ interior s, (f : (a : E) → ℝ) a < u
hfB : ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
a : E
ha : a ∈ s
⊢ (f : (a : E) → ℝ) a ≤ u
have refine_2 : a ∈ closure (interior s)
Tactic: apply closure_minimal (fun x hx => le_of_lt (hfA x hx)) <| isClosed_Iic.preimage f.continuous
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
have pos : ∀ (htne : t.Nonempty),
  ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
Tactic: by_cases htne : t.Nonempty
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
pos :
  ∀ (htne : t.Nonempty),
    ∃ (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
have neg : ∀ (htne : ¬t.Nonempty),
  ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
Tactic: by_cases htne : t.Nonempty
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
have pos : ∀ (f : StrongDual ℝ E) (u : ℝ) (hs' : ∀ a ∈ s, (f : (a : E) → ℝ) a ≤ u) (ht' : ∀ 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, u, -, hs', ht'⟩ :=
      geometric_hahn_banach_of_nonempty_interior hs ht hst hsint htne
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
x : E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
A : Set E
hA : Convex ℝ A
hxA : x ∉ interior A
hAint : (interior A).Nonempty
⊢ ∃ (f : StrongDual ℝ E), f ≠ 0 ∧ ∀ a ∈ A, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)
have obtain : ∀ (f : StrongDual ℝ E) (u : ℝ) (hfne : f ≠ 0) (hA' : ∀ a ∈ A, (f : (a : E) → ℝ) a ≤ u)
  (hx' : ∀ (b : E), Membership.mem (γ := Set E) {x} b → u ≤ (f : (a : E) → ℝ) b),
  ∃ (f : StrongDual ℝ E), f ≠ 0 ∧ ∀ a ∈ A, LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)
Tactic: obtain ⟨f, u, hfne, hA', hx'⟩ :=
    geometric_hahn_banach_of_nonempty_interior hA (convex_singleton x)
      (disjoint_singleton_right.2 hxA) hAint (singleton_nonempty x)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
have inl : ∀ (hs₁ : Convex.{0, u_2} ℝ (E := E) ∅) (hs₂ : IsCompact.{u_2} (X := E) ∅) (disj : Disjoint ∅ t),
  ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ),
    (∀ (a : E), Membership.mem (γ := Set E) ∅ a → (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs₁, hs₂, disj
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
inl :
  ∀ (hs₁ : Convex.{0, u_2} ℝ (E := E) ∅) (hs₂ : IsCompact.{u_2} (X := E) ∅) (disj : Disjoint ∅ t),
    ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ),
      (∀ (a : E), Membership.mem (γ := Set E) ∅ a → (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
have inr : ∀ (hs : s.Nonempty),
  ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
have inr : ∀ (ht₁ : Convex.{0, u_2} ℝ (E := E) ∅) (ht₂ : IsClosed.{u_2} (X := E) ∅) (disj : Disjoint s ∅),
  ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ),
    (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ (b : E), Membership.mem (γ := Set E) ∅ b → v < (f : (a : E) → ℝ) b
Tactic: obtain rfl | _ht := t.eq_empty_or_nonempty
Cleared hypotheses: t, ht₁, ht₂, disj
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
inr :
  ∀ (ht₁ : Convex.{0, u_2} ℝ (E := E) ∅) (ht₂ : IsClosed.{u_2} (X := E) ∅) (disj : Disjoint s ∅),
    ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ),
      (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ (b : E), Membership.mem (γ := Set E) ∅ b → v < (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
have inr₁ : ∀ (_ht : t.Nonempty),
  ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
Tactic: obtain rfl | _ht := t.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
_ht : t.Nonempty
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
have inr : ∀ (U V : Set E) (hU : IsOpen U) (hV : IsOpen V) (hU₁ : Convex ℝ U) (hV₁ : Convex ℝ V) (sU : s ⊆ U) (tV : t ⊆ V)
  (disj' : Disjoint U V),
  ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
Tactic: obtain ⟨U, V, hU, hV, hU₁, hV₁, sU, tV, disj'⟩ := disj.exists_open_convexes hs₁ hs₂ ht₁ ht₂
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
have inr : ∀ (f : StrongDual ℝ E) (u : ℝ) (hf₁ : ∀ a ∈ U, (f : (a : E) → ℝ) a < u) (hf₂ : ∀ b ∈ V, u < (f : (a : E) → ℝ) b),
  ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
Tactic: obtain ⟨f, u, hf₁, hf₂⟩ := geometric_hahn_banach_open_open hU₁ hU hV₁ hV disj'
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : StrongDual ℝ E
u : ℝ
hf₁ : ∀ a ∈ U, (f : (a : E) → ℝ) a < u
hf₂ : ∀ b ∈ V, u < (f : (a : E) → ℝ) b
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
have inr : ∀ (x : E) (hx₁ : x ∈ s) (hx₂ : IsMaxOn (β := ℝ) (⇑f : (a : E) → ℝ) s x),
  ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
Tactic: obtain ⟨x, hx₁, hx₂⟩ := hs₂.exists_isMaxOn hs f.continuous.continuousOn
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (hypothesis)
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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : StrongDual ℝ E
u : ℝ
hf₁ : ∀ a ∈ U, (f : (a : E) → ℝ) a < u
hf₂ : ∀ b ∈ V, u < (f : (a : E) → ℝ) b
x : E
hx₁ : x ∈ s
hx₂ : IsMaxOn (β := ℝ) (⇑f : (a : E) → ℝ) s x
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ) (v : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ u < v ∧ ∀ b ∈ t, v < (f : (a : E) → ℝ) b
have this : (f : (a : E) → ℝ) x < u
Tactic: have : f x < u := hf₁ x (sU hx₁)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (hypothesis)
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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : StrongDual ℝ E
u : ℝ
hf₁ : ∀ a ∈ U, (f : (a : E) → ℝ) a < u
hf₂ : ∀ b ∈ V, u < (f : (a : E) → ℝ) b
x : E
hx₁ : x ∈ s
hx₂ : IsMaxOn (β := ℝ) (⇑f : (a : E) → ℝ) s x
this : (f : (a : E) → ℝ) x < u
a : E
ha : a ∈ s
⊢ (f : (a : E) → ℝ) a < HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2
have this₁ : Membership.mem (γ := Set E)
  {x_1 : E | (fun (x_2 : E) ↦ LE.le (α := ℝ) ((f : (a : E) → ℝ) x_2 : ℝ) ((f : (a : E) → ℝ) x : ℝ)) x_1} a
Tactic: have := hx₂ ha
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
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
inst_5 : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : StrongDual ℝ E
u : ℝ
hf₁ : ∀ a ∈ U, (f : (a : E) → ℝ) a < u
hf₂ : ∀ b ∈ V, u < (f : (a : E) → ℝ) b
x : E
hx₁ : x ∈ s
hx₂ : IsMaxOn (β := ℝ) (⇑f : (a : E) → ℝ) s x
this_1 : (f : (a : E) → ℝ) x < u
a : E
ha : a ∈ s
this : LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) x : ℝ)
⊢ (f : (a : E) → ℝ) a < HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2
have linarith : HAdd.hAdd (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) u / 2 ≤ (f : (a : E) → ℝ) a → 2 / 2 = 1
Tactic: linarith