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

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.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
⊢ ↑s + ↑n < D

Tactic:
omega

Result:
no goals

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

Tactic:
let F := powerSeriesPart f

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

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 + ↑s)))

Tactic:
rw [hd]

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

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

Tactic:
simp only [ne_eq, WithZero.coe_ne_zero, not_false_iff, zero_lt_iff]

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

Tactic:
apply h_val_f (s + n)

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

Tactic:
rw [← neg_neg (-D + ↑s), ← sub_eq_neg_add, neg_sub, hd]

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

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:
rwa [← WithZero.coe_one, ← ofAdd_zero, WithZero.coe_le_coe, Multiplicative.ofAdd_le,
  Left.nonneg_neg_iff]

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
⊢ Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))

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

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

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

Tactic:
simp only [ne_eq, WithZero.coe_ne_zero, not_false_iff, zero_lt_iff]

Result:
no goals

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

Tactic:
omega

Result:
no goals