awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
m : ℕ
hm : n + (↑s : ℤ) = (↑m : ℤ)
d : ℕ
hd : D + (↑s : ℤ) = (↑d : ℤ)
pos : Eq (α := K) ((PowerSeries.coeff m : (a : K⟦X⟧) → K) f.powerSeriesPart : K) (0 : K)
⊢ f.coeff n = 0

Tactic:
rw [eq_add_neg_of_add_eq hm, add_comm, ← hs, ← powerSeriesPart_coeff]

Premises used: eq_add_neg_of_add_eq, LaurentSeries.powerSeriesPart_coeff, add_comm
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
m : ℕ
hm : n + (↑s : ℤ) = (↑m : ℤ)
d : ℕ
hd : D + (↑s : ℤ) = (↑d : ℤ)
linarith :
  d ≤ m →
    -1 + (n + 1 - D) + -(n + (↑s : ℤ) - (↑m : ℤ)) + (D + (↑s : ℤ) - (↑d : ℤ)) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑m : ℤ) = 0
⊢ m < d

Tactic:
linarith
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
m : ℕ
hm : n + (↑s : ℤ) = (↑m : ℤ)
d : ℕ
hd : D + (↑s : ℤ) = (↑d : ℤ)
apply :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))
⊢ Eq (α := K) ((PowerSeries.coeff m : (a : K⟦X⟧) → K) f.powerSeriesPart : K) (0 : K)

Tactic:
apply (intValuation_le_iff_coeff_lt_eq_zero K F).mp _ m (by linarith)

Premises used: LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, Iff.mp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
m : ℕ
hm : n + (↑s : ℤ) = (↑m : ℤ)
d : ℕ
hd : D + (↑s : ℤ) = (↑d : ℤ)
rw :
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ)) (exp (-(↑s : ℤ)))
      (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ)) ≤
    exp (-(↑s : ℤ)) * exp (-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) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))

Tactic:
rw [hF, ofPowerSeries_powerSeriesPart f, hs, neg_neg, ← hd, neg_add_rev, exp_add, map_mul,
      ← ofPowerSeries_X_pow s, PowerSeries.coe_pow, valuation_X_pow K s]

Premises used: neg_add_rev, WithZero.exp_add, HahnSeries.ofPowerSeries_X_pow, LaurentSeries.ofPowerSeries_powerSeriesPart, neg_neg, map_mul, PowerSeries.coe_pow, LaurentSeries.valuation_X_pow
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
m : ℕ
hm : n + (↑s : ℤ) = (↑m : ℤ)
d : ℕ
hd : D + (↑s : ℤ) = (↑d : ℤ)
⊢ HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ)) (exp (-(↑s : ℤ)))
      (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ)) ≤
    exp (-(↑s : ℤ)) * exp (-D)

Tactic:
gcongr
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
neg : ∀ (s : ℕ) (hs : -HahnSeries.order f = -(↑s : ℤ)), f.coeff n = 0
⊢ f.coeff n = 0

Tactic:
obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (Int.neg_nonpos_of_nonneg (le_of_lt ord_nonpos))

Premises used: le_of_lt, Int.neg_nonpos_of_nonneg, Int.exists_eq_neg_ofNat
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
⊢ 0 ≤ n - (↑s : ℤ)

Tactic:
grind
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
neg : ∀ (m : ℕ) (hm : n - (↑s : ℤ) = (↑m : ℤ)), f.coeff n = 0
⊢ f.coeff n = 0

Tactic:
obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (a := n - s) (by grind)

Premises used: Int.eq_ofNat_of_zero_le
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
m : ℕ
hm : n - (↑s : ℤ) = (↑m : ℤ)
⊢ 0 ≤ D - (↑s : ℤ)

Tactic:
lia
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
m : ℕ
hm : n - (↑s : ℤ) = (↑m : ℤ)
neg : ∀ (d : ℕ) (hd : D - (↑s : ℤ) = (↑d : ℤ)), f.coeff n = 0
⊢ f.coeff n = 0

Tactic:
obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le (a := D - s) (by lia)

Premises used: Int.eq_ofNat_of_zero_le
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
m : ℕ
hm : n - (↑s : ℤ) = (↑m : ℤ)
d : ℕ
hd : D - (↑s : ℤ) = (↑d : ℤ)
neg : Eq (α := K) ((PowerSeries.coeff m : (a : K⟦X⟧) → K) f.powerSeriesPart : K) (0 : K)
⊢ f.coeff n = 0

Tactic:
rw [sub_eq_iff_eq_add.mp hm, add_comm, ← neg_neg (s : ℤ), ← hs, neg_neg,
      ← powerSeriesPart_coeff]

