awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
a_1 : 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
ha : a_1 = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
a : K⟮X⟯
h :
  Membership.mem (γ := Set K⟮X⟯)
    (Set.preimage (β := adicCompletion (R := K[X]) K⟮X⟯ (idealX K))
      (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)))))
      {t : adicCompletion (R := K[X]) K⟮X⟯ (idealX K) |
        ((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
            t <
          γ})
    a
⊢ ((Valued.v : Valuation (UniformSpace.Completion K⟮X⟯) (WithZero (Multiplicative ℤ))) :
        (a : UniformSpace.Completion K⟮X⟯) → WithZero (Multiplicative ℤ))
      (↑a : UniformSpace.Completion K⟮X⟯) <
    γ

Tactic:
simp_all
-- Module: Mathlib.RingTheory.LaurentSeries
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
ha : ¬a = 0
⊢ Ne (α :=
    MonoidWithZeroHom.ValueGroup₀ (F :=
      Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) Valued.v)
    (((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 ℤ)))
        a :
      MonoidWithZeroHom.ValueGroup₀ (F := adicCompletion (R := K[X]) K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : adicCompletion K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ)))
    (0 :
      MonoidWithZeroHom.ValueGroup₀ (F :=
        Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) Valued.v)

Tactic:
simp [Valuation.restrict_def, ha]

Premises used: Valuation.restrict_def
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (RatFuncAdicCompl K) (WithZero (Multiplicative ℤ))) :
          (a : RatFuncAdicCompl K) → WithZero (Multiplicative ℤ))
        (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg f) :
      WithZero (Multiplicative ℤ))
    (Function.comp (β := space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg)
        (IsDenseInducing.extend ⋯ (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ)))
        (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg) f :
      WithZero (Multiplicative ℤ))
cont_f :
  Continuous.{u_2, 0} (X := WithVal (R := K⟮X⟯) (polynomialValuationX K)) (Y := WithZero (Multiplicative ℤ))
    (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
a :
  ∀ (a : space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg),
    Tendsto (β := WithZero (Multiplicative ℤ))
      (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
      (Filter.comap (AbstractCompletion.coe ratfuncAdicComplPkg) (𝓝 a))
      (𝓝
        (IsDenseInducing.extend ⋯ (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ)) a))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (RatFuncAdicCompl K) (WithZero (Multiplicative ℤ))) :
          (a : RatFuncAdicCompl K) → WithZero (Multiplicative ℤ))
        (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg f) :
      WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
      WithZero (Multiplicative ℤ))

Tactic:
rw [← valuation_LaurentSeries_equal_extension, ← compare_comp_eq_compare ratfuncAdicComplPkg _]

Premises used: AbstractCompletion.compare_comp_eq_compare, LaurentSeries.valuation_LaurentSeries_equal_extension, LaurentSeries.ratfuncAdicComplPkg
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (RatFuncAdicCompl K) (WithZero (Multiplicative ℤ))) :
          (a : RatFuncAdicCompl K) → WithZero (Multiplicative ℤ))
        (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg f) :
      WithZero (Multiplicative ℤ))
    (Function.comp (β := space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg)
        (IsDenseInducing.extend ⋯ (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ)))
        (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg) f :
      WithZero (Multiplicative ℤ))

Tactic:
congr_fun (ratfuncAdicComplPkg.isDenseInducing.extend_unique
      Valued.valuedCompletion_apply (Valued.continuous_valuation_of_surjective
        (valuedAdicCompletion_surjective _ _))).symm _

Premises used: Classical.epsilon, Set.Mem, IsDenseInducing.extend_unique, setOf, Valued.valuedCompletion_apply, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, Filter.lim, congr_fun, Valued.continuous_valuation_of_surjective, Eq.symm, Filter.limUnder, IsDenseInducing.extend, AbstractCompletion.isDenseInducing, LaurentSeries.ratfuncAdicComplPkg
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (RatFuncAdicCompl K) (WithZero (Multiplicative ℤ))) :
          (a : RatFuncAdicCompl K) → WithZero (Multiplicative ℤ))
        (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg f) :
      WithZero (Multiplicative ℤ))
    (Function.comp (β := space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg)
        (IsDenseInducing.extend ⋯ (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ)))
        (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg) f :
      WithZero (Multiplicative ℤ))

Tactic:
exact congr_fun (ratfuncAdicComplPkg.isDenseInducing.extend_unique
      Valued.valuedCompletion_apply (Valued.continuous_valuation_of_surjective
        (valuedAdicCompletion_surjective _ _))).symm _

