-- 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
x : adicCompletion (R := K[X]) K⟮X⟯ (idealX K)
hx :
  ((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
        (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
      x =
    γ
rwa :
  Ne (α :=
    MonoidWithZeroHom.ValueGroup₀ (F :=
      Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) Valued.v)
    (((restrict₀ Valued.v :
            adicCompletion (R := K[X]) K⟮X⟯ (idealX K) →*₀
              MonoidWithZeroHom.ValueGroup₀ (F :=
                Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) Valued.v) :
          (a : adicCompletion K⟮X⟯ (idealX K)) → MonoidWithZeroHom.ValueGroup₀ Valued.v)
        x :
      MonoidWithZeroHom.ValueGroup₀ (F :=
        Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) Valued.v)
    (0 :
      MonoidWithZeroHom.ValueGroup₀ (F :=
        Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) Valued.v)
rwa₁ :
  ¬Eq (α :=
      MonoidWithZeroHom.ValueGroup₀ (F :=
        Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) Valued.v)
      (((restrict₀ Valued.v :
              adicCompletion (R := K[X]) K⟮X⟯ (idealX K) →*₀
                MonoidWithZeroHom.ValueGroup₀ (F :=
                  Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) Valued.v) :
            (a : adicCompletion K⟮X⟯ (idealX K)) → MonoidWithZeroHom.ValueGroup₀ Valued.v)
          x :
        MonoidWithZeroHom.ValueGroup₀ (F :=
          Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) Valued.v)
      (0 :
        MonoidWithZeroHom.ValueGroup₀ (F :=
          Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) Valued.v)
rwa₂ :
  ¬Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
          x :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))
rwa₃ rwa₄ rwa₅ rwa₆ : ¬γ = 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 ℤ)))
        x :
      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:
rwa [Valuation.restrict_def, ne_eq, restrict₀_eq_zero_iff, hx]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff, ne_eq, Valuation.restrict_def