-- Module: Mathlib.RingTheory.LaurentSeries
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
b : K⟮X⟯
val_y :
  LT.lt (α :=
    MonoidWithZeroHom.ValueGroup₀ (F := adicCompletion (R := K[X]) K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ))
      (↑Valued.v : adicCompletion K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ)))
    (((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 ℤ)))
        (HSub.hSub (α := adicCompletion (R := K[X]) K⟮X⟯ (idealX K))
          ((↑((RingEquiv.symm (WithVal.equiv (valuation (R := K[X]) K⟮X⟯ (idealX K))) :
                    (a : K⟮X⟯) → WithVal (valuation K⟮X⟯ (idealX K)))
                  b) :
              UniformSpace.Completion (WithVal (R := K⟮X⟯) (valuation (R := K[X]) K⟮X⟯ (idealX K)))) :
            UniformSpace.Completion (WithVal (R := K⟮X⟯) (valuation (R := K[X]) K⟮X⟯ (idealX K))))
          a) :
      MonoidWithZeroHom.ValueGroup₀ (F := adicCompletion (R := K[X]) K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : adicCompletion K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ)))
    (((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 ℤ)))
        a :
      MonoidWithZeroHom.ValueGroup₀ (F := adicCompletion (R := K[X]) K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : adicCompletion K⟮X⟯ (idealX K) →*₀ WithZero (Multiplicative ℤ)))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v :
            Valuation (UniformSpace.Completion (WithVal (R := K⟮X⟯) (valuation (R := K[X]) K⟮X⟯ (idealX K))))
              (WithZero (Multiplicative ℤ))) :
          (a : UniformSpace.Completion (WithVal (valuation K⟮X⟯ (idealX K)))) → WithZero (Multiplicative ℤ))
        (↑((RingEquiv.symm (WithVal.equiv (valuation (R := K[X]) K⟮X⟯ (idealX K))) :
                (a : K⟮X⟯) → WithVal (valuation K⟮X⟯ (idealX K)))
              b) :
          UniformSpace.Completion (WithVal (valuation K⟮X⟯ (idealX K)))) :
      WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
        a :
      WithZero (Multiplicative ℤ))

Tactic:
exact (Valuation.restrict_inj _).mp <| Valuation.map_eq_of_sub_lt Valued.v.restrict val_y

Premises used: Valued.v, Valuation.restrict_inj, Iff.mp, Valuation.map_eq_of_sub_lt, Valuation.restrict