awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℤ)
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 : 0 < HahnSeries.order f
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 : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = (↑s : ℤ)
hDs : D - (↑s : ℤ) ≤ 0
pos : 0 ≤ -D + (↑s : ℤ)
⊢ 1 ≤ exp (-D + (↑s : ℤ))

Tactic:
rw [← log_le_iff_le_exp one_ne_zero, log_one]

Premises used: WithZero.log_le_iff_le_exp, WithZero.log_one, one_ne_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 : 0 < HahnSeries.order f
s : ℕ
hs : HahnSeries.order f = (↑s : ℤ)
hDs : D - (↑s : ℤ) ≤ 0
⊢ 0 ≤ -D + (↑s : ℤ)

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 : 0 < HahnSeries.order f
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 : 0 < HahnSeries.order f
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 [← neg_neg (-D + ↑s), ← sub_eq_neg_add, neg_sub, hd]

Premises used: neg_sub, sub_eq_neg_add, neg_neg, HAdd.hAdd, Neg.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 : 0 < HahnSeries.order f
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 : 0 < HahnSeries.order f
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 : 0 < HahnSeries.order f
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 (s + n)

Premises used: Nat.cast, HAdd.hAdd
-- 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 : ℤ)
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 : 0 < HahnSeries.order f
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 : 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
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
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ D ↔
    ∀ n < -D.log, f.coeff n = 0

Tactic:
cases D
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
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:
simp_all
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
D : Multiplicative ℤ
hD : (↑D : WithZero (Multiplicative ℤ)) ≠ 0
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
⊢ ((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

Tactic:
cases D
-- Module: Mathlib.RingTheory.LaurentSeries
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
coe₄ 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

Tactic:
rw [← exp, ← neg_neg D, valuation_le_iff_coeff_lt_eq_zero, log_exp, neg_neg]

Premises used: LaurentSeries.valuation_le_iff_coeff_lt_eq_zero, neg_neg, WithZero.log_exp, WithZero.exp
-- Module: Mathlib.RingTheory.LaurentSeries
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
neg : ∀ (triv : ¬g = f), n < d → g.coeff n = f.coeff n
⊢ n < d → g.coeff n = f.coeff n

Tactic:
by_cases triv : g = f
-- Module: Mathlib.RingTheory.LaurentSeries
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
rw rw₁ : f.coeff n = f.coeff n
⊢ g.coeff n = f.coeff n

Tactic:
rw [triv]
-- Module: Mathlib.RingTheory.LaurentSeries
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
⊢ n < d → g.coeff n = f.coeff n

Tactic:
exact fun _ => by rw [triv]
-- Module: Mathlib.RingTheory.LaurentSeries
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
neg : g.coeff n - f.coeff n = 0
⊢ g.coeff n = f.coeff n

Tactic:
apply eq_of_sub_eq_zero

Premises used: eq_of_sub_eq_zero
-- Module: Mathlib.RingTheory.LaurentSeries
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
neg : (g - f).coeff n = 0
⊢ g.coeff n - f.coeff n = 0

Tactic:
rw [← HahnSeries.coeff_sub]

Premises used: HahnSeries.coeff_sub
-- Module: Mathlib.RingTheory.LaurentSeries
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 - f).coeff n = 0

Tactic:
apply coeff_zero_of_lt_valuation K H hn

Premises used: LaurentSeries.coeff_zero_of_lt_valuation
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
rw : (∀ n < 0, f.coeff n = 0) ↔ ∃ (F : K⟦X⟧), ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F = f
⊢ 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

Tactic:
rw [valuation_le_iff_coeff_lt_log_eq_zero _ one_ne_zero, log_one, neg_zero]

Premises used: WithZero.log_one, LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero, one_ne_zero, neg_zero
-- Module: Mathlib.RingTheory.LaurentSeries
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

Tactic:
⟨fun h => ⟨PowerSeries.mk fun n => f.coeff n, ?_⟩, ?_⟩

Premises used: Nat.cast, Iff.intro, Exists.intro, HahnSeries.coeff, PowerSeries.mk
-- Module: Mathlib.RingTheory.LaurentSeries
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
refine_2 : (∃ (F : K⟦X⟧), ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F = f) → ∀ n < 0, f.coeff n = 0
⊢ (∀ n < 0, f.coeff n = 0) ↔ ∃ (F : K⟦X⟧), ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F = f

Tactic:
refine ⟨fun h => ⟨PowerSeries.mk fun n => f.coeff n, ?_⟩, ?_⟩
-- Module: Mathlib.RingTheory.LaurentSeries
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)
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)
⊢ ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)) = f

Tactic:
ext (_ | n)
-- Module: Mathlib.RingTheory.LaurentSeries
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)
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)
⊢ ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)) = f

Tactic:
on_goal 1 => ext (_ | n)
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
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:
simp only [Int.ofNat_eq_natCast, coeff_coe_powerSeries, coeff_mk]

Premises used: Int.ofNat_eq_natCast, PowerSeries.coeff_mk, LaurentSeries.coeff_coe_powerSeries
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
refine_1 :
  Eq.{u_2 + 1} (α := K)
    (HahnSeries.coeff
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)))
      (Int.negSucc n))
    0
⊢ 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:
simp only [h (Int.negSucc n) (Int.negSucc_lt_zero n)]

Premises used: Int.negSucc_lt_zero, Int.negSucc
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
refine_1 :
  Eq.{u_2 + 1} (α := K)
    (HahnSeries.coeff
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)))
      (Int.negSucc n))
    0
⊢ 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:
on_goal 1 => simp only [h (Int.negSucc n) (Int.negSucc_lt_zero n)]

