awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℤ)
⊢ 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 ℤ))
have neg : ∀ n < d, Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) F : K) (0 : K)
Tactic: apply (intValuation_le_iff_coeff_lt_eq_zero K F).mpr
-- 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 : ℤ)
n : ℕ
hn : n < d
⊢ Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) F : K) (0 : K)
have neg : f.coeff (HAdd.hAdd (α := ℤ) (-(↑s : ℤ)) (↑n : ℤ)) = 0
Tactic: rw [powerSeriesPart_coeff f n, hs]
-- 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 : ℤ)
n : ℕ
hn : n < d
⊢ f.coeff (HAdd.hAdd (α := ℤ) (-(↑s : ℤ)) (↑n : ℤ)) = 0
have neg : HAdd.hAdd (α := ℤ) (-(↑s : ℤ)) (↑n : ℤ) < D
Tactic: apply 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
ord_nonpos : 0 < HahnSeries.order f
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
have neg : ∀ (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 <| neg_nonpos_of_nonneg ord_nonpos.le
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
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 : ℤ)
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
have hs₁ : HahnSeries.order f = (↑s : ℤ)
Tactic: rw [neg_inj] at hs
Cleared hypotheses: hs
-- 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 : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = (↑s : ℤ)
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
have 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 : ℤ))
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]
-- 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 : 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 : ℤ))
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
have neg₁ : LT.lt (α := WithZero (Multiplicative ℤ)) 0 (exp (-(↑s : ℤ)))
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]
-- 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 : 0 < HahnSeries.order f
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 : 0 < HahnSeries.order f
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 : 0 < HahnSeries.order f
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 : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = (↑s : ℤ)
hDs : D - (↑s : ℤ) ≤ 0
⊢ 1 ≤ exp (-D + (↑s : ℤ))
have pos : 0 ≤ -D + (↑s : ℤ)
Tactic: rw [← log_le_iff_le_exp one_ne_zero, log_one]
-- 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 : 0 < HahnSeries.order f
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 : 0 < HahnSeries.order f
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 [← neg_neg (-D + ↑s), ← sub_eq_neg_add, neg_sub, hd]
-- 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 : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = (↑s : ℤ)
hDs : 0 < D - (↑s : ℤ)
d : ℕ
hd : D - (↑s : ℤ) = (↑d : ℤ)
⊢ 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 ℤ))
have neg : ∀ n < d, Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) F : K) (0 : K)
Tactic: apply (intValuation_le_iff_coeff_lt_eq_zero K F).mpr
-- 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 : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = (↑s : ℤ)
hDs : 0 < D - (↑s : ℤ)
d : ℕ
hd : D - (↑s : ℤ) = (↑d : ℤ)
n : ℕ
hn : n < d
⊢ Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) F : K) (0 : K)
have neg : f.coeff (HAdd.hAdd (α := ℤ) (↑s : ℤ) (↑n : ℤ)) = 0
Tactic: rw [powerSeriesPart_coeff f n, hs]
-- 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 : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = (↑s : ℤ)
hDs : 0 < D - (↑s : ℤ)
d : ℕ
hd : D - (↑s : ℤ) = (↑d : ℤ)
n : ℕ
hn : n < d
⊢ f.coeff (HAdd.hAdd (α := ℤ) (↑s : ℤ) (↑n : ℤ)) = 0
have neg : HAdd.hAdd (α := ℤ) (↑s : ℤ) (↑n : ℤ) < D
Tactic: apply h_val_f (s + n)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
D : WithZero (Multiplicative ℤ)
hD : D ≠ 0
f : K⸨X⸩
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ D ↔
    ∀ n < -D.log, f.coeff n = 0
have zero : ∀ (hD : Ne (α := WithZero (Multiplicative ℤ)) 0 0),
  LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ)) ↔
    ∀ n < -log 0, f.coeff n = 0
