-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
x : K⸨X⸩
hx :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x =
    (↑γ : WithZero (Multiplicative ℤ))
this :
  Ne (α :=
    MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
      (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
    (((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 ℤ)))
        x :
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
    (0 :
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
h :
  Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩)
    {P : K⸨X⸩ × K⸨X⸩ |
      LT.lt (α :=
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
        (((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 ℤ)))
            (P.2 - P.1) :
          MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
            (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
        (((MonoidWithZeroHom.ValueGroup₀.restrict₀ Valued.v :
                K⸨X⸩ →*₀ MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v) :
              (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ Valued.v)
            x :
          MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)}
⊢ Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩)
    {P : K⸨X⸩ × K⸨X⸩ |
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (P.2 - P.1) :
          WithZero (Multiplicative ℤ))
        ((MonoidWithZeroHom.ValueGroup₀.embedding :
              (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (((MonoidWithZeroHom.ValueGroup₀.restrict₀ Valued.v :
                    K⸨X⸩ →*₀
                      MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v) :
                  (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ Valued.v)
                x :
              MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v) :
          WithZero (Multiplicative ℤ))}

Tactic:
simp_rw [← Valued.v.restrict_lt_iff_lt_embedding]

Premises used: Valued.v, Valuation.restrict_lt_iff_lt_embedding