Premises used: LaurentSeries.powerSeriesPart_coeff, neg_neg, Nat.cast, add_comm, sub_eq_iff_eq_add, Iff.mp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
m : ℕ
hm : n - (↑s : ℤ) = (↑m : ℤ)
d : ℕ
hd : D - (↑s : ℤ) = (↑d : ℤ)
linarith :
  d ≤ m →
    -1 + (n + 1 - D) + -(n - (↑s : ℤ) - (↑m : ℤ)) + (D - (↑s : ℤ) - (↑d : ℤ)) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑m : ℤ) = 0
⊢ m < d

Tactic:
linarith
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
m : ℕ
hm : n - (↑s : ℤ) = (↑m : ℤ)
d : ℕ
hd : D - (↑s : ℤ) = (↑d : ℤ)
apply :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))
⊢ Eq (α := K) ((PowerSeries.coeff m : (a : K⟦X⟧) → K) f.powerSeriesPart : K) (0 : K)

Tactic:
apply (intValuation_le_iff_coeff_lt_eq_zero K F).mp _ m (by linarith)

Premises used: LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero, Iff.mp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
m : ℕ
hm : n - (↑s : ℤ) = (↑m : ℤ)
d : ℕ
hd : D - (↑s : ℤ) = (↑d : ℤ)
rw :
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ)) (exp (↑s : ℤ))
      (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ)) ≤
    exp (↑s : ℤ) * exp (-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) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))

Tactic:
rw [hF, ofPowerSeries_powerSeriesPart f, map_mul, ← hd, hs, neg_sub, sub_eq_add_neg,
      exp_add, valuation_single_zpow, neg_neg]

Premises used: WithZero.exp_add, neg_sub, LaurentSeries.valuation_single_zpow, LaurentSeries.ofPowerSeries_powerSeriesPart, sub_eq_add_neg, neg_neg, map_mul
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
m : ℕ
hm : n - (↑s : ℤ) = (↑m : ℤ)
d : ℕ
hd : D - (↑s : ℤ) = (↑d : ℤ)
⊢ HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ)) (exp (↑s : ℤ))
      (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ)) ≤
    exp (↑s : ℤ) * exp (-D)

Tactic:
gcongr
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D) ↔
    ∀ n < D, f.coeff n = 0

Tactic:
⟨fun hnD n hn => coeff_zero_of_lt_valuation K hnD hn, fun h_val_f => ?_⟩

Premises used: LaurentSeries.coeff_zero_of_lt_valuation, Iff.intro
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
refine :
  ∀ (h_val_f : ∀ n < D, f.coeff n = 0),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D) ↔
    ∀ n < D, f.coeff n = 0

Tactic:
refine ⟨fun hnD n hn => coeff_zero_of_lt_valuation K hnD hn, fun h_val_f => ?_⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
pos :
  ∀ (ord_nonpos : HahnSeries.order f ≤ 0),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
neg :
  ∀ (ord_nonpos : 0 < HahnSeries.order f),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)

Tactic:
by_cases! ord_nonpos : f.order ≤ 0

Premises used: HahnSeries.order
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
pos :
  ∀ (s : ℕ) (hs : HahnSeries.order f = -(↑s : ℤ)),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)

Tactic:
obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat ord_nonpos

Premises used: Int.exists_eq_neg_ofNat
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
pos :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart) ≤
    exp (-(D + (↑s : ℤ)))
pos₁ : LT.lt (α := WithZero (Multiplicative ℤ)) 0 (exp (↑s : ℤ))
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)

Tactic:
rw [← f.single_order_mul_powerSeriesPart, hs, map_mul, valuation_single_zpow, neg_neg, mul_comm,
      ← le_mul_inv_iff₀, exp_neg, ← mul_inv, ← exp_add, ← exp_neg]

Premises used: WithZero.exp_add, LaurentSeries.valuation_single_zpow, LaurentSeries.single_order_mul_powerSeriesPart, mul_inv, neg_neg, map_mul, le_mul_inv_iff₀, mul_comm, WithZero.exp_neg
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
pos :
  ∀ (hDs : D + (↑s : ℤ) ≤ 0),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart) ≤
      exp (-(D + (↑s : ℤ)))
neg :
  ∀ (hDs : 0 < D + (↑s : ℤ)),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart) ≤
      exp (-(D + (↑s : ℤ)))
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart) ≤
    exp (-(D + (↑s : ℤ)))

Tactic:
by_cases! hDs : D + s ≤ 0
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
hDs : D + (↑s : ℤ) ≤ 0
pos : 1 ≤ exp (-(D + (↑s : ℤ)))
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart) ≤
    exp (-(D + (↑s : ℤ)))

