awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
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))
pkg : AbstractCompletion.{u_2, u_2} (WithVal (R := K⟮X⟯) (polynomialValuationX 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⟦ℤ⟧)

Tactic:
rw [PowerSeries.coe_X, ← RatFunc.coe_X, ← LaurentSeries_coe, ← compare_coe]

Premises used: AbstractCompletion.compare_coe, RatFunc.coe_X, LaurentSeries.LaurentSeries_coe, PowerSeries.coe_X
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
a : K
⊢ Eq (α := K⸨X⸩) ((algebraMap K K⸨X⸩ : (a : K) → K⸨X⸩) a : K⸨X⸩) ((HahnSeries.C : (a : K) → K⟦ℤ⟧) a : K⟦ℤ⟧)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
K : Type u_2
inst : Field K
a : K
⊢ Eq (α := RatFuncAdicCompl K)
    ((LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K) ((algebraMap K K⸨X⸩ : (a : K) → K⸨X⸩) a) :
      RatFuncAdicCompl K)
    ((algebraMap K (RatFuncAdicCompl K) : (a : K) → RatFuncAdicCompl K) a : RatFuncAdicCompl K)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.LaurentSeries
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 ℤ))
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 ℤ))
⊢ 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 ℤ))

Tactic:
apply IsDenseInducing.extend_unique

Premises used: IsDenseInducing.extend_unique
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : WithVal (R := K⟮X⟯) (polynomialValuationX K)
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 ℤ))
⊢ 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:
rw [← WithVal.apply_ofVal, valuation_eq_LaurentSeries_valuation K]

Premises used: WithVal.apply_ofVal, RatFunc.valuation_eq_LaurentSeries_valuation
-- Module: Mathlib.RingTheory.LaurentSeries
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 ℤ))
    (((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:
rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
⊢ 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:
Valued.continuous_valuation_of_surjective (valuation_surjective K)

Premises used: LaurentSeries.valuation_surjective, Valued.continuous_valuation_of_surjective
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
⊢ 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:
exact Valued.continuous_valuation_of_surjective (valuation_surjective K)

Premises used: LaurentSeries.valuation_surjective, Valued.continuous_valuation_of_surjective
-- 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
S : Set (WithZero (Multiplicative ℤ))
hS :
  Membership.mem (γ := Filter (WithZero (Multiplicative ℤ)))
    (𝓝
        (((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 ℤ)))
    S
⊢ ∃ (i : WithZero (Multiplicative ℤ)), i ≠ 0 ∧ Set.Iio i ⊆ S

Tactic:
rw [ha, map_zero, WithZeroTopology.hasBasis_nhds_zero.1 S] at hS

Premises used: map_zero, WithZeroTopology.hasBasis_nhds_zero, Filter.HasBasis.mem_iff'
-- 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
S : Set (WithZero (Multiplicative ℤ))
hS : ∃ (i : WithZero (Multiplicative ℤ)), i ≠ 0 ∧ Set.Iio i ⊆ S
pos :
  ∀ (γ : WithZero (Multiplicative ℤ)) (γ_ne_zero : γ ≠ 0) (γ_le : Set.Iio γ ⊆ S),
    Membership.mem (γ := Filter K⟮X⟯)
      (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 : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) ⁻¹' S)
⊢ Membership.mem (γ := Filter K⟮X⟯)
    (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 : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) ⁻¹' S)

Tactic:
obtain ⟨γ, γ_ne_zero, γ_le⟩ := hS
-- 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
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
h :
  {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 ∧
    Subset.{u_2} (α := 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 <
            γ})
      ((⇑Valued.v : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) ⁻¹' S)
⊢ Membership.mem (γ := Filter K⟮X⟯)
    (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 : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) ⁻¹' S)

Tactic:
use {t | Valued.v t < γ}
-- 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
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
h :
  ∃ (γ_1 :
    (MonoidWithZeroHom.ValueGroup₀ (F :=
        Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) Valued.v)ˣ),
    Subset.{u_2} (α := Set (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)))
      {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 <
          (↑γ_1 : MonoidWithZeroHom.ValueGroup₀ Valued.v)}
      {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 <
          γ}
⊢ {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

Tactic:
rw [ha, this]
-- 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
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ Subset.{u_2} (α := 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 <
          γ})
    ((⇑Valued.v : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) ⁻¹' S)

Tactic:
Set.Subset.trans (fun a _ ↦ ?_) (Set.preimage_mono γ_le)

Premises used: Set.Subset.trans, Set.preimage_mono
-- 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
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
h :
  ∀ (a : K⟮X⟯),
    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 →
      Membership.mem (γ := Set K⟮X⟯) ((⇑Valued.v : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) ⁻¹' Set.Iio γ) a
⊢ Subset.{u_2} (α := 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 <
          γ})
    ((⇑Valued.v : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) ⁻¹' S)

Tactic:
refine Set.Subset.trans (fun a _ ↦ ?_) (Set.preimage_mono γ_le)

Premises used: Set.Subset.trans, Set.preimage_mono
-- 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_1 :
  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
h :
  ((Valued.v : Valuation (UniformSpace.Completion K⟮X⟯) (WithZero (Multiplicative ℤ))) :
        (a : UniformSpace.Completion K⟮X⟯) → WithZero (Multiplicative ℤ))
      (↑a : UniformSpace.Completion K⟮X⟯) <
    γ
⊢ Membership.mem (γ := Set K⟮X⟯) ((⇑Valued.v : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) ⁻¹' Set.Iio γ) a

Tactic:
rw [Set.mem_preimage, Set.mem_Iio, ← Valued.valuedCompletion_apply a]

Premises used: Set.mem_Iio, Valued.valuedCompletion_apply, Set.mem_preimage