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 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : ↥f.domain), (φ : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x
hφ₂ : ∀ (x : E), (φ : (a : E) → ℝ) x ≤ gauge s x
hφ₃ : Eq (α := ℝ) ((φ : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hφ₄ : ∀ x ∈ s, LT.lt (α := ℝ) ((φ : (a : E) → ℝ) x : ℝ) (1 : ℝ)
x : E
hx : x ∈ s
⊢ Membership.mem (γ := Set E) (fun (x : E) ↦ Eq (α := ℝ) ((φ : (a : E) → ℝ) x : ℝ) (0 : ℝ) → False) (-x₀ +ᵥ x)
have refine_2 : Ne (α := ℝ) ((φ : (a : E) → ℝ) (-x₀ + x) : ℝ) (0 : ℝ)
Tactic: change φ (-x₀ + x) ≠ 0
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : ↥f.domain), (φ : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x
hφ₂ : ∀ (x : E), (φ : (a : E) → ℝ) x ≤ gauge s x
hφ₃ : Eq (α := ℝ) ((φ : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hφ₄ : ∀ x ∈ s, LT.lt (α := ℝ) ((φ : (a : E) → ℝ) x : ℝ) (1 : ℝ)
x : E
hx : x ∈ s
⊢ Ne (α := ℝ) ((φ : (a : E) → ℝ) (-x₀ + x) : ℝ) (0 : ℝ)
have refine_2 : HAdd.hAdd (α := ℝ) (β := ℝ) (-(φ : (a : E) → ℝ) x₀ : ℝ) ((φ : (a : E) → ℝ) x : ℝ) ≠ 0
Tactic: rw [map_add, map_neg]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (hypothesis)
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : ↥f.domain), (φ : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x
hφ₂ : ∀ (x : E), (φ : (a : E) → ℝ) x ≤ gauge s x
hφ₃ : Eq (α := ℝ) ((φ : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
hφ₄ : ∀ x ∈ s, LT.lt (α := ℝ) ((φ : (a : E) → ℝ) x : ℝ) (1 : ℝ)
x : E
hx : x ∈ s
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) (-(φ : (a : E) → ℝ) x₀ : ℝ) ((φ : (a : E) → ℝ) x : ℝ) ≠ 0
have hφ₅ : LT.lt (α := ℝ) ((φ : (a : E) → ℝ) x : ℝ) (1 : ℝ)
Tactic: specialize hφ₄ x hx
Cleared hypotheses: hφ₄
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : ↥f.domain), (φ : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x
hφ₂ : ∀ (x : E), (φ : (a : E) → ℝ) x ≤ gauge s x
hφ₃ : Eq (α := ℝ) ((φ : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
x : E
hx : x ∈ s
hφ₄ : LT.lt (α := ℝ) ((φ : (a : E) → ℝ) x : ℝ) (1 : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) (-(φ : (a : E) → ℝ) x₀ : ℝ) ((φ : (a : E) → ℝ) x : ℝ) ≠ 0
have linarith : HAdd.hAdd (α := ℝ) (β := ℝ) (-(φ : (a : E) → ℝ) x₀ : ℝ) ((φ : (a : E) → ℝ) x : ℝ) = 0 →
  -HSub.hSub (α := ℝ) (β := ℝ) ((φ : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ) +
        HSub.hSub (α := ℝ) (β := ℝ) ((φ : (a : E) → ℝ) x : ℝ) (1 : ℝ) +
      -(HAdd.hAdd (α := ℝ) (β := ℝ) (-(φ : (a : E) → ℝ) x₀ : ℝ) ((φ : (a : E) → ℝ) x : ℝ) - 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 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
x : E
hx : x ∈ f.domain
⊢ (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) ≤
    gauge s (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x hx) : E)
have refine_1 : ∀ (y : ℝ) (hx : y • x₀ ∈ f.domain),
  (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (y • x₀) hx) ≤
    gauge s (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (y • x₀) hx) : E)
Tactic: obtain ⟨y, rfl⟩ := Submodule.mem_span_singleton.1 hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
y : ℝ
hx : y • x₀ ∈ f.domain
⊢ (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (y • x₀) hx) ≤
    gauge s (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (y • x₀) hx) : E)
have refine_1 : HSMul.hSMul (α := ℝ) (β := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) y : ℝ) 1 ≤
  gauge s (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (y • x₀) hx) : E)
Tactic: rw [LinearPMap.mkSpanSingleton'_apply]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
y : ℝ
hx : y • x₀ ∈ f.domain
⊢ HSMul.hSMul (α := ℝ) (β := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) y : ℝ) 1 ≤
    gauge s (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (y • x₀) hx) : E)
have refine_1 : (RingHom.id ℝ : (a : ℝ) → ℝ) y ≤ gauge s (y • x₀)
Tactic: simp only [mul_one, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
y : ℝ
hx : y • x₀ ∈ f.domain
⊢ (RingHom.id ℝ : (a : ℝ) → ℝ) y ≤ gauge s (y • x₀)
have refine_1 : ∀ (h : y ≤ 0), (RingHom.id ℝ : (a : ℝ) → ℝ) y ≤ gauge s (y • x₀)
Tactic: obtain h | h := le_or_gt y 0
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
y : ℝ
hx : y • x₀ ∈ f.domain
refine_1 : ∀ (h : y ≤ 0), (RingHom.id ℝ : (a : ℝ) → ℝ) y ≤ gauge s (y • x₀)
⊢ (RingHom.id ℝ : (a : ℝ) → ℝ) y ≤ gauge s (y • x₀)
have refine_1₁ : ∀ (h : 0 < y), (RingHom.id ℝ : (a : ℝ) → ℝ) y ≤ gauge s (y • x₀)
Tactic: obtain h | h := le_or_gt y 0
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Separation (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
y : ℝ
hx : y • x₀ ∈ f.domain
h : 0 < y
⊢ (RingHom.id ℝ : (a : ℝ) → ℝ) y ≤ gauge s (y • x₀)
have refine_1 : 1 ≤ gauge s x₀
Tactic: rw [gauge_smul_of_nonneg h.le, smul_eq_mul, RingHom.id_apply, le_mul_iff_one_le_right h]
-- 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
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
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
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) ∅) (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, 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
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
⊢ ∃ (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
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
⊢ Eq.{u_2 + 1} (α := E) ((fun (x : E) ↦ x₀ +ᵥ x) (a₀ - b₀)) 0
have simp_rw₃ : b₀ - a₀ + (a₀ - b₀) = 0
Tactic: simp_rw [x₀, vadd_eq_add, sub_add_sub_cancel', sub_self]
-- 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
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
⊢ Eq.{u_2 + 1} (α := E) ((fun (x : E) ↦ x₀ +ᵥ x) (a₀ - b₀)) 0
have simp_rw₄ : a₀ - a₀ = 0
Tactic: simp_rw [x₀, vadd_eq_add, sub_add_sub_cancel', sub_self]
-- 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
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
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
have this : 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]⟩
-- 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
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
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
have this₁ : Convex ℝ C
Tactic: have : Convex ℝ C := (hs₁.sub ht).vadd _
-- 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
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
⊢ False
have hx₁ : x₀ + 0 ∈ C
Tactic: rw [← add_zero x₀] at hx₀
Cleared hypotheses: 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
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
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
have this₁ : 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₀)
-- 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
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) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
have 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
Tactic: obtain ⟨f, hf₁, hf₂⟩ := separate_convex_open_set ‹0 ∈ C› ‹_› (hs₂.sub_right.vadd _) ‹x₀ ∉ C›
-- 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
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
⊢ LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ)
have this₁ : LT.lt (α := ℝ) ((f : (a : E) → ℝ) (x₀ + (a - b)) : ℝ) (1 : ℝ)
Tactic: have := hf₂ (x₀ + (a - b)) (vadd_mem_vadd_set <| sub_mem_sub ha hb)
-- 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
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 : ℝ)
⊢ LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ)
have this₁ : 1 + HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ) < 1
Tactic: simp only [f.map_add, f.map_sub, hf₁] at this
Cleared hypotheses: this
-- 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
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
⊢ LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) b : ℝ)
have 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
Tactic: linarith
-- 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
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 : ℝ)
⊢ ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, (f : (a : E) → ℝ) a < u) ∧ ∀ b ∈ t, u ≤ (f : (a : E) → ℝ) b
have forall_le : ∀ 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
-- 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
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
have inr : Subset (α := Set ℝ) ((⇑f : (a : E) → ℝ) '' s) (Iio (sInf ((⇑f : (a : E) → ℝ) '' t)))
Tactic: refine ⟨f, sInf (f '' t), image_subset_iff.1 (?_ : f '' s ⊆ Iio (sInf (f '' t))), fun 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
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)))
⊢ ∃ (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), LE.le (α := ℝ) (sInf ((⇑f : (a : E) → ℝ) '' t) : ℝ) ((f : (a : E) → ℝ) b : ℝ)
Tactic: refine ⟨f, sInf (f '' t), image_subset_iff.1 (?_ : f '' s ⊆ Iio (sInf (f '' t))), fun 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
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) (Iio (sInf ((⇑f : (a : E) → ℝ) '' t)))
have inr : Subset (α := Set ℝ) ((⇑f : (a : E) → ℝ) '' s) (interior (Iic (sInf ((⇑f : (a : E) → ℝ) '' t))))
Tactic: rw [← interior_Iic]
-- 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
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))))
have inr : ∀ (a : E) (ha : a ∈ s),
  Membership.mem (γ := Set E) (preimage (β := ℝ) (⇑f : (a : E) → ℝ) (Iic (sInf ((⇑f : (a : E) → ℝ) '' t)))) a
Tactic: refine interior_maximal (image_subset_iff.2 fun a ha => ?_) (f.isOpenMap_of_ne_zero ?_ _ hs₂)
-- 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
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
⊢ Subset (α := Set ℝ) ((⇑f : (a : E) → ℝ) '' s) (interior (Iic (sInf ((⇑f : (a : E) → ℝ) '' t))))
have inr₁ : f ≠ 0
Tactic: refine interior_maximal (image_subset_iff.2 fun a ha => ?_) (f.isOpenMap_of_ne_zero ?_ _ hs₂)