awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hD :
  exp (-D) <
    (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
apply :
  ∀ (x : K⸨X⸩),
    (∀ d < D, coeff hℱ d = x.coeff d) →
      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 ℤ))}
        x
⊢ ∀ᶠ (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

Tactic:
apply coeff_eventually_equal (D := D) hℱ |>.mono

Premises used: Filter.Eventually.mono, LaurentSeries.Cauchy.coeff_eventually_equal
-- 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
hD :
  exp (-D) <
    (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
x : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x.coeff d
n : ℤ
hn : n < D
rw : (limit hℱ).coeff n = x.coeff n
⊢ (x - limit hℱ).coeff n = 0

Tactic:
rw [HahnSeries.coeff_sub, sub_eq_zero, eq_comm]

Premises used: sub_eq_zero, HahnSeries.coeff_sub, eq_comm
-- 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
hD :
  exp (-D) <
    (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
x : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x.coeff d
n : ℤ
hn : n < D
⊢ (limit hℱ).coeff n = x.coeff n

Tactic:
hf _ hn

Premises used: LaurentSeries.Cauchy.coeff, Classical.choose, DiscreteUniformity.cauchyConst
-- 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
hD :
  exp (-D) <
    (embedding : (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
      (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)
x : K⸨X⸩
hf : ∀ d < D, coeff hℱ d = x.coeff d
n : ℤ
hn : n < D
⊢ (limit hℱ).coeff n = x.coeff n

Tactic:
exact hf _ hn
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
K : Type u_2
inst : Field K
⊢ CompleteSpace.{u_2} K⸨X⸩

Tactic:
⟨fun hℱ ↦ ⟨Cauchy.limit hℱ, fun _ hS ↦ Cauchy.eventually_mem_nhds hℱ hS⟩⟩

Premises used: LaurentSeries.Cauchy.limit, CompleteSpace.mk, LaurentSeries.Cauchy.eventually_mem_nhds, Exists.intro
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
pos :
  ∀ (h_neg : 1 < η),
    ∃ (P : K[X]),
      ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          (F - (↑P : K⟦X⟧)) <
        (↑η : WithZero (Multiplicative ℤ))
neg :
  ∀ (h_neg : η ≤ 1),
    ∃ (P : K[X]),
      ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          (F - (↑P : K⟦X⟧)) <
        (↑η : WithZero (Multiplicative ℤ))
⊢ ∃ (P : K[X]),
    ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (F - (↑P : K⟦X⟧)) <
      (↑η : WithZero (Multiplicative ℤ))

Tactic:
by_cases! h_neg : 1 < η
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : 1 < η
h :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑0 : K⟦X⟧)) <
    (↑η : WithZero (Multiplicative ℤ))
⊢ ∃ (P : K[X]),
    ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (F - (↑P : K⟦X⟧)) <
      (↑η : WithZero (Multiplicative ℤ))

Tactic:
use 0
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : 1 < η
⊢ ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑0 : K⟦X⟧)) <
    (↑η : WithZero (Multiplicative ℤ))

Tactic:
simpa using (intValuation_le_one (PowerSeries.idealX K) F).trans_lt h_neg

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_le_one, PowerSeries.idealX, LE.le.trans_lt
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : η ≤ 1
⊢ LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)

Tactic:
rw [← Units.val_le_val, Units.val_one, ← WithZero.coe_one, ← coe_unzero η.ne_zero,
      coe_le_coe, ← Multiplicative.toAdd_le, toAdd_one] at h_neg

Premises used: Units.ne_zero, Units.val_le_val, WithZero.coe_unzero, toAdd_one, Multiplicative.toAdd_le, Units.val_one, WithZero.coe_le_coe, WithZero.coe_one
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
neg :
  ∀ (d : ℕ) (hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)),
    ∃ (P : K[X]),
      ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          (F - (↑P : K⟦X⟧)) <
        (↑η : WithZero (Multiplicative ℤ))
⊢ ∃ (P : K[X]),
    ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (F - (↑P : K⟦X⟧)) <
      (↑η : WithZero (Multiplicative ℤ))

Tactic:
obtain ⟨d, hd⟩ := Int.exists_eq_neg_ofNat h_neg

Premises used: Int.exists_eq_neg_ofNat
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
d : ℕ
hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)
h :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧)) <
    (↑η : WithZero (Multiplicative ℤ))
⊢ ∃ (P : K[X]),
    ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (F - (↑P : K⟦X⟧)) <
      (↑η : WithZero (Multiplicative ℤ))