Premises used: Int.negSucc_lt_zero, Int.negSucc
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
refine_2 :
  ∀ (F : K⟦X⟧),
    ∀ n < 0, Eq.{u_2 + 1} (α := K) (HahnSeries.coeff (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) n) 0
⊢ (∃ (F : K⟦X⟧), ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F = f) → ∀ n < 0, f.coeff n = 0

Tactic:
on_goal 2 => rintro ⟨F, rfl⟩ _ _

Premises used: rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
refine_1 :
  Int.negSucc n ∉
    Set.range (ι := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
            { toFun := (⇑(Nat.castAddMonoidHom ℤ) : (a : ℕ) → ℤ), inj' := ⋯ } ⋯) :
        (a : ℕ) → ℤ)
⊢ Eq.{u_2 + 1} (α := K)
    (HahnSeries.coeff
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)))
      (Int.negSucc n))
    0

Tactic:
apply HahnSeries.embDomain_notin_range

Premises used: HahnSeries.embDomain_notin_range
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
refine_1 : ∀ (x : ℕ), ¬False
⊢ Int.negSucc n ∉
    Set.range (ι := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
            { toFun := (⇑(Nat.castAddMonoidHom ℤ) : (a : ℕ) → ℤ), inj' := ⋯ } ⋯) :
        (a : ℕ) → ℤ)

Tactic:
simp only [Nat.coe_castAddMonoidHom, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk,
      Set.mem_range, not_exists, reduceCtorEq]

Premises used: reduceCtorEq, Set.mem_range, not_exists, Nat.coe_castAddMonoidHom, Function.Embedding.coeFn_mk, RelEmbedding.coe_mk
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
n : ℤ
h : n < 0
refine_2 :
  n ∉
    Set.range (ι := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
            { toFun := (⇑(Nat.castAddMonoidHom ℤ) : (a : ℕ) → ℤ), inj' := ⋯ } ⋯) :
        (a : ℕ) → ℤ)
⊢ Eq.{u_2 + 1} (α := K) (HahnSeries.coeff (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) n) 0

Tactic:
apply HahnSeries.embDomain_notin_range

Premises used: HahnSeries.embDomain_notin_range
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
n : ℤ
h : n < 0
refine_2 : ∀ (x : ℕ), ¬(↑x : ℤ) = n
⊢ n ∉
    Set.range (ι := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
            { toFun := (⇑(Nat.castAddMonoidHom ℤ) : (a : ℕ) → ℤ), inj' := ⋯ } ⋯) :
        (a : ℕ) → ℤ)

Tactic:
simp only [Nat.coe_castAddMonoidHom, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk,
      Set.mem_range, not_exists, reduceCtorEq]

Premises used: reduceCtorEq, Set.mem_range, not_exists, Nat.coe_castAddMonoidHom, Function.Embedding.coeFn_mk, RelEmbedding.coe_mk
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n x : ℕ
⊢ ¬False

Tactic:
simp only [not_false_eq_true]

Premises used: not_false_eq_true
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
n : ℤ
h : n < 0
x : ℕ
⊢ ¬(↑x : ℤ) = n

Tactic:
lia
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n : WithZero (Multiplicative ℤ)
pos :
  ∀ (hn0 : n = 0),
    ∃ (a : K⸨X⸩),
      ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a = n
neg :
  ∀ (hn0 : ¬n = 0),
    ∃ (a : K⸨X⸩),
      ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a = n
⊢ ∃ (a : K⸨X⸩),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a = n

Tactic:
by_cases hn0 : n = 0
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n : WithZero (Multiplicative ℤ)
hn0 : n = 0
h : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) 0 = n
⊢ ∃ (a : K⸨X⸩),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a = n

Tactic:
use 0
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n : WithZero (Multiplicative ℤ)
hn0 : n = 0
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) 0 = n

Tactic:
simp [hn0]
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
h :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      ((single (-n.log) : (a : K) → K⟦ℤ⟧) 1) =
    n
⊢ ∃ (a : K⸨X⸩),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a = n

Tactic:
use ((HahnSeries.single (-WithZero.log n)) 1)

Premises used: HahnSeries.single, WithZero.log, OfNat.ofNat, DFunLike.coe, Neg.neg
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      ((single (-n.log) : (a : K) → K⟦ℤ⟧) 1) =
    n

Tactic:
simp [LaurentSeries.valuation_single_zpow, exp_log hn0]

Premises used: LaurentSeries.valuation_single_zpow, WithZero.exp_log
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
uK : UniformSpace K
d : ℤ
⊢ UniformContinuous (β := K) fun (f : K⸨X⸩) ↦ f.coeff d

Tactic:
uniformContinuous_iff_eventually.mpr fun S hS ↦ eventually_iff_exists_mem.mpr ?_

Premises used: Iff.mpr, uniformContinuous_iff_eventually, Filter.eventually_iff_exists_mem
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
uK : UniformSpace K
d : ℤ
refine :
  ∀ (S : Set (K × K)) (hS : S ∈ uniformity K),
    ∃ (v : Set (K⸨X⸩ × K⸨X⸩)),
      Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) v ∧ ∀ y ∈ v, (y.1.coeff d, y.2.coeff d) ∈ S
⊢ UniformContinuous (β := K) fun (f : K⸨X⸩) ↦ f.coeff d

Tactic:
refine uniformContinuous_iff_eventually.mpr fun S hS ↦ eventually_iff_exists_mem.mpr ?_

Premises used: Iff.mpr, uniformContinuous_iff_eventually, Filter.eventually_iff_exists_mem