-- Mathlib/RingTheory/LaurentSeries.lean
theorem valuation_le_iff_coeff_lt_eq_zero {D : ℤ} {f : K⸨X⸩} :
    Valued.v f ≤ ↑(Multiplicative.ofAdd (-D : ℤ)) ↔ ∀ n : ℤ, n < D → f.coeff n = 0

Proof state:
case pos.intro
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 f ≤ ↑(Multiplicative.ofAdd (-D))

Tactic:
rw [← f.single_order_mul_powerSeriesPart, hs, map_mul, valuation_single_zpow, neg_neg, mul_comm,
  ← le_mul_inv_iff₀, ofAdd_neg, WithZero.coe_inv, ← mul_inv, ← WithZero.coe_mul, ← ofAdd_add,
  ← WithZero.coe_inv, ← ofAdd_neg]

Result:
case pos.intro
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 ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ ↑(Multiplicative.ofAdd (-(D + ↑s)))

case pos.intro
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
⊢ 0 < ↑(Multiplicative.ofAdd ↑s)

Proof state:
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 f ≤ ↑(Multiplicative.ofAdd (-D))

Tactic:
by_cases ord_nonpos : f.order ≤ 0

Result:
case pos
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 f ≤ ↑(Multiplicative.ofAdd (-D))

case neg
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 f ≤ ↑(Multiplicative.ofAdd (-D))

Proof state:
case pos
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 f ≤ ↑(Multiplicative.ofAdd (-D))

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

Result:
case pos.intro
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 f ≤ ↑(Multiplicative.ofAdd (-D))

Proof state:
case neg.intro
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
d : ℕ
hd : D + ↑s = ↑d
n : ℕ
hn : n < d
⊢ f.coeff (-↑s + ↑n) = 0

Tactic:
apply h_val_f

Result:
case neg.intro.a
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
d : ℕ
hd : D + ↑s = ↑d
n : ℕ
hn : n < d
⊢ -↑s + ↑n < D

Proof state:
case neg.intro
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
d : ℕ
hd : D + ↑s = ↑d
n : ℕ
hn : n < d
⊢ (PowerSeries.coeff K n) F = 0

Tactic:
rw [powerSeriesPart_coeff f n, hs]

Result:
case neg.intro
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
d : ℕ
hd : D + ↑s = ↑d
n : ℕ
hn : n < d
⊢ f.coeff (-↑s + ↑n) = 0

Proof state:
case neg.intro
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 ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ ↑(Multiplicative.ofAdd (-D + ↑s))

Tactic:
by_cases hDs : D - s ≤ 0

Result:
case pos
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 ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ ↑(Multiplicative.ofAdd (-D + ↑s))

case neg
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 ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ ↑(Multiplicative.ofAdd (-D + ↑s))

Proof state:
case neg
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 ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ ↑(Multiplicative.ofAdd (-D + ↑s))

Tactic:
obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le (le_of_lt <| not_le.mp hDs)

Result:
case neg.intro
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
d : ℕ
hd : D - ↑s = ↑d
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ ↑(Multiplicative.ofAdd (-D + ↑s))

Proof state:
case neg.intro
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 f ≤ ↑(Multiplicative.ofAdd (-D))

Tactic:
rw [neg_inj] at hs

Result:
case neg.intro
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 f ≤ ↑(Multiplicative.ofAdd (-D))

Proof state:
case pos
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 ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ ↑(Multiplicative.ofAdd (-(D + ↑s)))

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

Result:
case pos
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 ≤ ↑(Multiplicative.ofAdd (-(D + ↑s)))

Proof state:
case neg
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 f ≤ ↑(Multiplicative.ofAdd (-D))

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

Result:
case neg.intro
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 f ≤ ↑(Multiplicative.ofAdd (-D))

Proof state:
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
⊢ Valued.v f ≤ ↑(Multiplicative.ofAdd (-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 => ?_⟩

Result:
K : Type u_2
inst✝ : Field K
D : ℤ
f : K⸨X⸩
h_val_f : ∀ n < D, f.coeff n = 0
⊢ Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))

Proof state:
case neg.intro
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
d : ℕ
hd : D - ↑s = ↑d
n : ℕ
hn : n < d
⊢ (PowerSeries.coeff K n) F = 0

Tactic:
rw [powerSeriesPart_coeff f n, hs]

Result:
case neg.intro
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
d : ℕ
hd : D - ↑s = ↑d
n : ℕ
hn : n < d
⊢ f.coeff (↑s + ↑n) = 0