awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
⊢ Eq (α := ContinuousAlgEquiv.{u_4, u_5, u_6} R (V →L[R] V) (W →L[R] W)) g.conjContinuousAlgEquiv
      f.conjContinuousAlgEquiv ↔
    ∃ (α : Rˣ), f = α • g
have simp_rw : (∃ (y : R), HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)) ↔
  ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
Tactic: simp_rw [ContinuousAlgEquiv.ext_iff, funext_iff, conjContinuousAlgEquiv_apply,
    ← eq_toContinuousLinearMap_symm_comp, ← ContinuousLinearMap.comp_assoc,
    eq_comp_toContinuousLinearMap_symm, ContinuousLinearMap.comp_assoc,
    ← ContinuousLinearMap.comp_assoc _ f.toContinuousLinearMap, comp_coe, ← mul_def,
    ← Subalgebra.mem_center_iff (R := R), Algebra.IsCentral.center_eq_bot, ← comp_coe,
    Algebra.mem_bot, Set.mem_range, Algebra.algebraMap_eq_smul_one, ContinuousLinearEquiv.ext_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
h_1 : ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
y : Rˣ
h : Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(y • g) : (a : V) → W)
⊢ HSMul.hSMul (β := V →L[R] V) (↑y : R) 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
have h₁ : ∀ (x : V),
  Eq (α := V) ((HSMul.hSMul (β := V →L[R] V) (↑y : R) 1 : (a : V) → V) x : V)
    (((↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W) : (a : V) → V) x : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
⊢ (∃ (y : R), HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)) ↔
    ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
have refine : (∃ (y : R), HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)) →
  ∀ (y : R) (h : HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)),
    ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
Tactic: refine ⟨fun ⟨y, h⟩ ↦ ?_, fun ⟨y, h⟩ ↦ ⟨(y : R), by ext; simp [h]⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
h_1 : ∃ (y : R), HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
y : R
h : HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
⊢ ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
have if : ∀ (hy : y = 0), ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
Tactic: if hy : y = 0 then exact ⟨1, funext fun x ↦ by simp [by simpa [hy] using congr($h x).symm]⟩
  else exact ⟨.mk0 y hy, funext fun x ↦ by simp [by simpa [eq_symm_apply] using congr($h x)]⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
h_1 : ∃ (y : R), HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
y : R
h : HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
if : ∀ (hy : y = 0), ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
⊢ ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
have if₁ : ∀ (hy : ¬y = 0), ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
Tactic: if hy : y = 0 then exact ⟨1, funext fun x ↦ by simp [by simpa [hy] using congr($h x).symm]⟩
  else exact ⟨.mk0 y hy, funext fun x ↦ by simp [by simpa [eq_symm_apply] using congr($h x)]⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ ∃ (A : V ≃L[R] V), (A : (a : V) → V) x = y
have obtain : ∀ (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), (A : (a : V) → V) x = y
Tactic: obtain ⟨G, Gx, Gy⟩ : ∃ G : StrongDual R V, G x = 1 ∧ G y ≠ 0 :=
    exists_eq_one_ne_zero_of_ne_zero_pair hx hy
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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 b : V
⊢ a + b + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) (a + b) : R) (y - x) =
    a + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) a : R) (y - x) +
      (b + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) b : R) (y - x))
have simp : a + b +
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) a : R) (y - x) +
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) b : R) (y - x)) =
  a + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) a : R) (y - x) +
    (b + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) b : R) (y - x))
Tactic: simp [add_smul]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ (fun (z : V) ↦ z + HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • (x - y))
      ((fun (z : V) ↦ z + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) (y - x)) z) =
    z
have simp : z + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) (y - x) +
    HMul.hMul (α := R) (((G : (a : V) → R) y)⁻¹ : R)
        (HMul.hMul (α := R) (β := R) ((G : (a : V) → R) z : R) ((G : (a : V) → R) y : R)) •
      (x - y) =
  z
Tactic: simp only [RingHom.id_apply, smul_eq_mul,
        -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `map_smulₛₗ` into `map_smulₛₗ _`
        map_add, map_smulₛₗ _, map_sub, Gx, mul_sub, mul_one, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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 + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) (y - x) +
      HMul.hMul (α := R) (((G : (a : V) → R) y)⁻¹ : R)
          (HMul.hMul (α := R) (β := R) ((G : (a : V) → R) z : R) ((G : (a : V) → R) y : R)) •
        (x - y) =
    z
