awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
d : ℕ
f : K⟦X⟧
⊢ 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 ℤ)) ↔
    ∀ n < d, Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) f : K) (0 : K)
have this : HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f ↔ ∀ n < d, Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) f : K) (0 : K)
Tactic: have : PowerSeries.X ^ d ∣ f ↔ ∀ n : ℕ, n < d → (PowerSeries.coeff n) f = 0 :=
    ⟨PowerSeries.X_pow_dvd_iff.mp, PowerSeries.X_pow_dvd_iff.mpr⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
d : ℕ
f : K⟦X⟧
this :
  HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f ↔
    ∀ n < d, Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) f : 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) :
        WithZero (Multiplicative ℤ))
      (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    ∀ n < d, Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) f : K) (0 : K)
have rw : LE.le (α := WithZero (Multiplicative ℤ))
    (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        f :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)) ↔
  HPow.hPow (α := Ideal K⟦X⟧) (Ideal.span {PowerSeries.X}) d ∣ Ideal.span {f}
Tactic: rw [← this, ← LaurentSeries.coe_algebraMap, valuation_def, valuation_of_algebraMap,
    ← Ideal.span_singleton_dvd_span_singleton_iff_dvd, ← Ideal.span_singleton_pow]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ f.coeff n = 0
have pos : ∀ (h_n_ord : n < HahnSeries.order f), f.coeff n = 0
Tactic: by_cases! h_n_ord : n < f.order
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
pos : ∀ (h_n_ord : n < HahnSeries.order f), f.coeff n = 0
⊢ f.coeff n = 0
have neg : ∀ (h_n_ord : HahnSeries.order f ≤ n), f.coeff n = 0
Tactic: by_cases! h_n_ord : n < f.order
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
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.coeff n = 0
have hF : let F := f.powerSeriesPart;
F = f.powerSeriesPart
Tactic: set F := powerSeriesPart f with hF
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ f.coeff n = 0
have pos : ∀ (ord_nonpos : HahnSeries.order f ≤ 0), f.coeff n = 0
Tactic: by_cases! ord_nonpos : f.order ≤ 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
pos : ∀ (ord_nonpos : HahnSeries.order f ≤ 0), f.coeff n = 0
⊢ f.coeff n = 0
have neg : ∀ (ord_nonpos : 0 < HahnSeries.order f), f.coeff n = 0
Tactic: by_cases! ord_nonpos : f.order ≤ 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ f.coeff n = 0
have pos : ∀ (s : ℕ) (hs : HahnSeries.order f = -(↑s : ℤ)), f.coeff n = 0
Tactic: obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat ord_nonpos
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ f.coeff n = 0
have pos : ∀ (m : ℕ) (hm : n + (↑s : ℤ) = (↑m : ℤ)), f.coeff n = 0
Tactic: obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (neg_le_iff_add_nonneg.mp (hs ▸ h_n_ord))
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ f.coeff n = 0
have pos : ∀ (d : ℕ) (hd : D + (↑s : ℤ) = (↑d : ℤ)), f.coeff n = 0
Tactic: obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le (a := D + s) (by lia)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ f.coeff n = 0
have pos : Eq (α := K) ((PowerSeries.coeff m : (a : K⟦X⟧) → K) f.powerSeriesPart : K) (0 : K)
Tactic: rw [eq_add_neg_of_add_eq hm, add_comm, ← hs, ← powerSeriesPart_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ m < d
have linarith : d ≤ m →
  -1 + (n + 1 - D) + -(n + (↑s : ℤ) - (↑m : ℤ)) + (D + (↑s : ℤ) - (↑d : ℤ)) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑m : ℤ) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ Eq (α := K) ((PowerSeries.coeff m : (a : K⟦X⟧) → K) f.powerSeriesPart : K) (0 : K)