Tactic:
use F.trunc (d + 1)

Premises used: HAdd.hAdd, OfNat.ofNat, DFunLike.coe, PowerSeries.trunc
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
d : ℕ
hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)
apply :
  ∀ n < d + 1,
    Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧)) : K)
      (0 : K)
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧)
          (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧))) :
      WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-HAdd.hAdd (α := ℤ) (↑d : ℤ) 1)) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))

Tactic:
apply (intValuation_le_iff_coeff_lt_eq_zero K _).mpr

Premises used: Iff.mpr, LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
d : ℕ
hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)
⊢ ∀ n < d + 1,
    Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧)) : K)
      (0 : K)

Tactic:
simpa only [map_sub, sub_eq_zero, Polynomial.coeff_coe, coeff_trunc] using
        fun _ h ↦ (if_pos h).symm

Premises used: PowerSeries.coeff_trunc, map_sub, sub_eq_zero, if_pos, Eq.symm, Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
d : ℕ
hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧)
          (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧))) :
      WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-HAdd.hAdd (α := ℤ) (↑d : ℤ) 1)) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))

Tactic:
have : Valued.v ((ofPowerSeries ℤ K) (F - (trunc (d + 1) F))) ≤
      (Multiplicative.ofAdd (-(d + 1 : ℤ))) := by
      apply (intValuation_le_iff_coeff_lt_eq_zero K _).mpr
      simpa only [map_sub, sub_eq_zero, Polynomial.coeff_coe, coeff_trunc] using
        fun _ h ↦ (if_pos h).symm
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
d : ℕ
hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)
this :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧)
          (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧))) :
      WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-HAdd.hAdd (α := ℤ) (↑d : ℤ) 1)) :
        WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧))) ≤
    HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))

Tactic:
rw [neg_add, ofAdd_add, ← hd, ofAdd_toAdd, WithZero.coe_mul, coe_unzero,
      ← coe_algebraMap] at this

Premises used: ofAdd_toAdd, LaurentSeries.coe_algebraMap, neg_add, WithZero.coe_unzero, ofAdd_add, WithZero.coe_mul
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
d : ℕ
hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)
this :
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧))) ≤
    HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))
h :
  ((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
        (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (↑(F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧)) : K⸨X⸩) <
    (↑η : WithZero (Multiplicative ℤ))
⊢ ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧)) <
    (↑η : WithZero (Multiplicative ℤ))

Tactic:
rw [← valuation_of_algebraMap (K := K⸨X⸩) (PowerSeries.idealX K) (F - F.trunc (d + 1))]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, HSub.hSub, PowerSeries.idealX, HAdd.hAdd, Polynomial.toPowerSeries, OfNat.ofNat, DFunLike.coe, PowerSeries.trunc
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
d : ℕ
hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)
this :
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧))) ≤
    HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))
h :
  HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ)) <
    (↑η : WithZero (Multiplicative ℤ))
⊢ ((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
        (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (↑(F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧)) : K⸨X⸩) <
    (↑η : WithZero (Multiplicative ℤ))

Tactic:
apply lt_of_le_of_lt this

Premises used: lt_of_le_of_lt
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
d : ℕ
hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)
this :
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧))) ≤
    HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))
h :
  HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ)) <
    (↑η : WithZero (Multiplicative ℤ)) * 1
⊢ HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ)) <
    (↑η : WithZero (Multiplicative ℤ))

Tactic:
rw [← mul_one (η : ℤᵐ⁰), mul_assoc, one_mul]

Premises used: Units.val, mul_assoc, mul_one, one_mul
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
d : ℕ
hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)
this :
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧))) ≤
    HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))
h : 0 < (↑η : WithZero (Multiplicative ℤ))
h₁ :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ)) <
    (↑η : WithZero (Multiplicative ℤ)) * 1

Tactic:
gcongr
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
d : ℕ
hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)
this :
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧))) ≤
    HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))
⊢ 0 < (↑η : WithZero (Multiplicative ℤ))

Tactic:
zero_lt_iff.2 η.ne_zero

Premises used: Iff.mpr, Units.ne_zero, zero_lt_iff
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
d : ℕ
hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)
this :
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧))) ≤
    HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))
⊢ 0 < (↑η : WithZero (Multiplicative ℤ))

Tactic:
exact zero_lt_iff.2 η.ne_zero

Premises used: Iff.mpr, Units.ne_zero, zero_lt_iff