-- 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
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))

Tactic:
rw [← WithZero.coe_one, ← ofAdd_zero, WithZero.coe_le_coe, Multiplicative.ofAdd_le]

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
⊢ 0 ≤ -D + ↑s

Proof state:
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

Tactic:
omega

Result:
no goals

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
⊢ Valued.v ((ofPowerSeries ℤ K) f.powerSeriesPart) ≤ ↑(Multiplicative.ofAdd (-↑d))

Tactic:
apply (intValuation_le_iff_coeff_lt_eq_zero K F).mpr

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 < d, (PowerSeries.coeff K n) F = 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
hDs : ¬D - ↑s ≤ 0
d : ℕ
hd : D - ↑s = ↑d
⊢ ∀ n < d, (PowerSeries.coeff K n) F = 0

Tactic:
intro n hn

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
⊢ (PowerSeries.coeff K n) F = 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
hDs : ¬D + ↑s ≤ 0
d : ℕ
hd : D + ↑s = ↑d
⊢ ∀ n < d, (PowerSeries.coeff K n) F = 0

Tactic:
intro n hn

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
⊢ (PowerSeries.coeff K n) F = 0

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)))