have 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 ℤ))
Tactic: apply (intValuation_le_iff_coeff_lt_eq_zero K F).mp _ m (by linarith)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ 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 ℤ))
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ f.coeff n = 0
have neg : ∀ (s : ℕ) (hs : -HahnSeries.order f = -(↑s : ℤ)), f.coeff n = 0
Tactic: obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (Int.neg_nonpos_of_nonneg (le_of_lt ord_nonpos))
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ f.coeff n = 0
have neg : ∀ (m : ℕ) (hm : n - (↑s : ℤ) = (↑m : ℤ)), f.coeff n = 0
Tactic: obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (a := n - s) (by grind)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ f.coeff n = 0
have neg : ∀ (d : ℕ) (hd : D - (↑s : ℤ) = (↑d : ℤ)), f.coeff n = 0
Tactic: obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le (a := D - s) (by lia)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ f.coeff n = 0
have neg : Eq (α := K) ((PowerSeries.coeff m : (a : K⟦X⟧) → K) f.powerSeriesPart : K) (0 : K)
Tactic: rw [sub_eq_iff_eq_add.mp hm, add_comm, ← neg_neg (s : ℤ), ← hs, neg_neg,
      ← powerSeriesPart_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ m < d
have linarith : d ≤ m →
  -1 + (n + 1 - D) + -(n - (↑s : ℤ) - (↑m : ℤ)) + (D - (↑s : ℤ) - (↑d : ℤ)) + HSub.hSub (α := ℤ) (↑d : ℤ) (↑m : ℤ) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ Eq (α := K) ((PowerSeries.coeff m : (a : K⟦X⟧) → K) f.powerSeriesPart : K) (0 : K)
have 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 ℤ))
Tactic: apply (intValuation_le_iff_coeff_lt_eq_zero K F).mp _ m (by linarith)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ 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 ℤ))
have 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)
Tactic: rw [hF, ofPowerSeries_powerSeriesPart f, map_mul, ← hd, hs, neg_sub, sub_eq_add_neg,
      exp_add, valuation_single_zpow, neg_neg]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
have 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)
Tactic: refine ⟨fun hnD n hn => coeff_zero_of_lt_valuation K hnD hn, fun h_val_f => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
have pos : ∀ (ord_nonpos : HahnSeries.order f ≤ 0),
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
Tactic: by_cases! ord_nonpos : f.order ≤ 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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)
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
have neg : ∀ (ord_nonpos : 0 < HahnSeries.order f),
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
Tactic: by_cases! ord_nonpos : f.order ≤ 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
have pos : ∀ (s : ℕ) (hs : HahnSeries.order f = -(↑s : ℤ)),
  ((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
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
have 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 : ℤ)))
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]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)))
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
have pos₁ : LT.lt (α := WithZero (Multiplicative ℤ)) 0 (exp (↑s : ℤ))
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]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ ((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 : ℤ)))
have 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 : ℤ)))
Tactic: by_cases! hDs : D + s ≤ 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)))
⊢ ((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 : ℤ)))
have 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 : ℤ)))
Tactic: by_cases! hDs : D + s ≤ 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ ((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 : ℤ)))
have pos : 1 ≤ exp (-(D + (↑s : ℤ)))
Tactic: apply le_trans ((PowerSeries.idealX K).valuation_le_one F)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ 1 ≤ exp (-(D + (↑s : ℤ)))
have pos : log 1 ≤ -(D + (↑s : ℤ))
Tactic: rwa [← log_le_iff_le_exp one_ne_zero, le_neg, log_one, neg_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ))
⊢ 1 ≤ exp (-(D + (↑s : ℤ)))
have pos₁ : D + (↑s : ℤ) ≤ -log 1
Tactic: rwa [← log_le_iff_le_exp one_ne_zero, le_neg, log_one, neg_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ 1 ≤ exp (-(D + (↑s : ℤ)))
have pos₂ : D + (↑s : ℤ) ≤ -0
Tactic: rwa [← log_le_iff_le_exp one_ne_zero, le_neg, log_one, neg_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ ((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 : ℤ)))
have 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 : ℤ)))
Tactic: obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le hDs.le
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 : ℤ)
⊢ ((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 : ℤ)))
have 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 ℤ))
Tactic: rw [hd]