have rw : z + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) (y - x) +
    HMul.hMul (α := R) (β := R) (1 : R) ((G : (a : V) → R) z : R) • (x - y) =
  z
Tactic: rw [mul_comm (G z), ← mul_assoc, inv_mul_cancel₀ Gy]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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 + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) (y - x) +
      HMul.hMul (α := R) (β := R) (1 : R) ((G : (a : V) → R) z : R) • (x - y) =
    z
have simp : z +
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) y -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) x) +
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) x -
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) y) =
  z
Tactic: simp only [smul_sub, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ (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
have 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
Tactic: simp only [map_add, map_smulₛₗ _, map_mul, map_inv₀, RingHom.id_apply, map_sub, Gx,
        smul_eq_mul, mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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 - 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
have 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
Tactic: rw [mul_comm _ (G y), ← mul_assoc, mul_inv_cancel₀ Gy]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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 - 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
have 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
Tactic: simp only [smul_sub, one_mul, add_sub_cancel]
-- 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 ⋯
⊢ ∃ (f : StrongDual ℝ E),
    Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ) ∧ ∀ x ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
have 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 : ℝ)
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₀) ?_
-- 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 ⋯
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 : ℝ)
⊢ ∃ (f : StrongDual ℝ E),
    Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ) ∧ ∀ x ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
have refine_1 : ∀ (x : ↥f.domain), (↑f : ↥f.domain → ℝ) x ≤ gauge s (↑x : E)
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₀) ?_
-- 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 ⋯
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 : ℝ)
have 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 : ℝ)
Tactic: obtain ⟨φ, hφ₁, hφ₂⟩ := 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 : 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 : ℝ)
have rw : Eq (α := ℝ) ((φ : (a : E) → ℝ) (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x₀ sorry) : E) : ℝ) (1 : ℝ)
Tactic: rw [← f.domain.coe_mk x₀ (Submodule.mem_span_singleton_self _), hφ₁,
        LinearPMap.mkSpanSingleton'_apply_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 : 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 : ℝ)
⊢ Eq (α := ℝ) ((φ : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
have rw₁ : (↑f : ↥f.domain → ℝ) (Subtype.mk (p := fun (x : E) ↦ x ∈ f.domain) x₀ sorry) = 1
Tactic: rw [← f.domain.coe_mk x₀ (Submodule.mem_span_singleton_self _), hφ₁,
        LinearPMap.mkSpanSingleton'_apply_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 : 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
⊢ Eq (α := ℝ) ((φ : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ)
have rw₂ : Eq (α := ℝ) 1 1
Tactic: rw [← f.domain.coe_mk x₀ (Submodule.mem_span_singleton_self _), hφ₁,
        LinearPMap.mkSpanSingleton'_apply_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 : 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
⊢ ∃ (f : StrongDual ℝ E),
    Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ) ∧ ∀ x ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
have hφ₃ : 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]
-- 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 : ℝ)
⊢ ∃ (f : StrongDual ℝ E),
    Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ) ∧ ∀ x ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
have hφ₄ : ∀ 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)
-- 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 : ℝ)
⊢ ∃ (f : StrongDual ℝ E),
    Eq (α := ℝ) ((f : (a : E) → ℝ) x₀ : ℝ) (1 : ℝ) ∧ ∀ x ∈ s, LT.lt (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (1 : ℝ)
have refine_2 : Continuous φ.toFun
Tactic: refine ⟨⟨φ, ?_⟩, hφ₃, 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 : ℝ)
hφ₄ : ∀ x ∈ s, LT.lt (α := ℝ) ((φ : (a : E) → ℝ) x : ℝ) (1 : ℝ)
⊢ Continuous φ.toFun
have refine_2 : ∀ (x : E) (hx : x ∈ s),
  Membership.mem (γ := Set E) (fun (x : E) ↦ Eq (α := ℝ) ((φ : (a : E) → ℝ) x : ℝ) (0 : ℝ) → False) (-x₀ +ᵥ x)
Tactic: refine
      φ.continuous_of_nonzero_on_open _ (hs₂.vadd (-x₀)) (Nonempty.vadd_set ⟨0, hs₀⟩)
        (vadd_set_subset_iff.mpr fun x hx => ?_)