awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w : Set K⟮X⟯
hT : Membership.mem (γ := Filter K⟮X⟯) (nhds 0) w
pre_T : (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w ⊆ S
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)} ⊆
    w
X : Set K⸨X⸩ :=
  {f : K⸨X⸩ |
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
        WithZero (Multiplicative ℤ))}
X_def :
  X =
    {f : K⸨X⸩ |
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
          WithZero (Multiplicative ℤ))
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
          WithZero (Multiplicative ℤ))}
⊢ Membership.mem (γ := Filter K⸨X⸩) (nhds 0) X
have h : ∃ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ),
  {y : K⸨X⸩ |
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) y :
          WithZero (Multiplicative ℤ))
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
          WithZero (Multiplicative ℤ))} ⊆
    X
Tactic: simp only [Valued.mem_nhds, sub_zero, Valuation.restrict_lt_iff_lt_embedding]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w : Set K⟮X⟯
hT : Membership.mem (γ := Filter K⟮X⟯) (nhds 0) w
pre_T : (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w ⊆ S
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)} ⊆
    w
X : Set K⸨X⸩ :=
  {f : K⸨X⸩ |
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
        WithZero (Multiplicative ℤ))}
X_def :
  X =
    {f : K⸨X⸩ |
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
          WithZero (Multiplicative ℤ))
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
          WithZero (Multiplicative ℤ))}
⊢ ∃ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ),
    {y : K⸨X⸩ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) y :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))} ⊆
      X
have h : ∀ (x : K⟮X⟯)
  (hx :
    ((restrict₀ Valued.v :
            K⟮X⟯ →*₀ MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) Valued.v) :
          (a : K⟮X⟯) → MonoidWithZeroHom.ValueGroup₀ Valued.v)
        x =
      (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)),
  ∃ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ),
    {y : K⸨X⸩ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) y :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))} ⊆
      X
Tactic: obtain ⟨x, hx⟩ := restrict₀_surjective _ d.1
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w : Set K⟮X⟯
hT : Membership.mem (γ := Filter K⟮X⟯) (nhds 0) w
pre_T : (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w ⊆ S
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)} ⊆
    w
X : Set K⸨X⸩ :=
  {f : K⸨X⸩ |
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
        WithZero (Multiplicative ℤ))}
X_def :
  X =
    {f : K⸨X⸩ |
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
          WithZero (Multiplicative ℤ))
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
          WithZero (Multiplicative ℤ))}
⊢ Set.preimage (β := K⸨X⸩ × K⸨X⸩)
      (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))
      ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' X) ⊆
    S
have h : ∀ (x : K⟮X⟯ × K⟮X⟯),
  Membership.mem (γ := Set (K⟮X⟯ × K⟮X⟯))
      (Set.preimage (β := K⸨X⸩ × K⸨X⸩)
        (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))
        ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' X))
      x →
    Membership.mem (γ := Set (K⟮X⟯ × K⟮X⟯)) ((fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w) x
Tactic: refine subset_trans (fun _ _ ↦ ?_) pre_T
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w : Set K⟮X⟯
hT : Membership.mem (γ := Filter K⟮X⟯) (nhds 0) w
pre_T : (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w ⊆ S
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)} ⊆
    w
X : Set K⸨X⸩ :=
  {f : K⸨X⸩ |
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
        WithZero (Multiplicative ℤ))}
X_def :
  X =
    {f : K⸨X⸩ |
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
          WithZero (Multiplicative ℤ))
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
          WithZero (Multiplicative ℤ))}
x : K⟮X⟯ × K⟮X⟯
h :
  Membership.mem (γ := Set (K⟮X⟯ × K⟮X⟯))
    (Set.preimage (β := K⸨X⸩ × K⸨X⸩)
      (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))
      ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' X))
    x
⊢ Membership.mem (γ := Set (K⟮X⟯ × K⟮X⟯)) ((fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w) x
have h : Membership.mem (γ := Set K⟮X⟯)
  {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)}
  ((fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) x)
Tactic: apply hd
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w : Set K⟮X⟯
hT : Membership.mem (γ := Filter K⟮X⟯) (nhds 0) w
pre_T : (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w ⊆ S
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)} ⊆
    w
X : Set K⸨X⸩ :=
  {f : K⸨X⸩ |
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
        WithZero (Multiplicative ℤ))}
X_def :
  X =
    {f : K⸨X⸩ |
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
          WithZero (Multiplicative ℤ))
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
          WithZero (Multiplicative ℤ))}
x : K⟮X⟯ × K⟮X⟯
h :
  Membership.mem (γ := Set (K⟮X⟯ × K⟮X⟯))
    (Set.preimage (β := K⸨X⸩ × K⸨X⸩)
      (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))
      ((fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' X))
    x
⊢ Membership.mem (γ := Set K⟮X⟯)
    {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)}
    ((fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) x)
have h : LT.lt (α := WithZero (Multiplicative ℤ))
  (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
        (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (HSub.hSub (α := K⸨X⸩) (β := K⸨X⸩) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2 : K⸨X⸩)
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1 : K⸨X⸩)) :
    WithZero (Multiplicative ℤ))
  ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
    WithZero (Multiplicative ℤ))