Tactic:
apply le_trans ((PowerSeries.idealX K).valuation_le_one F)

Premises used: PowerSeries.idealX, IsDedekindDomain.HeightOneSpectrum.valuation_le_one, le_trans
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
hDs : D + (↑s : ℤ) ≤ 0
pos : log 1 ≤ -(D + (↑s : ℤ))
pos₁ : D + (↑s : ℤ) ≤ -log 1
pos₂ : D + (↑s : ℤ) ≤ -0
pos₃ pos₄ pos₅ pos₆ : D + (↑s : ℤ) ≤ 0
⊢ 1 ≤ exp (-(D + (↑s : ℤ)))

Tactic:
rwa [← log_le_iff_le_exp one_ne_zero, le_neg, log_one, neg_zero]

Premises used: WithZero.log_le_iff_le_exp, WithZero.log_one, le_neg, one_ne_zero, neg_zero
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
hDs : 0 < D + (↑s : ℤ)
neg :
  ∀ (d : ℕ) (hd : D + (↑s : ℤ) = (↑d : ℤ)),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart) ≤
      exp (-(D + (↑s : ℤ)))
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart) ≤
    exp (-(D + (↑s : ℤ)))

Tactic:
obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le hDs.le

Premises used: LT.lt.le, Int.eq_ofNat_of_zero_le
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
hDs : 0 < D + (↑s : ℤ)
d : ℕ
hd : D + (↑s : ℤ) = (↑d : ℤ)
neg :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart) ≤
    exp (-(D + (↑s : ℤ)))

Tactic:
rw [hd]
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
hDs : 0 < D + (↑s : ℤ)
d : ℕ
hd : D + (↑s : ℤ) = (↑d : ℤ)
neg : ∀ n < d, Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) F : K) (0 : K)
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))

Tactic:
apply (intValuation_le_iff_coeff_lt_eq_zero K F).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
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
hDs : 0 < D + (↑s : ℤ)
d : ℕ
hd : D + (↑s : ℤ) = (↑d : ℤ)
n : ℕ
hn : n < d
neg : f.coeff (HAdd.hAdd (α := ℤ) (-(↑s : ℤ)) (↑n : ℤ)) = 0
⊢ Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) F : K) (0 : K)

Tactic:
rw [powerSeriesPart_coeff f n, hs]

Premises used: LaurentSeries.powerSeriesPart_coeff
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
hDs : 0 < D + (↑s : ℤ)
d : ℕ
hd : D + (↑s : ℤ) = (↑d : ℤ)
n : ℕ
hn : n < d
neg : HAdd.hAdd (α := ℤ) (-(↑s : ℤ)) (↑n : ℤ) < D
⊢ f.coeff (HAdd.hAdd (α := ℤ) (-(↑s : ℤ)) (↑n : ℤ)) = 0

Tactic:
apply h_val_f
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
hDs : 0 < D + (↑s : ℤ)
d : ℕ
hd : D + (↑s : ℤ) = (↑d : ℤ)
n : ℕ
hn : n < d
⊢ HAdd.hAdd (α := ℤ) (-(↑s : ℤ)) (↑n : ℤ) < D

Tactic:
lia
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) 0 (exp (↑s : ℤ))

Tactic:
simp [ne_eq, zero_lt_iff]

Premises used: ne_eq, zero_lt_iff
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
neg :
  ∀ (s : ℕ) (hs : -HahnSeries.order f = -(↑s : ℤ)),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)

Tactic:
obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat <| neg_nonpos_of_nonneg ord_nonpos.le

Premises used: LT.lt.le, neg_nonpos_of_nonneg, Int.exists_eq_neg_ofNat
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
⊢ HahnSeries.order f = (↑s : ℤ)

Tactic:
rw [neg_inj] at hs

Premises used: neg_inj
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
F : K⟦X⟧ := f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = (↑s : ℤ)
neg :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart) ≤
    exp (-D + (↑s : ℤ))
neg₁ : LT.lt (α := WithZero (Multiplicative ℤ)) 0 (exp (-(↑s : ℤ)))
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)

Tactic:
rw [← f.single_order_mul_powerSeriesPart, hs, map_mul, valuation_single_zpow, mul_comm,
      ← le_mul_inv_iff₀, ← exp_neg, ← exp_add, neg_neg]

Premises used: WithZero.exp_add, LaurentSeries.valuation_single_zpow, LaurentSeries.single_order_mul_powerSeriesPart, neg_neg, map_mul, le_mul_inv_iff₀, mul_comm, WithZero.exp_neg