Premises used: IsDenseInducing.extend_unique, Valued.valuedCompletion_apply, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, congr_fun, Valued.continuous_valuation_of_surjective, Eq.symm, AbstractCompletion.isDenseInducing, LaurentSeries.ratfuncAdicComplPkg
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
⊢ Continuous.{u_2, 0} (X := WithVal (R := K⟮X⟯) (polynomialValuationX K)) (Y := WithZero (Multiplicative ℤ))
    (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))

Tactic:
Valued.continuous_valuation_of_surjective (fun x ↦ ?_)

Premises used: Valued.continuous_valuation_of_surjective
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
cont_f :
  ∀ (x : WithZero (Multiplicative ℤ)),
    ∃ (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)),
      ((Valued.v : Valuation (WithVal (R := K⟮X⟯) (polynomialValuationX K)) (WithZero (Multiplicative ℤ))) :
            (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
          a =
        x
⊢ Continuous.{u_2, 0} (X := WithVal (R := K⟮X⟯) (polynomialValuationX K)) (Y := WithZero (Multiplicative ℤ))
    (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))

Tactic:
refine Valued.continuous_valuation_of_surjective (fun x ↦ ?_)

Premises used: Valued.continuous_valuation_of_surjective
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
x : WithZero (Multiplicative ℤ)
cont_f :
  ∀ (y : K⟮X⟯),
    ∃ (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)),
      Eq (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation (WithVal (R := K⟮X⟯) (polynomialValuationX K)) (WithZero (Multiplicative ℤ))) :
              (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
            a :
          WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) y :
          WithZero (Multiplicative ℤ))
⊢ ∃ (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)),
    ((Valued.v : Valuation (WithVal (R := K⟮X⟯) (polynomialValuationX K)) (WithZero (Multiplicative ℤ))) :
          (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
        a =
      x

Tactic:
obtain ⟨y, rfl⟩ := RatFunc.valuation_surjective K x

Premises used: RatFunc.valuation_surjective, rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
y : K⟮X⟯
⊢ ∃ (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)),
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (WithVal (R := K⟮X⟯) (polynomialValuationX K)) (WithZero (Multiplicative ℤ))) :
            (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) y :
        WithZero (Multiplicative ℤ))

Tactic:
⟨.toVal _ y, rfl⟩

Premises used: Exists.intro, rfl, WithVal.toVal
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
y : K⟮X⟯
⊢ ∃ (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)),
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (WithVal (R := K⟮X⟯) (polynomialValuationX K)) (WithZero (Multiplicative ℤ))) :
            (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) y :
        WithZero (Multiplicative ℤ))