Tactic: rw [Set.mem_setOf_eq, sub_zero, Valuation.restrict_lt_iff_lt_embedding, v_def,
        valuation_eq_LaurentSeries_valuation, map_sub]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Field K
x y : RatFuncAdicCompl K
⊢ Equiv.toFun (UniformEquiv.toEquiv (comparePkg K)) (x * y) =
    Equiv.toFun (UniformEquiv.toEquiv (comparePkg K)) x * Equiv.toFun (UniformEquiv.toEquiv (comparePkg K)) y
have rw : HMul.hMul (α := K⸨X⸩) (β := K⸨X⸩)
    ((extensionAsRingHom K sorry : (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → K⸨X⸩) x : K⸨X⸩)
    ((extensionAsRingHom K sorry : (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → K⸨X⸩) y : K⸨X⸩) =
  HMul.hMul (α := K⸨X⸩) (β := K⸨X⸩) ((comparePkg K : (a : RatFuncAdicCompl K) → K⸨X⸩) x : K⸨X⸩)
    ((comparePkg K : (a : RatFuncAdicCompl K) → K⸨X⸩) y : K⸨X⸩)
Tactic: rw [Equiv.toFun_as_coe, UniformEquiv.coe_toEquiv, comparePkg_eq_extension,
        (extensionAsRingHom K (continuous_coe' _)).map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Field K
x y : RatFuncAdicCompl K
⊢ Equiv.toFun (UniformEquiv.toEquiv (comparePkg K)) (x + y) =
    Equiv.toFun (UniformEquiv.toEquiv (comparePkg K)) x + Equiv.toFun (UniformEquiv.toEquiv (comparePkg K)) y
have rw : HAdd.hAdd (α := K⸨X⸩) (β := K⸨X⸩)
    ((extensionAsRingHom K sorry : (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → K⸨X⸩) x : K⸨X⸩)
    ((extensionAsRingHom K sorry : (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → K⸨X⸩) y : K⸨X⸩) =
  HAdd.hAdd (α := K⸨X⸩) (β := K⸨X⸩) ((comparePkg K : (a : RatFuncAdicCompl K) → K⸨X⸩) x : K⸨X⸩)
    ((comparePkg K : (a : RatFuncAdicCompl K) → K⸨X⸩) y : K⸨X⸩)
Tactic: rw [Equiv.toFun_as_coe, UniformEquiv.coe_toEquiv, comparePkg_eq_extension,
        (extensionAsRingHom K (continuous_coe' _)).map_add]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
⊢ Eq (α := K⸨X⸩)
    ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩)
        (↑((RingEquiv.symm (WithVal.equiv (valuation (R := K[X]) K⟮X⟯ (idealX K))) :
                (a : K⟮X⟯) → WithVal (valuation K⟮X⟯ (idealX K)))
              RatFunc.X) :
          UniformSpace.Completion (WithVal (valuation K⟮X⟯ (idealX K)))) :
      K⸨X⸩)
    (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X : K⟦ℤ⟧)
have rw : Eq (α := K⸨X⸩)
  ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩)
      (↑((RingEquiv.symm (WithVal.equiv (valuation (R := K[X]) K⟮X⟯ (idealX K))) :
              (a : K⟮X⟯) → WithVal (valuation K⟮X⟯ (idealX K)))
            RatFunc.X) :
        UniformSpace.Completion (WithVal (valuation K⟮X⟯ (idealX K)))) :
    K⸨X⸩)
  (AbstractCompletion.compare ratfuncAdicComplPkg (LaurentSeriesPkg K)
      (AbstractCompletion.coe ratfuncAdicComplPkg (WithVal.toVal (polynomialValuationX K) RatFunc.X)) :
    space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) (LaurentSeriesPkg K))
Tactic: rw [PowerSeries.coe_X, ← RatFunc.coe_X, ← LaurentSeries_coe, ← compare_coe]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
rw :
  Eq (α := K⸨X⸩)
    ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩)
        (↑((RingEquiv.symm (WithVal.equiv (valuation (R := K[X]) K⟮X⟯ (idealX K))) :
                (a : K⟮X⟯) → WithVal (valuation K⟮X⟯ (idealX K)))
              RatFunc.X) :
          UniformSpace.Completion (WithVal (valuation K⟮X⟯ (idealX K)))) :
      K⸨X⸩)
    (AbstractCompletion.compare ratfuncAdicComplPkg (LaurentSeriesPkg K)
        (AbstractCompletion.coe ratfuncAdicComplPkg (WithVal.toVal (polynomialValuationX K) RatFunc.X)) :
      space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) (LaurentSeriesPkg K))
⊢ Eq (α := K⸨X⸩)
    ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩)
        (↑((RingEquiv.symm (WithVal.equiv (valuation (R := K[X]) K⟮X⟯ (idealX K))) :
                (a : K⟮X⟯) → WithVal (valuation K⟮X⟯ (idealX K)))
              RatFunc.X) :
          UniformSpace.Completion (WithVal (valuation K⟮X⟯ (idealX K)))) :
      K⸨X⸩)
    (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X : K⟦ℤ⟧)
