-- 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
⊢ ∃ (γ : (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 ℤ))}
have h : ∀ (x : K⟮X⟯)
  (hx :
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
        WithZero (Multiplicative ℤ))),
  ∃ (γ : (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 ℤ))}
Tactic: obtain ⟨x, hx⟩ := RatFunc.valuation_surjective K (embedding d.1)