Tactic: cases D
Cleared hypotheses: D, hD
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
D : WithZero (Multiplicative ℤ)
hD : D ≠ 0
f : K⸨X⸩
zero :
  ∀ (hD : Ne (α := WithZero (Multiplicative ℤ)) 0 0),
    LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
          WithZero (Multiplicative ℤ))
        (0 : WithZero (Multiplicative ℤ)) ↔
      ∀ n < -log 0, f.coeff n = 0
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ D ↔
    ∀ n < -D.log, f.coeff n = 0
have coe : ∀ (a : Multiplicative ℤ) (hD : (↑a : WithZero (Multiplicative ℤ)) ≠ 0),
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤
      (↑a : WithZero (Multiplicative ℤ)) ↔
    ∀ n < -(↑a : WithZero (Multiplicative ℤ)).log, f.coeff n = 0
Tactic: cases D
Cleared hypotheses: D, hD
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
D : Multiplicative ℤ
hD : (↑D : WithZero (Multiplicative ℤ)) ≠ 0
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤
      (↑D : WithZero (Multiplicative ℤ)) ↔
    ∀ n < -(↑D : WithZero (Multiplicative ℤ)).log, f.coeff n = 0
have coe : ∀ (a : ℤ)
  (hD :
    Ne (α := WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) a) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))),
  LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) a) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ)) ↔
    ∀ n < -log (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) a) : WithZero (Multiplicative ℤ)), f.coeff n = 0
Tactic: cases D
Cleared hypotheses: D, hD
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
D : ℤ
hD :
  Ne (α := WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ)) ↔
    ∀ n < -log (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)), f.coeff n = 0
have coe : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp D ↔
  ∀ n < -(exp D).log, f.coeff n = 0
Tactic: rw [← exp, ← neg_neg D, valuation_le_iff_coeff_lt_eq_zero, log_exp, neg_neg]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
D : ℤ
hD :
  Ne (α := WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
coe :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp D ↔
    ∀ n < -(exp D).log, f.coeff n = 0
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ)) ↔
    ∀ n < -log (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)), f.coeff n = 0
have coe₁ : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (- -D) ↔
  ∀ n < -(exp (- -D)).log, f.coeff n = 0
Tactic: rw [← exp, ← neg_neg D, valuation_le_iff_coeff_lt_eq_zero, log_exp, neg_neg]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
D : ℤ
hD :
  Ne (α := WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
coe :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp D ↔
    ∀ n < -(exp D).log, f.coeff n = 0
coe₁ :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤
      exp (- -D) ↔
    ∀ n < -(exp (- -D)).log, f.coeff n = 0
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ)) ↔
    ∀ n < -log (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)), f.coeff n = 0
have coe₂ : (∀ n < -D, f.coeff n = 0) ↔ ∀ n < -(exp (- -D)).log, f.coeff n = 0
Tactic: rw [← exp, ← neg_neg D, valuation_le_iff_coeff_lt_eq_zero, log_exp, neg_neg]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
D : ℤ
hD :
  Ne (α := WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
coe :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp D ↔
    ∀ n < -(exp D).log, f.coeff n = 0
coe₁ :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤
      exp (- -D) ↔
    ∀ n < -(exp (- -D)).log, f.coeff n = 0
coe₂ : (∀ n < -D, f.coeff n = 0) ↔ ∀ n < -(exp (- -D)).log, f.coeff n = 0
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ)) ↔
    ∀ n < -log (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)), f.coeff n = 0
have coe₃ : (∀ n < -D, f.coeff n = 0) ↔ ∀ n < - - -D, f.coeff n = 0
Tactic: rw [← exp, ← neg_neg D, valuation_le_iff_coeff_lt_eq_zero, log_exp, neg_neg]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
D : ℤ
hD :
  Ne (α := WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))
coe :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp D ↔
    ∀ n < -(exp D).log, f.coeff n = 0
coe₁ :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤
      exp (- -D) ↔
    ∀ n < -(exp (- -D)).log, f.coeff n = 0
