-- 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)
⊢ {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))
                    ⋯) :
                MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v) :
              MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v) :
          WithZero (Multiplicative ℤ))} ⊆
    X
have h : ∀ (a : K⸨X⸩),
  LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a :
        WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
          ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) x) :
        WithZero (Multiplicative ℤ)) →
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a :
        WithZero (Multiplicative ℤ))
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑d : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
        WithZero (Multiplicative ℤ))
Tactic: simp only [Units.val_mk0, ← Valuation.restrict_lt_iff_lt_embedding,
          X_def, Set.setOf_subset_setOf, Valuation.restrict_lt_iff]