awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_1
V : Type u_2
inst : Field R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalRing R
inst_5 : Module R V
inst_6 : SeparatingDual R V
inst_7 : IsTopologicalAddGroup V
inst_8 : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R)
Gy : Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)
z : V
simp :
  z + HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • (x - y) +
      HAdd.hAdd (α := R) ((G : (a : V) → R) z : R)
          (HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) -
            HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R))
              ((G : (a : V) → R) y : R)) •
        (y - x) =
    z
⊢ (fun (z : V) ↦ z + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) (y - x))
      ((fun (z : V) ↦ z + HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • (x - y))
        z) =
    z

Tactic:
simp only [map_add, map_smulₛₗ _, map_mul, map_inv₀, RingHom.id_apply, map_sub, Gx,
        smul_eq_mul, mul_sub, mul_one]

Premises used: map_sub, RingHom.id_apply, mul_sub, map_inv₀, map_add, MulActionSemiHomClass.map_smulₛₗ, map_mul, smul_eq_mul, mul_one
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_1
V : Type u_2
inst : Field R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalRing R
inst_5 : Module R V
inst_6 : SeparatingDual R V
inst_7 : IsTopologicalAddGroup V
inst_8 : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R)
Gy : Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)
z : V
rw :
  z + HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • (x - y) +
      HAdd.hAdd (α := R) ((G : (a : V) → R) z : R)
          (HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) -
            HMul.hMul (α := R) (β := R) (1 : R) ((G : (a : V) → R) z : R)) •
        (y - x) =
    z
⊢ z + HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • (x - y) +
      HAdd.hAdd (α := R) ((G : (a : V) → R) z : R)
          (HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) -
            HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R))
              ((G : (a : V) → R) y : R)) •
        (y - x) =
    z

Tactic:
rw [mul_comm _ (G y), ← mul_assoc, mul_inv_cancel₀ Gy]

Premises used: mul_inv_cancel₀, mul_assoc, mul_comm, DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_1
V : Type u_2
inst : Field R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalRing R
inst_5 : Module R V
inst_6 : SeparatingDual R V
inst_7 : IsTopologicalAddGroup V
inst_8 : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R)
Gy : Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)
z : V
simp :
  z +
        (HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • x -
          HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • y) +
      (HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • y -
        HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • x) =
    z
⊢ z + HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • (x - y) +
      HAdd.hAdd (α := R) ((G : (a : V) → R) z : R)
          (HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) -
            HMul.hMul (α := R) (β := R) (1 : R) ((G : (a : V) → R) z : R)) •
        (y - x) =
    z

Tactic:
simp only [smul_sub, one_mul, add_sub_cancel]

Premises used: smul_sub, add_sub_cancel, one_mul
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_1
V : Type u_2
inst : Field R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalRing R
inst_5 : Module R V
inst_6 : SeparatingDual R V
inst_7 : IsTopologicalAddGroup V
inst_8 : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R)
Gy : Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)
z : V
⊢ z +
        (HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • x -
          HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • y) +
      (HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • y -
        HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • x) =
    z

Tactic:
abel
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_1
V : Type u_2
inst : Field R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalRing R
inst_5 : Module R V
inst_6 : SeparatingDual R V
inst_7 : IsTopologicalAddGroup V
inst_8 : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R)
Gy : Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)
A : V ≃L[R] V :=
  { toFun := fun (z : V) ↦ z + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) (y - x), map_add' := ⋯,
    map_smul' := ⋯,
    invFun := fun (z : V) ↦
      z + HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • (x - y),
    left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ x + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) x : R) (y - x) = y

Tactic:
simp [Gx]
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_1
V : Type u_2
inst : Field R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalRing R
inst_5 : Module R V
inst_6 : SeparatingDual R V
inst_7 : IsTopologicalAddGroup V
inst_8 : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R)
Gy : Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)
A : V ≃L[R] V :=
  { toFun := fun (z : V) ↦ z + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) (y - x), map_add' := ⋯,
    map_smul' := ⋯,
    invFun := fun (z : V) ↦
      z + HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • (x - y),
    left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ ∃ (A : V ≃L[R] V), (A : (a : V) → V) x = y

Tactic:
exact ⟨A, show x + G x • (y - x) = y by simp [Gx]⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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 ⋯
refine_2 :
  ∀
    (this :
      ∃ (g : E →ₗ[ℝ] ℝ),
        (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧
          ∀ (x : E), (g : (a : E) → ℝ) x ≤ gauge s x),
    ∃ (f : StrongDual ℝ E),
      Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ) ∧ ∀ x ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