coe₂ : (∀ n < -D, f.coeff n = 0) ↔ ∀ n < -(exp (- -D)).log, f.coeff n = 0
coe₃ : (∀ n < -D, f.coeff n = 0) ↔ ∀ n < - - -D, f.coeff n = 0
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ)) ↔
    ∀ n < -log (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) D) : WithZero (Multiplicative ℤ)), f.coeff n = 0
have coe₄ : (∀ n < -D, f.coeff n = 0) ↔ ∀ n < -D, f.coeff n = 0
Tactic: rw [← exp, ← neg_neg D, valuation_le_iff_coeff_lt_eq_zero, log_exp, neg_neg]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
d n : ℤ
f g : K⸨X⸩
H :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (g - f) ≤
    exp (-d)
⊢ n < d → g.coeff n = f.coeff n
have pos : ∀ (triv : g = f), n < d → g.coeff n = f.coeff n
Tactic: by_cases triv : g = f
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
d n : ℤ
f g : K⸨X⸩
H :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (g - f) ≤
    exp (-d)
pos : ∀ (triv : g = f), n < d → g.coeff n = f.coeff n
⊢ n < d → g.coeff n = f.coeff n
have neg : ∀ (triv : ¬g = f), n < d → g.coeff n = f.coeff n
Tactic: by_cases triv : g = f
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
d n : ℤ
f g : K⸨X⸩
H :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (g - f) ≤
    exp (-d)
triv : g = f
h : n < d
⊢ g.coeff n = f.coeff n
have rw : f.coeff n = f.coeff n
Tactic: rw [triv]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
d n : ℤ
f g : K⸨X⸩
H :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (g - f) ≤
    exp (-d)
triv : ¬g = f
hn : n < d
⊢ g.coeff n = f.coeff n
have neg : g.coeff n - f.coeff n = 0
Tactic: apply eq_of_sub_eq_zero
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
d n : ℤ
f g : K⸨X⸩
H :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (g - f) ≤
    exp (-d)
triv : ¬g = f
hn : n < d
⊢ g.coeff n - f.coeff n = 0
have neg : (g - f).coeff n = 0
Tactic: rw [← HahnSeries.coeff_sub]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    ∃ (F : K⟦X⟧), ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F = f
have rw : (∀ n < 0, f.coeff n = 0) ↔ ∃ (F : K⟦X⟧), ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F = f
Tactic: rw [valuation_le_iff_coeff_lt_log_eq_zero _ one_ne_zero, log_one, neg_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
⊢ (∀ n < 0, f.coeff n = 0) ↔ ∃ (F : K⟦X⟧), ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F = f
have refine_1 : ∀ (h : ∀ n < 0, f.coeff n = 0),
  ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)) = f
Tactic: refine ⟨fun h => ⟨PowerSeries.mk fun n => f.coeff n, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
refine_1 :
  ∀ (h : ∀ n < 0, f.coeff n = 0),
    ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)) = f
⊢ (∀ n < 0, f.coeff n = 0) ↔ ∃ (F : K⟦X⟧), ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F = f
have refine_2 : (∃ (F : K⟦X⟧), ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F = f) → ∀ n < 0, f.coeff n = 0
Tactic: refine ⟨fun h => ⟨PowerSeries.mk fun n => f.coeff n, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
⊢ ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)) = f
have refine_1 : ∀ (a : ℕ),
  HahnSeries.coeff
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)))
      (Int.ofNat a) =
    f.coeff (Int.ofNat a)
Tactic: ext (_ | n)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
refine_1 :
  ∀ (a : ℕ),
    HahnSeries.coeff
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)))
        (Int.ofNat a) =
      f.coeff (Int.ofNat a)
⊢ ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)) = f
have refine_1₁ : ∀ (n : ℕ),
  HahnSeries.coeff
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)))
      (Int.negSucc n) =
    f.coeff (Int.negSucc n)
Tactic: ext (_ | n)