-- 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
h :
  Subset.{u_2} (α := Set (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)))
    {y : adicCompletion (R := K[X]) K⟮X⟯ (idealX K) |
      LT.lt (α :=
        MonoidWithZeroHom.ValueGroup₀ (F := adicCompletion (R := K[X]) K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : adicCompletion K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ)))
        (((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 ℤ)))
            (y - a) :
          MonoidWithZeroHom.ValueGroup₀ (F :=
            adicCompletion (R := K[X]) K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ))
            (↑Valued.v : adicCompletion K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ)))
        ((↑(Units.mk0
                (((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 :=
              Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) Valued.v) :
          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) |
      ∀ (a_1 : K⟮X⟯),
        (↑((RingEquiv.symm (WithVal.equiv (valuation (R := K[X]) K⟮X⟯ (idealX K))) :
                    (a : K⟮X⟯) → WithVal (valuation K⟮X⟯ (idealX K)))
                  a_1) :
              UniformSpace.Completion (WithVal (valuation K⟮X⟯ (idealX K)))) =
            x →
          Eq (α := WithZero (Multiplicative ℤ))
            (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
                a_1 :
              WithZero (Multiplicative ℤ))
            (((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
                  (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
                a :
              WithZero (Multiplicative ℤ))}
⊢ ∃ (γ :
    (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)))
      {y : 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 ℤ)))
            (y - a) <
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)}
      {x : adicCompletion (R := K[X]) K⟮X⟯ (idealX K) |
        ∀ (a_1 : K⟮X⟯),
          (↑((RingEquiv.symm (WithVal.equiv (valuation (R := K[X]) K⟮X⟯ (idealX K))) :
                      (a : K⟮X⟯) → WithVal (valuation K⟮X⟯ (idealX K)))
                    a_1) :
                UniformSpace.Completion (WithVal (valuation K⟮X⟯ (idealX K)))) =
              x →
            Eq (α := WithZero (Multiplicative ℤ))
              (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
                  a_1 :
                WithZero (Multiplicative ℤ))
              (((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
                    (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
                  a :
                WithZero (Multiplicative ℤ))}

Tactic:
use Units.mk0 (Valued.v.restrict a) (by simp [Valuation.restrict_def, ha])

Premises used: Valued.v, Units.mk0, DFunLike.coe, Valuation.restrict