-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T :
  (fun (x : K⟮X⟯ × K⟮X⟯) ↦
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x.2)) ⁻¹'
      T ⊆
    S
R : Set K⸨X⸩
hR : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) R
pre_R : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hd :
  {y : K⸨X⸩ |
      ((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 ℤ)))
          (y - 0) <
        (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    R
⊢ Membership.mem (γ := Filter K⟮X⟯) (nhds 0)
      {P : K⟮X⟯ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) P :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))} ∧
    Set.preimage (β := K⟮X⟯) (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1)
        {P : K⟮X⟯ |
          LT.lt (α := WithZero (Multiplicative ℤ))
            (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) P :
              WithZero (Multiplicative ℤ))
            ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
                (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
              WithZero (Multiplicative ℤ))} ⊆
      S
have h : (∃ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) Valued.v)ˣ),
    Subset.{u_2} (α := Set K⟮X⟯)
      {y : K⟮X⟯ |
        ((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 ℤ)))
            y <
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)}
      {P : K⟮X⟯ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) P :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))}) ∧
  Set.preimage (β := K⟮X⟯) (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1)
      {P : K⟮X⟯ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) P :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))} ⊆
    S
Tactic: simp only [Valued.mem_nhds, sub_zero]