-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
a : adicCompletion (R := K[X]) K⟮X⟯ (idealX K)
this :
  ∀ (s : Set (adicCompletion (R := K[X]) K⟮X⟯ (idealX K))),
    Membership.mem (γ := Filter (adicCompletion (R := K[X]) K⟮X⟯ (idealX K))) (𝓝 0) s ↔
      ∃ (γ :
        (MonoidWithZeroHom.ValueGroup₀ (F :=
            Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) Valued.v)ˣ),
        {x : adicCompletion (R := K[X]) K⟮X⟯ (idealX K) |
            ((Valuation.restrict Valued.v :
                    Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K))
                      (MonoidWithZeroHom.ValueGroup₀ (F :=
                        adicCompletion (R := K[X]) K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ))
                        (↑Valued.v : adicCompletion K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ)))) :
                  (a : adicCompletion K⟮X⟯ (idealX K)) →
                    MonoidWithZeroHom.ValueGroup₀
                      (↑Valued.v : adicCompletion K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ)))
                x <
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
          s
ha : a = 0
S : Set (WithZero (Multiplicative ℤ))
γ : WithZero (Multiplicative ℤ)
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
h :
  {t : adicCompletion (R := K[X]) K⟮X⟯ (idealX K) |
      ((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
          t <
        γ} ∈
    𝓝 a
⊢ {t : adicCompletion (R := K[X]) K⟮X⟯ (idealX K) |
        ((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
            t <
          γ} ∈
      𝓝 a ∧
    Subset.{u_2} (α := Set K⟮X⟯)
      (Set.preimage (β := adicCompletion (R := K[X]) K⟮X⟯ (idealX K))
        (fun (x : K⟮X⟯) ↦
          (↑((RingEquiv.symm (WithVal.equiv (valuation (R := K[X]) K⟮X⟯ (idealX K))) :
                  (a : K⟮X⟯) → WithVal (valuation K⟮X⟯ (idealX K)))
                x) :
            UniformSpace.Completion (WithVal (valuation K⟮X⟯ (idealX K)))))
        {t : adicCompletion (R := K[X]) K⟮X⟯ (idealX K) |
          ((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
                (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
              t <
            γ})
      ((⇑Valued.v : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) ⁻¹' S)
have h₁ : Subset.{u_2} (α := Set K⟮X⟯)
  (Set.preimage (β := adicCompletion (R := K[X]) K⟮X⟯ (idealX K))
    (fun (x : K⟮X⟯) ↦
      (↑((RingEquiv.symm (WithVal.equiv (valuation (R := K[X]) K⟮X⟯ (idealX K))) :
              (a : K⟮X⟯) → WithVal (valuation K⟮X⟯ (idealX K)))
            x) :
        UniformSpace.Completion (WithVal (valuation K⟮X⟯ (idealX K)))))
    {t : adicCompletion (R := K[X]) K⟮X⟯ (idealX K) |
      ((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
          t <
        γ})
  ((⇑Valued.v : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) ⁻¹' S)
Tactic: constructor