awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T
hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hγ :
  {x : K⸨X⸩ |
      ((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          x <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    T
this : WithZero (Multiplicative ℤ)
⊢ ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
have h : ∀ (P : K⟮X⟯)
  (hP :
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
          (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P : K⸨X⸩)) :
        WithZero (Multiplicative ℤ))
      ((↑((Units.map (↑embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* WithZero (Multiplicative ℤ)) :
                (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → (WithZero (Multiplicative ℤ))ˣ)
              γ) :
          WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))),
  ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
Tactic: obtain ⟨P, hP⟩ := exists_ratFunc_val_lt f
    (Units.map (embedding (f := (valued K).v)).toMonoidHom γ)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T
hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hγ :
  {x : K⸨X⸩ |
      ((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          x <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    T
this : WithZero (Multiplicative ℤ)
P : K⟮X⟯
hP :
  LT.lt (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P : K⸨X⸩)) :
      WithZero (Multiplicative ℤ))
    ((↑((Units.map (↑embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* WithZero (Multiplicative ℤ)) :
              (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → (WithZero (Multiplicative ℤ))ˣ)
            γ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
⊢ ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
have h : Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P : K⸨X⸩)
Tactic: use P
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T
hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hγ :
  {x : K⸨X⸩ |
      ((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          x <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    T
this : WithZero (Multiplicative ℤ)
P : K⟮X⟯
hP :
  LT.lt (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P : K⸨X⸩)) :
      WithZero (Multiplicative ℤ))
    ((↑((Units.map (↑embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* WithZero (Multiplicative ℤ)) :
              (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → (WithZero (Multiplicative ℤ))ˣ)
            γ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
⊢ Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P : K⸨X⸩)
have h : Membership.mem (α := K⸨X⸩ × K⸨X⸩) (γ := Set (K⸨X⸩ × K⸨X⸩)) ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T)
  ((f, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P) : K⸨X⸩ × K⸨X⸩)
Tactic: apply hT₁
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T
hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hγ :
  {x : K⸨X⸩ |
      ((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          x <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    T
this : WithZero (Multiplicative ℤ)
P : K⟮X⟯
hP :
  LT.lt (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P : K⸨X⸩)) :
      WithZero (Multiplicative ℤ))
    ((↑((Units.map (↑embedding : MonoidWithZeroHom.ValueGroup₀ Valued.v →* WithZero (Multiplicative ℤ)) :
              (a : (MonoidWithZeroHom.ValueGroup₀ Valued.v)ˣ) → (WithZero (Multiplicative ℤ))ˣ)
            γ) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
⊢ Membership.mem (α := K⸨X⸩ × K⸨X⸩) (γ := Set (K⸨X⸩ × K⸨X⸩)) ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T)
    ((f, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P) : K⸨X⸩ × K⸨X⸩)
have h : Membership.mem (γ := Set K⸨X⸩)
  {x : K⸨X⸩ |
    ((Valuation.restrict Valued.v :
            Valuation K⸨X⸩
              (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
          (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
        x <
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)}
  ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) (f, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P))
Tactic: apply hγ
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
x : K⸨X⸩
⊢ ∃ (f : K⟮X⟯),
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
have pos : ∀
  (hx :
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))),
  ∃ (f : K⟮X⟯),
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
Tactic: by_cases hx : Valued.v x = 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
x : K⸨X⸩
pos :
  ∀
    (hx :
      Eq (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
          WithZero (Multiplicative ℤ))
        (0 : WithZero (Multiplicative ℤ))),
    ∃ (f : K⟮X⟯),
      Eq (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) f :
          WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
          WithZero (Multiplicative ℤ))
⊢ ∃ (f : K⟮X⟯),
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
have neg : ∀
  (hx :
    ¬Eq (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
          WithZero (Multiplicative ℤ))
        (0 : WithZero (Multiplicative ℤ))),
  ∃ (f : K⟮X⟯),
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
Tactic: by_cases hx : Valued.v x = 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
x : K⸨X⸩
hx :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
⊢ ∃ (f : K⟮X⟯),
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
have h : Eq (α := WithZero (Multiplicative ℤ))
  (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) 0 :
    WithZero (Multiplicative ℤ))
  (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
    WithZero (Multiplicative ℤ))
Tactic: use 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
x : K⸨X⸩
hx :
  ¬Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
⊢ ∃ (f : K⟮X⟯),
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
have h : Eq (α := WithZero (Multiplicative ℤ))
  (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
      (HPow.hPow (α := K⟮X⟯) (β := ℤ) RatFunc.X
        (-log
            (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
              x))) :
    WithZero (Multiplicative ℤ))
  (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
    WithZero (Multiplicative ℤ))
Tactic: use RatFunc.X ^ (-log (Valued.v x))
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
x : K⸨X⸩
hx :
  ¬Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := K⟮X⟯) (β := ℤ) RatFunc.X
          (-log
              (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
                x))) :
      WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
have h : exp
    (-HSMul.hSMul (α := ℤ) (β := ℤ)
        (log (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x))
        (-1)) =
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x
Tactic: rw [zpow_neg, map_inv₀, map_zpow₀, v_def, valuation_X_eq_neg_one, ← exp_zsmul, ← exp_neg]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
⊢ IsUniformInducing.{u_2, u_2} (α := K⟮X⟯) (β := K⸨X⸩) (⇑(algebraMap K⟮X⟯ K⸨X⸩) : (a : K⟮X⟯) → K⸨X⸩)
have rw : Eq.{u_2 + 1} (α := Filter (K⟮X⟯ × K⟮X⟯))
  {
    sets :=
      {s : Set (K⟮X⟯ × K⟮X⟯) |
        ∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
          Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) t ∧
            (fun (x : K⟮X⟯ × K⟮X⟯) ↦
                  ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
                t ⊆
              s},
    univ_sets := sorry, sets_of_superset := sorry, inter_sets := sorry }
  (uniformity K⟮X⟯)
Tactic: rw [isUniformInducing_iff, Filter.comap]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
⊢ Eq.{u_2 + 1} (α := Filter (K⟮X⟯ × K⟮X⟯))
    {
      sets :=
        {s : Set (K⟮X⟯ × K⟮X⟯) |
          ∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
            Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) t ∧
              (fun (x : K⟮X⟯ × K⟮X⟯) ↦
                    ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1,
                      (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
                  t ⊆
                s},
      univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
    (uniformity K⟮X⟯)
have h : ∀ (S : Set (K⟮X⟯ × K⟮X⟯)),
  Membership.mem (γ := Filter (K⟮X⟯ × K⟮X⟯))
      {
        sets :=
          {s : Set (K⟮X⟯ × K⟮X⟯) |
            ∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
              Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) t ∧
                (fun (x : K⟮X⟯ × K⟮X⟯) ↦
                      ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1,
                        (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
                    t ⊆
                  s},
        univ_sets := sorry, sets_of_superset := sorry, inter_sets := sorry }
      S ↔
    Membership.mem (γ := Filter (K⟮X⟯ × K⟮X⟯)) (uniformity K⟮X⟯) S
Tactic: ext S
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
⊢ Membership.mem (γ := Filter (K⟮X⟯ × K⟮X⟯))
      {
        sets :=
          {s : Set (K⟮X⟯ × K⟮X⟯) |
            ∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
              Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) t ∧
                (fun (x : K⟮X⟯ × K⟮X⟯) ↦
                      ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1,
                        (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
                    t ⊆
                  s},
        univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
      S ↔
    Membership.mem (γ := Filter (K⟮X⟯ × K⟮X⟯)) (uniformity K⟮X⟯) S
have h : (∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
    (∃ (t_1 : Set K⸨X⸩),
        Membership.mem (γ := Filter K⸨X⸩) (nhds 0) t_1 ∧ (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
      (fun (x : K⟮X⟯ × K⟮X⟯) ↦
            ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
          t ⊆
        S) ↔
  ∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S
Tactic: simp only [Filter.mem_mk, Set.mem_setOf_eq, uniformity_eq_comap_nhds_zero,
    Filter.mem_comap]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
⊢ (∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
      (∃ (t_1 : Set K⸨X⸩),
          Membership.mem (γ := Filter K⸨X⸩) (nhds 0) t_1 ∧ (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
        (fun (x : K⟮X⟯ × K⟮X⟯) ↦
              ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
            t ⊆
          S) ↔
    ∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S
have h : (∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
    (∃ (t_1 : Set K⸨X⸩),
        Membership.mem (γ := Filter K⸨X⸩) (nhds 0) t_1 ∧ (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
      (fun (x : K⟮X⟯ × K⟮X⟯) ↦
            ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
          t ⊆
        S) →
  ∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
h :
  (∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
      (∃ (t_1 : Set K⸨X⸩),
          Membership.mem (γ := Filter K⸨X⸩) (nhds 0) t_1 ∧ (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
        (fun (x : K⟮X⟯ × K⟮X⟯) ↦
              ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
            t ⊆
          S) →
    ∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S
⊢ (∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
      (∃ (t_1 : Set K⸨X⸩),
          Membership.mem (γ := Filter K⸨X⸩) (nhds 0) t_1 ∧ (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
        (fun (x : K⟮X⟯ × K⟮X⟯) ↦
              ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
            t ⊆
          S) ↔
    ∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S
have h₁ : (∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S) →
  ∃ (t : Set (K⸨X⸩ × K⸨X⸩)),
    (∃ (t_1 : Set K⸨X⸩),
        Membership.mem (γ := Filter K⸨X⸩) (nhds 0) t_1 ∧ (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧
      (fun (x : K⟮X⟯ × K⟮X⟯) ↦
            ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
          t ⊆
        S
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T :
  (fun (x : K⟮X⟯ × K⟮X⟯) ↦
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
      T ⊆
    S
R : Set K⸨X⸩
hR : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) R
pre_R : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' R ⊆ T
⊢ ∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S
have h : ∀ (d : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ)
  (hd :
    {y : K⸨X⸩ |
        ((Valuation.restrict Valued.v :
                Valuation K⸨X⸩
                  (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                    (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
              (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
            (y - 0) <
          (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
      R),
  ∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S
Tactic: obtain ⟨d, hd⟩ := Valued.mem_nhds.mp hR
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T :
  (fun (x : K⟮X⟯ × K⟮X⟯) ↦
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
      T ⊆
    S
R : Set K⸨X⸩
hR : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) R
pre_R : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hd :
  {y : K⸨X⸩ |
      ((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (y - 0) <
        (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    R
⊢ ∃ (t : Set K⟮X⟯), Membership.mem (γ := Filter K⟮X⟯) (nhds 0) t ∧ (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' t ⊆ S
have h : Membership.mem (γ := Filter K⟮X⟯) (nhds 0)
    {P : K⟮X⟯ |
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) P :
          WithZero (Multiplicative ℤ))
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
          WithZero (Multiplicative ℤ))} ∧
  Set.preimage (β := K⟮X⟯) (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1)
      {P : K⟮X⟯ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) P :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))} ⊆
    S
Tactic: use {P : K⟮X⟯ | Valued.v P < embedding d.1}