-- Mathlib/RingTheory/LaurentSeries.lean
theorem exists_ratFunc_val_lt (f : K⸨X⸩) (γ : ℤₘ₀ˣ) :
    ∃ Q : RatFunc K, Valued.v (f - Q) < γ

Proof state:
case neg
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : ¬HahnSeries.order f < 0
⊢ ∃ Q, Valued.v (f - ↑Q) < ↑γ

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

Result:
case neg.intro
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : ¬HahnSeries.order f < 0
s : ℕ
hs : -HahnSeries.order f = -↑s
⊢ ∃ Q, Valued.v (f - ↑Q) < ↑γ

Proof state:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : ℤₘ₀ˣ := Units.mk0 ↑(Multiplicative.ofAdd (HahnSeries.order f)) ⋯
hη : η = Units.mk0 ↑(Multiplicative.ofAdd (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
F_mul : (ofPowerSeries ℤ K) f.powerSeriesPart = (single (-HahnSeries.order f)) 1 * f
⊢ Valued.v (f - ↑(RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

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

Result:
case h.intro
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : ℤₘ₀ˣ := Units.mk0 ↑(Multiplicative.ofAdd (HahnSeries.order f)) ⋯
hη : η = Units.mk0 ↑(Multiplicative.ofAdd (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
F_mul : (ofPowerSeries ℤ K) f.powerSeriesPart = (single (-HahnSeries.order f)) 1 * f
s : ℕ
hs : HahnSeries.order f = -↑s
⊢ Valued.v (f - ↑(RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

Proof state:
case pos
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
⊢ ∃ Q, Valued.v (f - ↑Q) < ↑γ

Tactic:
set η : ℤₘ₀ˣ := Units.mk0 (Multiplicative.ofAdd f.order : Multiplicative ℤ) coe_ne_zero
  with hη

Result:
case pos
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : ℤₘ₀ˣ := Units.mk0 ↑(Multiplicative.ofAdd (HahnSeries.order f)) ⋯
hη : η = Units.mk0 ↑(Multiplicative.ofAdd (HahnSeries.order f)) ⋯
⊢ ∃ Q, Valued.v (f - ↑Q) < ↑γ

Proof state:
case neg.intro
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : ¬HahnSeries.order f < 0
s : ℕ
hs : -HahnSeries.order f = -↑s
⊢ ∃ Q, Valued.v (f - ↑Q) < ↑γ

Tactic:
obtain ⟨P, hP⟩ := exists_Polynomial_intValuation_lt (PowerSeries.X ^ s * F) γ

Result:
case neg.intro.intro
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : ¬HahnSeries.order f < 0
s : ℕ
hs : -HahnSeries.order f = -↑s
P : K[X]
hP : (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * F - ↑P) < ↑γ
⊢ ∃ Q, Valued.v (f - ↑Q) < ↑γ

Proof state:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : ¬HahnSeries.order f < 0
s : ℕ
hs : -HahnSeries.order f = -↑s
P : K[X]
hP : (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * F - ↑P) < ↑γ
⊢ Valued.v (f - ↑↑P) < ↑γ

Tactic:
rw [← X_order_mul_powerSeriesPart (neg_inj.1 hs).symm, ← RatFunc.coe_coe,
  ← PowerSeries.coe_sub, ← coe_algebraMap, adicValued_apply, valuation_of_algebraMap]

Result:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : ¬HahnSeries.order f < 0
s : ℕ
hs : -HahnSeries.order f = -↑s
P : K[X]
hP : (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * F - ↑P) < ↑γ
⊢ (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * f.powerSeriesPart - ↑P) < ↑γ

Proof state:
case neg.intro.intro
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : ¬HahnSeries.order f < 0
s : ℕ
hs : -HahnSeries.order f = -↑s
P : K[X]
hP : (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * F - ↑P) < ↑γ
⊢ ∃ Q, Valued.v (f - ↑Q) < ↑γ

Tactic:
use P

Result:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : ¬HahnSeries.order f < 0
s : ℕ
hs : -HahnSeries.order f = -↑s
P : K[X]
hP : (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * F - ↑P) < ↑γ
⊢ Valued.v (f - ↑↑P) < ↑γ

Proof state:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : ¬HahnSeries.order f < 0
s : ℕ
hs : -HahnSeries.order f = -↑s
P : K[X]
hP : (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * F - ↑P) < ↑γ
⊢ (PowerSeries.idealX K).intValuation (PowerSeries.X ^ s * f.powerSeriesPart - ↑P) < ↑γ

Tactic:
exact hP

Result:
no goals

Proof state:
case h.intro
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : ℤₘ₀ˣ := Units.mk0 ↑(Multiplicative.ofAdd (HahnSeries.order f)) ⋯
hη : η = Units.mk0 ↑(Multiplicative.ofAdd (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
⊢ Valued.v (f - ↑(RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

Tactic:
rw [hs, ← F_mul, PowerSeries.coe_pow, PowerSeries.coe_X, RatFunc.coe_mul, zpow_neg,
  zpow_natCast, inv_eq_one_div (RatFunc.X ^ s), RatFunc.coe_div, RatFunc.coe_pow,
  RatFunc.coe_X, RatFunc.coe_one, ← inv_eq_one_div, ← mul_sub, map_mul, map_inv₀,
  ← PowerSeries.coe_X, valuation_X_pow, ← hs, ← RatFunc.coe_coe, ← PowerSeries.coe_sub,
  ← coe_algebraMap, adicValued_apply, valuation_of_algebraMap,
  ← Units.val_mk0 (a := ((Multiplicative.ofAdd f.order : Multiplicative ℤ) : ℤₘ₀)), ← hη]

Result:
case h.intro
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : ℤₘ₀ˣ := Units.mk0 ↑(Multiplicative.ofAdd (HahnSeries.order f)) ⋯
hη : η = Units.mk0 ↑(Multiplicative.ofAdd (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
⊢ (↑η)⁻¹ * (PowerSeries.idealX K).intValuation (F - ↑P) < ↑γ

Proof state:
case h.intro.h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : ℤₘ₀ˣ := Units.mk0 ↑(Multiplicative.ofAdd (HahnSeries.order f)) ⋯
hη : η = Units.mk0 ↑(Multiplicative.ofAdd (HahnSeries.order f)) ⋯
P : K[X]
hP : (PowerSeries.idealX K).intValuation (F - ↑P) < ↑(η * γ)
s : ℕ
F_mul : ((ofPowerSeries ℤ K) (PowerSeries.X ^ s))⁻¹ * (ofPowerSeries ℤ K) F = f
hs : HahnSeries.order f = -↑s
⊢ (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η * ↑γ

Tactic:
rwa [← Units.val_mul]

Result:
no goals