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

Proof state:
case neg.intro.intro.intro
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
m : ℕ
hm : n - ↑s = ↑m
d : ℕ
hd : D - ↑s = ↑d
⊢ (PowerSeries.coeff K m) f.powerSeriesPart = 0

Tactic:
apply (intValuation_le_iff_coeff_lt_eq_zero K F).mp _ m (by linarith)

Result:
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
m : ℕ
hm : n - ↑s = ↑m
d : ℕ
hd : D - ↑s = ↑d
⊢ Valued.v ((ofPowerSeries ℤ K) F) ≤ ↑(Multiplicative.ofAdd (-↑d))

Proof state:
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
m : ℕ
hm : n - ↑s = ↑m
d : ℕ
hd : D - ↑s = ↑d
⊢ Valued.v ((ofPowerSeries ℤ K) F) ≤ ↑(Multiplicative.ofAdd (-↑d))

Tactic:
rwa [hF, ofPowerSeries_powerSeriesPart f, map_mul, ← hd, hs, neg_sub, sub_eq_add_neg,
  ofAdd_add, valuation_single_zpow, neg_neg, WithZero.coe_mul,
  mul_le_mul_left (by simp only [ne_eq, WithZero.coe_ne_zero, not_false_iff, zero_lt_iff])]

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
⊢ f.coeff n = 0

Tactic:
by_cases h_n_ord : n < f.order

Result:
case pos
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : n < HahnSeries.order f
⊢ f.coeff n = 0

case neg
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : ¬n < HahnSeries.order f
⊢ f.coeff n = 0

Proof state:
case pos.intro.intro.intro
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
d : ℕ
hd : D + ↑s = ↑d
⊢ f.coeff n = 0

Tactic:
rw [eq_add_neg_of_add_eq hm, add_comm, ← hs, ← powerSeriesPart_coeff]

Result:
case pos.intro.intro.intro
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
d : ℕ
hd : D + ↑s = ↑d
⊢ (PowerSeries.coeff K m) f.powerSeriesPart = 0

Proof state:
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
m : ℕ
hm : n - ↑s = ↑m
d : ℕ
hd : D - ↑s = ↑d
⊢ m < ?m.356526

Tactic:
linarith

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
m : ℕ
hm : n - ↑s = ↑m
d : ℕ
hd : D - ↑s = ↑d
⊢ 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.intro
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ f.coeff n = 0

Tactic:
obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (neg_le_iff_add_nonneg.mp (hs ▸ h_n_ord))

Result:
case pos.intro.intro
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
⊢ f.coeff n = 0

Proof state:
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
m : ℕ
hm : n - ↑s = ↑m
⊢ 0 ≤ D - ↑s

Tactic:
omega

Result:
no goals

Proof state:
case pos
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : n < HahnSeries.order f
⊢ f.coeff n = 0

Tactic:
exact coeff_eq_zero_of_lt_order h_n_ord

Result:
no goals

Proof state:
case pos.intro.intro.intro
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
d : ℕ
hd : D + ↑s = ↑d
⊢ (PowerSeries.coeff K m) f.powerSeriesPart = 0

Tactic:
apply (intValuation_le_iff_coeff_lt_eq_zero K F).mp _ m (by linarith)

Result:
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
d : ℕ
hd : D + ↑s = ↑d
⊢ Valued.v ((ofPowerSeries ℤ K) F) ≤ ↑(Multiplicative.ofAdd (-↑d))

Proof state:
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f ≤ 0
s : ℕ
hs : HahnSeries.order f = -↑s
m : ℕ
hm : n + ↑s = ↑m
⊢ 0 ≤ D + ↑s

Tactic:
omega

Result:
no goals

Proof state:
case neg
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
⊢ f.coeff n = 0

Tactic:
obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (Int.neg_nonpos_of_nonneg (le_of_lt ord_nonpos))

Result:
case neg.intro
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
⊢ f.coeff n = 0

Proof state:
case neg.intro.intro
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
m : ℕ
hm : n - ↑s = ↑m
⊢ f.coeff n = 0

Tactic:
obtain ⟨d, hd⟩ := Int.eq_ofNat_of_zero_le (a := D - s) (by omega)

Result:
case neg.intro.intro.intro
K : Type u_2
inst✝ : Field K
n D : ℤ
f : K⸨X⸩
H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 < HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -↑s
m : ℕ
hm : n - ↑s = ↑m
d : ℕ
hd : D - ↑s = ↑d
⊢ f.coeff n = 0