awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ,
    ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = f.coeff d

Tactic:
have := (exists_lb_coeff_ne hℱ).choose_spec
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
this :
  ∀ᶠ (f : K⸨X⸩) in ℱ,
    ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = f.coeff d
⊢ {x : K⸨X⸩ |
      ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d} ∈
    ℱ

Tactic:
rw [Filter.eventually_iff] at this

Premises used: Filter.eventually_iff
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
this :
  {x : K⸨X⸩ |
      ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d} ∈
    ℱ
⊢ {x : K⸨X⸩ |
      ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d} ∈
    ℱ

Tactic:
this
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
this :
  {x : K⸨X⸩ |
      ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d} ∈
    ℱ
h :
  Eq.{u_2 + 1} (α := Set K⸨X⸩) (⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n)
    {x : K⸨X⸩ |
      ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d}
⊢ ⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n ∈ ℱ

Tactic:
convert! this
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
this :
  {x : K⸨X⸩ |
      ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d} ∈
    ℱ
h :
  ∀ (x : K⸨X⸩),
    Membership.mem (γ := Set K⸨X⸩) (⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n) x ↔
      Membership.mem (γ := Set K⸨X⸩)
        {x : K⸨X⸩ |
          ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d),
            coeff hℱ d = x.coeff d}
        x
⊢ Eq.{u_2 + 1} (α := Set K⸨X⸩) (⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n)
    {x : K⸨X⸩ |
      ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d}

Tactic:
ext
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
this :
  {x : K⸨X⸩ |
      ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d} ∈
    ℱ
x : K⸨X⸩
h :
  (∀ (i : ℤ) (i_1 : i < ℓ), x ∈ φ i) ↔
    ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d
⊢ Membership.mem (γ := Set K⸨X⸩) (⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n) x ↔
    Membership.mem (γ := Set K⸨X⸩)
      {x : K⸨X⸩ |
        ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d}
      x

Tactic:
simp only [Set.mem_iInter, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, Set.mem_iInter
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
this :
  {x : K⸨X⸩ |
      ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d} ∈
    ℱ
x : K⸨X⸩
⊢ (∀ (i : ℤ) (i_1 : i < ℓ), x ∈ φ i) ↔
    ∀ d < ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d), coeff hℱ d = x.coeff d

Tactic:
rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
right : ∀ i ∈ Set.Icc ℓ N, φ i ∈ ℱ
⊢ ⋂ n ∈ Set.Icc ℓ N, φ n ∈ ℱ

Tactic:
rw [biInter_mem (Set.finite_Icc ℓ N)]

Premises used: Set.finite_Icc, Filter.biInter_mem
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
i : ℤ
right : i ∈ Set.Icc ℓ N → φ i ∈ ℱ
⊢ i ∈ Set.Icc ℓ N → φ i ∈ ℱ

Tactic:
_
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
i : ℤ
h : i ∈ Set.Icc ℓ N
right : ∀ᶠ (y : K) in 𝓟 {coeff hℱ i}, coeff hℱ i = y
⊢ φ i ∈ ℱ

Tactic:
apply (coeff_tendsto hℱ _).eventually

Premises used: LaurentSeries.Cauchy.coeff_tendsto, Filter.Tendsto.eventually
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
intersec₂ : Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
i : ℤ
h : i ∈ Set.Icc ℓ N
⊢ ∀ᶠ (y : K) in 𝓟 {coeff hℱ i}, coeff hℱ i = y

Tactic:
simp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
obtain :
  ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ)
    (hU₁ :
      {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 - limit hℱ) <
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
        U),
    ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U

Tactic:
obtain ⟨γ, hU₁⟩ := Valued.mem_nhds.mp hU

Premises used: Valued.mem_nhds, Iff.mp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hU₁ :
  {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 - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    U
this :
  ∀ᶠ (f : K⸨X⸩) in ℱ,
    Membership.mem (γ := Set K⸨X⸩)
      {y : K⸨X⸩ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
              (y - limit hℱ) :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))}
      f
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ,
    Membership.mem (γ := Set K⸨X⸩)
      {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 - limit hℱ) <
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)}
      f

Tactic:
simp_rw [← Valued.v.restrict_lt_iff_lt_embedding] at this

Premises used: Valued.v, Valuation.restrict_lt_iff_lt_embedding
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hU₁ :
  {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 - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    U
this :
  ∀ᶠ (f : K⸨X⸩) in ℱ,
    Membership.mem (γ := Set K⸨X⸩)
      {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 - limit hℱ) <
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)}
      f
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U

Tactic:
apply this.mono fun _ hf ↦ hU₁ hf

Premises used: Filter.Eventually.mono
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hU₁ :
  {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 - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    U
suffices :
  ∀ᶠ (f : K⸨X⸩) in ℱ,
    Membership.mem (γ := Set K⸨X⸩)
      {y : K⸨X⸩ |
        LT.lt (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
              (y - limit hℱ) :
            WithZero (Multiplicative ℤ))
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
            WithZero (Multiplicative ℤ))}
      f
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, f ∈ U

Tactic:
suffices ∀ᶠ f in ℱ, f ∈ {y : K⸨X⸩ | Valued.v (y - limit hℱ) < embedding γ.1} by
    simp_rw [← Valued.v.restrict_lt_iff_lt_embedding] at this
    apply this.mono fun _ hf ↦ hU₁ hf
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hU₁ :
  {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 - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    U
⊢ let D :=
    -HSub.hSub (α := ℤ)
        (log
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
        1;
  D =
    -HSub.hSub (α := ℤ)
        (log
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
        1

Tactic:
set D := -(log (embedding γ.1) - 1) with hD₀

Premises used: Units.val, HSub.hSub, WithZero.log, MonoidWithZeroHom.ValueGroup₀.embedding, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hU₁ :
  {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 - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    U
D : ℤ :=
  -HSub.hSub (α := ℤ)
      (log
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
      1
hD₀ :
  D =
    -HSub.hSub (α := ℤ)
        (log
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
        1
⊢ Ne (α := WithZero (Multiplicative ℤ))
    ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))

Tactic:
simp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hU₁ :
  {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 - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    U
D : ℤ :=
  -HSub.hSub (α := ℤ)
      (log
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
      1
hD₀ :
  D =
    -HSub.hSub (α := ℤ)
        (log
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
        1
rw :
  -
      -HSub.hSub (α := ℤ)
          (log
            ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
          1 <
    log
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v))
⊢ exp (-D) <
    (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)

Tactic:
rw [← lt_log_iff_exp_lt (by simp), hD₀]

Premises used: WithZero.lt_log_iff_exp_lt
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hU₁ :
  {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 - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    U
D : ℤ :=
  -HSub.hSub (α := ℤ)
      (log
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
      1
hD₀ :
  D =
    -HSub.hSub (α := ℤ)
        (log
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
        1
⊢ -
      -HSub.hSub (α := ℤ)
          (log
            ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
              (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
          1 <
    log
      ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v))

Tactic:
simp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
U : Set K⸨X⸩
hU : U ∈ 𝓝 (limit hℱ)
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hU₁ :
  {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 - limit hℱ) <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    U
D : ℤ :=
  -HSub.hSub (α := ℤ)
      (log
        ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
      1
hD₀ :
  D =
    -HSub.hSub (α := ℤ)
        (log
          ((embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
            (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)))
        1
⊢ exp (-D) <
    (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)

Tactic:
have hD : exp (-D) < embedding γ.1 := by
    rw [← lt_log_iff_exp_lt (by simp), hD₀]
    simp