-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 ℤ)))
⊢ 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 ℤ))}
have 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)}
Tactic: simp_rw [← Valued.v.restrict_lt_iff_lt_embedding]