refine_1 : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ gauge s (↑x : E)
⊢ ∃ (f : StrongDual ℝ E),
    Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ) ∧ ∀ x ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
have := exists_extension_of_le_sublinear f (gauge s) (fun c hc => gauge_smul_of_nonneg hc.le)
    (gauge_add_le hs₁ <| absorbent_nhds_zero <| hs₂.mem_nhds hs₀) ?_
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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 ⋯
this :
  ∃ (g : E →ₗ[ℝ] ℝ),
    (∀ (x : ↥f.domain), (g : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x) ∧
      ∀ (x : E), (g : (a : E) → ℝ) x ≤ gauge s x
refine_2 :
  ∀ (φ : E →ₗ[ℝ] ℝ) (hφ₁ : ∀ (x : ↥f.domain), (φ : (a : E) → ℝ) (↑x : E) = (↑f : ↥f.domain → ℝ) x)
    (hφ₂ : ∀ (x : E), (φ : (a : E) → ℝ) x ≤ gauge s x),
    ∃ (f : StrongDual ℝ E),
      Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ) ∧ ∀ x ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
⊢ ∃ (f : StrongDual ℝ E),
    Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ) ∧ ∀ x ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
obtain ⟨φ, hφ₁, hφ₂⟩ := this
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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
rw : Eq (α := ℝ) ((φ : (a : E) → ℝ) (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x₀ ⋯) : E) : ℝ) (1 : ℝ)
rw₁ : (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x₀ ⋯) = 1
rw₂ rw₃ : Eq (α := ℝ) 1 1
⊢ Eq (α := ℝ) ((φ : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)

Tactic:
rw [← f.domain.coe_mk x₀ (Submodule.mem_span_singleton_self _), hφ₁,
        LinearPMap.mkSpanSingleton'_apply_self]

Premises used: Submodule.coe_mk, LinearPMap.mkSpanSingleton'_apply_self, Submodule.mem_span_singleton_self
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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
⊢ Eq (α := ℝ) ((φ : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)

Tactic:
have hφ₃ : φ x₀ = 1 := by
      rw [← f.domain.coe_mk x₀ (Submodule.mem_span_singleton_self _), hφ₁,
        LinearPMap.mkSpanSingleton'_apply_self]
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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 ∈ s, LT.lt (α := ℝ) ((φ : (a : E) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
have hφ₄ : ∀ x ∈ s, φ x < 1 := fun x hx =>
      (hφ₂ x).trans_lt (gauge_lt_one_of_mem_of_isOpen hs₂ hx)
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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 : ℝ)
⊢ ∃ (f : StrongDual ℝ E),
    Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ) ∧ ∀ x ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
⟨⟨φ, ?_⟩, hφ₃, hφ₄⟩

Premises used: ContinuousLinearMap.mk, And.intro, Exists.intro
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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 : ℝ)
refine_2 : Continuous φ.toFun
⊢ ∃ (f : StrongDual ℝ E),
    Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ) ∧ ∀ x ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
refine ⟨⟨φ, ?_⟩, hφ₃, hφ₄⟩
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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 : ℝ)
⊢ Continuous φ.toFun

Tactic:
φ.continuous_of_nonzero_on_open _ (hs₂.vadd (-x₀)) (Nonempty.vadd_set ⟨0, hs₀⟩)
        (vadd_set_subset_iff.mpr fun x hx => ?_)

Premises used: Iff.mpr, Set.vadd_set_subset_iff, LinearMap.continuous_of_nonzero_on_open, Exists.intro, Set.Nonempty.vadd_set, OfNat.ofNat, IsOpen.vadd, Neg.neg
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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 : ℝ)
refine_2 :
  ∀ (x : E) (hx : x ∈ s),
    Membership.mem (γ := Set E) (fun (x : E) ↦ Eq (α := ℝ) ((φ : (a : E) → ℝ) x : ℝ) (0 : ℝ) → False) (-x₀ +ᵥ x)
⊢ Continuous φ.toFun

Tactic:
refine
      φ.continuous_of_nonzero_on_open _ (hs₂.vadd (-x₀)) (Nonempty.vadd_set ⟨0, hs₀⟩)
        (vadd_set_subset_iff.mpr fun x hx => ?_)