Tactic:
exact ⟨.toVal _ y, rfl⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
x : space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg
⊢ Continuous.{u_2, 0} (X := adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (Y := WithZero (Multiplicative ℤ))
    (⇑Valued.v : (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))

Tactic:
have h_cont := Valued.continuous_valuation_of_surjective
      (valuedAdicCompletion_surjective K⟮X⟯ (idealX K))
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
x : space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg
h_cont :
  Continuous.{u_2, 0} (X := adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (Y := WithZero (Multiplicative ℤ))
    (⇑Valued.v : (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
a :
  Tendsto (β := WithZero (Multiplicative ℤ))
    ((⇑Valued.v : (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)) → WithZero (Multiplicative ℤ)) :
      (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
    (Filter.comap (AbstractCompletion.coe ratfuncAdicComplPkg) (𝓝 x))
    (𝓝
        (((Valued.v :
              Valuation (UniformSpace.Completion (WithVal (R := K⟮X⟯) (polynomialValuationX K)))
                (WithZero (Multiplicative ℤ))) :
            (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → WithZero (Multiplicative ℤ))
          x) :
      Filter (WithZero (Multiplicative ℤ)))
⊢ Tendsto (β := WithZero (Multiplicative ℤ))
    (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
    (Filter.comap (AbstractCompletion.coe ratfuncAdicComplPkg) (𝓝 x))
    (𝓝 (IsDenseInducing.extend ⋯ (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ)) x))

Tactic:
rw [ratfuncAdicComplPkg.isDenseInducing.extend_unique
        Valued.valuedCompletion_apply h_cont]

Premises used: IsDenseInducing.extend_unique, Valued.valuedCompletion_apply, AbstractCompletion.isDenseInducing, LaurentSeries.ratfuncAdicComplPkg
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
x : space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg
h_cont :
  Continuous.{u_2, 0} (X := adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (Y := WithZero (Multiplicative ℤ))
    (⇑Valued.v : (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
⊢ Tendsto (β := WithZero (Multiplicative ℤ))
    ((⇑Valued.v : (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)) → WithZero (Multiplicative ℤ)) :
      (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
    (Filter.comap (AbstractCompletion.coe ratfuncAdicComplPkg) (𝓝 x))
    (𝓝
        (((Valued.v :
              Valuation (UniformSpace.Completion (WithVal (R := K⟮X⟯) (polynomialValuationX K)))
                (WithZero (Multiplicative ℤ))) :
            (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → WithZero (Multiplicative ℤ))
          x) :
      Filter (WithZero (Multiplicative ℤ)))

Tactic:
(h_cont.continuousAt.tendsto.comp tendsto_comap).congr
      Valued.valuedCompletion_apply

Premises used: Filter.tendsto_comap, Valued.valuedCompletion_apply, Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.congr, Filter.Tendsto.comp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
x : space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg
h_cont :
  Continuous.{u_2, 0} (X := adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (Y := WithZero (Multiplicative ℤ))
    (⇑Valued.v : (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
⊢ Tendsto (β := WithZero (Multiplicative ℤ))
    ((⇑Valued.v : (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)) → WithZero (Multiplicative ℤ)) :
      (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
    (Filter.comap (AbstractCompletion.coe ratfuncAdicComplPkg) (𝓝 x))
    (𝓝
        (((Valued.v :
              Valuation (UniformSpace.Completion (WithVal (R := K⟮X⟯) (polynomialValuationX K)))
                (WithZero (Multiplicative ℤ))) :
            (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → WithZero (Multiplicative ℤ))
          x) :
      Filter (WithZero (Multiplicative ℤ)))

Tactic:
exact (h_cont.continuousAt.tendsto.comp tendsto_comap).congr
      Valued.valuedCompletion_apply

Premises used: Filter.tendsto_comap, Valued.valuedCompletion_apply, Continuous.continuousAt, ContinuousAt.tendsto, Filter.Tendsto.congr, Filter.Tendsto.comp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⟦X⟧
⊢ Eq (α := ↥(powerSeries_as_subring K))
    ((powerSeriesEquivSubring K : (a : K⟦X⟧) → ↥(powerSeries_as_subring K)) f : ↥(powerSeries_as_subring K))
    (Subtype.mk (p := fun (x : K⸨X⸩) ↦ Membership.mem (γ := Subring K⸨X⸩) (powerSeries_as_subring K) x)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) ⋯ :
      ↥(powerSeries_as_subring K))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⟦X⟧
⊢ Eq (α := K⸨X⸩) ((↑((powerSeriesEquivSubring K : (a : K⟦X⟧) → ↥(powerSeries_as_subring K)) f) : K⸨X⸩) : K⸨X⸩)
    (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f : K⟦ℤ⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
simp :
  ∃ (F_1 : K⟦X⟧),
    Eq (α := K⟦ℤ⟧) (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F_1 : K⟦ℤ⟧)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧)
⊢ Membership.mem (α := RatFuncAdicCompl K) (γ := ValuationSubring (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)))
    (adicCompletionIntegers K⟮X⟯ (idealX K))
    ((LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) :
      RatFuncAdicCompl K)

Tactic:
simp only [mem_adicCompletionIntegers, LaurentSeriesRingEquiv_def,
    valuation_compare, val_le_one_iff_eq_coe]

Premises used: LaurentSeries.LaurentSeriesRingEquiv_def, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, LaurentSeries.val_le_one_iff_eq_coe, LaurentSeries.valuation_compare
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
⊢ ∃ (F_1 : K⟦X⟧),
    Eq (α := K⟦ℤ⟧) (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F_1 : K⟦ℤ⟧)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧)

Tactic:
⟨F, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
⊢ ∃ (F_1 : K⟦X⟧),
    Eq (α := K⟦ℤ⟧) (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F_1 : K⟦ℤ⟧)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧)

Tactic:
exact ⟨F, rfl⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
hx :
  Membership.mem (γ := ValuationSubring (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)))
    (adicCompletionIntegers K⟮X⟯ (idealX K)) x
⊢ let f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x;
  f = (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x

Tactic:
set f := (ratfuncAdicComplRingEquiv K) x with hf

Premises used: LaurentSeries.ratfuncAdicComplRingEquiv, DFunLike.coe
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
hx :
  Membership.mem (γ := ValuationSubring (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)))
    (adicCompletionIntegers K⟮X⟯ (idealX K)) x
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
hf : f = (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
⊢ AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
      ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x) =
    x

Tactic:
have H_x : (LaurentSeriesPkg K).compare ratfuncAdicComplPkg ((ratfuncAdicComplRingEquiv K) x) =
      x := congr_fun (inverse_compare (LaurentSeriesPkg K) ratfuncAdicComplPkg) x
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
hx :
  Membership.mem (γ := ValuationSubring (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)))
    (adicCompletionIntegers K⟮X⟯ (idealX K)) x
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
hf : f = (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
H_x :
  AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
      ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x) =
    x
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
        (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
          ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
rw [mem_adicCompletionIntegers, ← H_x] at hx

Premises used: IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers