awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : f = 0
x : K⸨X⸩
hg :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (x - f) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
rw [hf, sub_zero] at hg

Premises used: sub_zero
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : f = 0
x : K⸨X⸩
hg :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ ∀ n < 0, x.coeff n = 0

Tactic:
(valuation_le_iff_coeff_lt_eq_zero K).mp hg

Premises used: LaurentSeries.valuation_le_iff_coeff_lt_eq_zero, Iff.mp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : f = 0
x : K⸨X⸩
hg :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ ∀ n < 0, x.coeff n = 0

Tactic:
exact (valuation_le_iff_coeff_lt_eq_zero K).mp hg

Premises used: LaurentSeries.valuation_le_iff_coeff_lt_eq_zero, Iff.mp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : ¬f = 0
⊢ ∃ (N : ℤ),
    ∀ (g : K⸨X⸩),
      LE.le (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
              (g - f) :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ)) →
        ∀ n < N, g.coeff n = 0

Tactic:
⟨min (f.2.isWF.min (HahnSeries.support_nonempty_iff.mpr hf)) 0 - 1, fun _ hg n hn ↦ ?_⟩

Premises used: Iff.mpr, HSub.hSub, HahnSeries.isPWO_support', Set.IsPWO.isWF, HahnSeries.support_nonempty_iff, Set.IsWF.min, Exists.intro, OfNat.ofNat, Min.min
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : ¬f = 0
neg :
  ∀ (x : K⸨X⸩)
    (hg :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (x - f) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)))
    (n : ℤ) (hn : n < min (⋯.min (s := Function.support f.coeff) ⋯) 0 - 1), x.coeff n = 0
⊢ ∃ (N : ℤ),
    ∀ (g : K⸨X⸩),
      LE.le (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
              (g - f) :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ)) →
        ∀ n < N, g.coeff n = 0

Tactic:
refine ⟨min (f.2.isWF.min (HahnSeries.support_nonempty_iff.mpr hf)) 0 - 1, fun _ hg n hn ↦ ?_⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : ¬f = 0
x : K⸨X⸩
hg :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (x - f) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : ℤ
hn : n < min (⋯.min (s := Function.support f.coeff) ⋯) 0 - 1
neg : f.coeff n = 0
neg₁ : n < 0
⊢ x.coeff n = 0

Tactic:
rw [eq_coeff_of_valuation_sub_lt K hg (d := 0)]

Premises used: LaurentSeries.eq_coeff_of_valuation_sub_lt
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : ¬f = 0
x : K⸨X⸩
hg :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (x - f) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : ℤ
hn : n < min (⋯.min (s := Function.support f.coeff) ⋯) 0 - 1
⊢ f.coeff n = 0

Tactic:
Function.notMem_support.mp fun h ↦
        f.2.isWF.not_lt_min (HahnSeries.support_nonempty_iff.mpr hf) h
        <| lt_trans hn <| Int.sub_one_lt_iff.mpr <| min_le_left _ _

Premises used: Iff.mpr, lt_trans, Set.IsWF.not_lt_min, HahnSeries.isPWO_support', Set.IsPWO.isWF, Function.notMem_support, HahnSeries.support_nonempty_iff, min_le_left, Set.IsWF.min, Iff.mp, OfNat.ofNat, Int.sub_one_lt_iff
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : ¬f = 0
x : K⸨X⸩
hg :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (x - f) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : ℤ
hn : n < min (⋯.min (s := Function.support f.coeff) ⋯) 0 - 1
⊢ f.coeff n = 0

Tactic:
exact Function.notMem_support.mp fun h ↦
        f.2.isWF.not_lt_min (HahnSeries.support_nonempty_iff.mpr hf) h
        <| lt_trans hn <| Int.sub_one_lt_iff.mpr <| min_le_left _ _

Premises used: Iff.mpr, lt_trans, Set.IsWF.not_lt_min, HahnSeries.isPWO_support', Set.IsPWO.isWF, Function.notMem_support, HahnSeries.support_nonempty_iff, min_le_left, Set.IsWF.min, Iff.mp, OfNat.ofNat, Int.sub_one_lt_iff
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : ¬f = 0
x : K⸨X⸩
hg :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (x - f) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : ℤ
hn : n < min (⋯.min (s := Function.support f.coeff) ⋯) 0 - 1
⊢ n < 0

Tactic:
lt_of_lt_of_le hn <| le_of_lt (Int.sub_one_lt_of_le <| min_le_right _ _)

Premises used: Int.sub_one_lt_of_le, le_of_lt, min_le_right, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : ¬f = 0
x : K⸨X⸩
hg :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (x - f) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : ℤ
hn : n < min (⋯.min (s := Function.support f.coeff) ⋯) 0 - 1
⊢ n < 0

Tactic:
exact lt_of_lt_of_le hn <| le_of_lt (Int.sub_one_lt_of_le <| min_le_right _ _)

Premises used: Int.sub_one_lt_of_le, le_of_lt, min_le_right, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
obtain :
  ∀ (N : ℤ)
    (hN :
      ∀ (g : K⸨X⸩),
        LE.le (α := WithZero (Multiplicative ℤ))
            (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
                (g - f) :
              WithZero (Multiplicative ℤ))
            (1 : WithZero (Multiplicative ℤ)) →
          ∀ n < N, g.coeff n = 0),
    ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
⊢ ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0

Tactic:
obtain ⟨N, hN⟩ : ∃ N : ℤ, ∀ g : K⸨X⸩,
    Valued.v (g - f) ≤ 1 → ∀ n < N, g.coeff n = 0 := by
    by_cases hf : f = 0
    · refine ⟨0, fun x hg ↦ ?_⟩
      rw [hf, sub_zero] at hg
      exact (valuation_le_iff_coeff_lt_eq_zero K).mp hg
    · refine ⟨min (f.2.isWF.min (HahnSeries.support_nonempty_iff.mpr hf)) 0 - 1, fun _ hg n hn ↦ ?_⟩
      rw [eq_coeff_of_valuation_sub_lt K hg (d := 0)]
      · exact Function.notMem_support.mp fun h ↦
        f.2.isWF.not_lt_min (HahnSeries.support_nonempty_iff.mpr hf) h
        <| lt_trans hn <| Int.sub_one_lt_iff.mpr <| min_le_left _ _
      exact lt_of_lt_of_le hn <| le_of_lt (Int.sub_one_lt_of_le <| min_le_right _ _)
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN :
  ∀ (g : K⸨X⸩),
    LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (g - f) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) →
      ∀ n < N, g.coeff n = 0
h : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
⊢ ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0

Tactic:
use N
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((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 ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN :
  ∀ (g : K⸨X⸩),
    LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (g - f) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) →
      ∀ n < N, g.coeff n = 0
h : S ∩ T ⊆ {x : K⸨X⸩ | (fun (f : K⸨X⸩) ↦ ∀ n < N, f.coeff n = 0) x}
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0

Tactic:
apply mem_of_superset (inter_mem hS hT)

Premises used: Filter.inter_mem, Filter.mem_of_superset