have pkg : AbstractCompletion.{u_2, u_2} (WithVal (R := K⟮X⟯) (polynomialValuationX K))
Tactic: rw [PowerSeries.coe_X, ← RatFunc.coe_X, ← LaurentSeries_coe, ← compare_coe]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
⊢ Eq (α :=
    (b : space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) (LaurentSeriesPkg K)) → WithZero (Multiplicative ℤ))
    (IsDenseInducing.extend ⋯ (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ)))
    (⇑Valued.v : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
have hf : ∀ (x : WithVal (R := K⟮X⟯) (polynomialValuationX K)),
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (AbstractCompletion.coe (LaurentSeriesPkg K) x) :
      WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (WithVal (R := K⟮X⟯) (polynomialValuationX K)) (WithZero (Multiplicative ℤ))) :
          (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
Tactic: apply IsDenseInducing.extend_unique
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
hf :
  ∀ (x : WithVal (R := K⟮X⟯) (polynomialValuationX K)),
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
          (AbstractCompletion.coe (LaurentSeriesPkg K) x) :
        WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (WithVal (R := K⟮X⟯) (polynomialValuationX K)) (WithZero (Multiplicative ℤ))) :
            (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
          x :
        WithZero (Multiplicative ℤ))
⊢ Eq (α :=
    (b : space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) (LaurentSeriesPkg K)) → WithZero (Multiplicative ℤ))
    (IsDenseInducing.extend ⋯ (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ)))
    (⇑Valued.v : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
have hg : Continuous.{u_2, 0} (X := space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) (LaurentSeriesPkg K)) (Y :=
  WithZero (Multiplicative ℤ)) (⇑Valued.v : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
Tactic: apply IsDenseInducing.extend_unique
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
x : WithVal (R := K⟮X⟯) (polynomialValuationX K)
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (AbstractCompletion.coe (LaurentSeriesPkg K) x) :
      WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (WithVal (R := K⟮X⟯) (polynomialValuationX K)) (WithZero (Multiplicative ℤ))) :
          (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
        x :
      WithZero (Multiplicative ℤ))
have hf : Eq (α := WithZero (Multiplicative ℤ))
  (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (AbstractCompletion.coe (LaurentSeriesPkg K) x) :
    WithZero (Multiplicative ℤ))
  (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
        (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.ofVal) :
    WithZero (Multiplicative ℤ))
Tactic: rw [← WithVal.apply_ofVal, valuation_eq_LaurentSeries_valuation K]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
a : adicCompletion (R := K[X]) K⟮X⟯ (idealX K)
this :
  ∀ (s : Set (adicCompletion (R := K[X]) K⟮X⟯ (idealX K))),
    Membership.mem (γ := Filter (adicCompletion (R := K[X]) K⟮X⟯ (idealX K))) (𝓝 0) s ↔
      ∃ (γ :
        (MonoidWithZeroHom.ValueGroup₀ (F :=
            Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) Valued.v)ˣ),
        {x : adicCompletion (R := K[X]) K⟮X⟯ (idealX K) |
            ((Valuation.restrict Valued.v :
                    Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K))
                      (MonoidWithZeroHom.ValueGroup₀ (F :=
                        adicCompletion (R := K[X]) K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ))
                        (↑Valued.v : adicCompletion K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ)))) :
                  (a : adicCompletion K⟮X⟯ (idealX K)) →
                    MonoidWithZeroHom.ValueGroup₀
                      (↑Valued.v : adicCompletion K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ)))
                x <
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
          s
⊢ Tendsto (α := K⟮X⟯) (β := WithZero (Multiplicative ℤ))
    ((⇑Valued.v : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
    (Filter.comap
      (fun (x : K⟮X⟯) ↦
        (↑((RingEquiv.symm (WithVal.equiv (valuation (R := K[X]) K⟮X⟯ (idealX K))) :
                (a : K⟮X⟯) → WithVal (valuation K⟮X⟯ (idealX K)))
              x) :
          UniformSpace.Completion (WithVal (valuation K⟮X⟯ (idealX K)))))
      (𝓝 a))
    (𝓝
        (((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
          a) :
      Filter (WithZero (Multiplicative ℤ)))
have pos : ∀ (ha : a = 0),
  Tendsto (α := K⟮X⟯) (β := WithZero (Multiplicative ℤ))
    ((⇑Valued.v : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
    (Filter.comap
      (fun (x : K⟮X⟯) ↦
        (↑((RingEquiv.symm (WithVal.equiv (valuation (R := K[X]) K⟮X⟯ (idealX K))) :
                (a : K⟮X⟯) → WithVal (valuation K⟮X⟯ (idealX K)))
              x) :
          UniformSpace.Completion (WithVal (valuation K⟮X⟯ (idealX K)))))
      (𝓝 a))
    (𝓝
        (((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
          a) :
      Filter (WithZero (Multiplicative ℤ)))
Tactic: by_cases ha : a = 0