-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
w : Set K⟮X⟯
hT : Membership.mem (γ := Filter K⟮X⟯) (nhds 0) w
pre_T : (fun (x : K⟮X⟯ × K⟮X⟯) ↦ x.2 - x.1) ⁻¹' w ⊆ S
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)} ⊆
    w
X : Set K⸨X⸩ :=
  {f : K⸨X⸩ |
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
        WithZero (Multiplicative ℤ))}
X_def :
  X =
    {f : K⸨X⸩ |
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
          WithZero (Multiplicative ℤ))
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
          WithZero (Multiplicative ℤ))}
x : K⟮X⟯
hx :
  ((restrict₀ Valued.v :
          K⟮X⟯ →*₀ MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) Valued.v) :
        (a : K⟮X⟯) → MonoidWithZeroHom.ValueGroup₀ Valued.v)
      x =
    (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v)
⊢ ∃ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ),
    {y : K⸨X⸩ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) y :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))} ⊆
      X
have h : {y : K⸨X⸩ |
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) y :
        WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          ((↑(Units.mk0
                  (((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 ℤ)))
                    ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x))
                  sorry) :
              MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v) :
            MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v) :
        WithZero (Multiplicative ℤ))} ⊆
  X
Tactic: use Units.mk0 (Valued.v.restrict (x : K⸨X⸩)) (by
          rw [Valuation.restrict_def, ne_eq, restrict₀_eq_zero_iff, valuation_def,
            ← valuation_eq_LaurentSeries_valuation, ← v_def, ← restrict₀_eq_zero_iff]
          simp [hx])