Premises used: Iff.mpr, Set.vadd_set_subset_iff, LinearMap.continuous_of_nonzero_on_open, Exists.intro, Set.Nonempty.vadd_set, OfNat.ofNat, IsOpen.vadd, Neg.neg
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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
refine_2 : Ne (α := ℝ) ((φ : (a : E) → ℝ) (-x₀ + x) : ℝ) (0 : ℝ)
⊢ Membership.mem (γ := Set E) (fun (x : E) ↦ Eq (α := ℝ) ((φ : (a : E) → ℝ) x : ℝ) (0 : ℝ) → False) (-x₀ +ᵥ x)

Tactic:
change φ (-x₀ + x) ≠ 0

Premises used: HAdd.hAdd, DFunLike.coe, Neg.neg
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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
refine_2 : HAdd.hAdd (α := ℝ) (β := ℝ) (-(φ : (a : E) → ℝ) x₀ : ℝ) ((φ : (a : E) → ℝ) x : ℝ) ≠ 0
⊢ Ne (α := ℝ) ((φ : (a : E) → ℝ) (-x₀ + x) : ℝ) (0 : ℝ)

Tactic:
rw [map_add, map_neg]

Premises used: map_add, map_neg
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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
⊢ LT.lt (α := ℝ) ((φ : (a : E) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
specialize hφ₄ x hx
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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 : ℝ)
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
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) (-(φ : (a : E) → ℝ) x₀ : ℝ) ((φ : (a : E) → ℝ) x : ℝ) ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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
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)
⊢ (↑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)

Tactic:
obtain ⟨y, rfl⟩ := Submodule.mem_span_singleton.1 hx

Premises used: Submodule.mem_span_singleton, Iff.mp, rfl
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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 :
  HSMul.hSMul (α := ℝ) (β := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) y : ℝ) 1 ≤
    gauge s (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (y • x₀) hx) : E)
⊢ (↑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:
rw [LinearPMap.mkSpanSingleton'_apply]

Premises used: LinearPMap.mkSpanSingleton'_apply
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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 : (RingHom.id ℝ : (a : ℝ) → ℝ) y ≤ gauge s (y • x₀)
⊢ HSMul.hSMul (α := ℝ) (β := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) y : ℝ) 1 ≤
    gauge s (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) (y • x₀) hx) : E)

Tactic:
simp only [mul_one, smul_eq_mul]

Premises used: smul_eq_mul, mul_one
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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₀)
refine_1₁ : ∀ (h : 0 < y), (RingHom.id ℝ : (a : ℝ) → ℝ) y ≤ gauge s (y • x₀)
⊢ (RingHom.id ℝ : (a : ℝ) → ℝ) y ≤ gauge s (y • x₀)

Tactic:
obtain h | h := le_or_gt y 0

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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 : y ≤ 0
⊢ (RingHom.id ℝ : (a : ℝ) → ℝ) y ≤ gauge s (y • x₀)

Tactic:
h.trans (gauge_nonneg _)

Premises used: gauge_nonneg, LE.le.trans
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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 : y ≤ 0
⊢ (RingHom.id ℝ : (a : ℝ) → ℝ) y ≤ gauge s (y • x₀)

Tactic:
exact h.trans (gauge_nonneg _)

Premises used: gauge_nonneg, LE.le.trans
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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
refine_1 : 1 ≤ gauge s x₀
⊢ (RingHom.id ℝ : (a : ℝ) → ℝ) y ≤ gauge s (y • x₀)

Tactic:
rw [gauge_smul_of_nonneg h.le, smul_eq_mul, RingHom.id_apply, le_mul_iff_one_le_right h]

Premises used: gauge_smul_of_nonneg, RingHom.id_apply, le_mul_iff_one_le_right, LT.lt.le, smul_eq_mul
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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
⊢ 1 ≤ gauge s x₀

Tactic:
one_le_gauge_of_notMem (hs₁.starConvex hs₀)
        (absorbent_nhds_zero <| hs₂.mem_nhds hs₀).absorbs hx₀

Premises used: Absorbent.absorbs, absorbent_nhds_zero, one_le_gauge_of_notMem, IsOpen.mem_nhds, Convex.starConvex
-- Module: Mathlib.Analysis.LocallyConvex.Separation
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
⊢ 1 ≤ gauge s x₀

Tactic:
exact
      one_le_gauge_of_notMem (hs₁.starConvex hs₀)
        (absorbent_nhds_zero <| hs₂.mem_nhds hs₀).absorbs hx₀

Premises used: Absorbent.absorbs, absorbent_nhds_zero, one_le_gauge_of_notMem, IsOpen.mem_nhds, Convex.starConvex