-- Mathlib/RingTheory/LaurentSeries.lean
theorem exists_ratFunc_val_lt (f : K⸨X⸩) (γ : ℤₘ₀ˣ) :
    ∃ Q : RatFunc K, 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) < ↑(η * γ)
⊢ Valued.v (f - ↑(RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

Tactic:
have F_mul := f.ofPowerSeries_powerSeriesPart

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
η : ℤₘ₀ˣ := 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)) < ↑γ

Proof state:
case pos.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) < ↑(η * γ)
⊢ ∃ Q, Valued.v (f - ↑Q) < ↑γ

Tactic:
use RatFunc.X ^ f.order * (P : RatFunc K)

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
η : ℤₘ₀ˣ := 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) < ↑(η * γ)
⊢ Valued.v (f - ↑(RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

Proof state:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
⊢ ∃ Q, Valued.v (f - ↑Q) < ↑γ

Tactic:
set F := f.powerSeriesPart with hF

Result:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
γ : ℤₘ₀ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
⊢ ∃ Q, Valued.v (f - ↑Q) < ↑γ

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
η : ℤₘ₀ˣ := Units.mk0 ↑(Multiplicative.ofAdd (HahnSeries.order f)) ⋯
hη : η = Units.mk0 ↑(Multiplicative.ofAdd (HahnSeries.order f)) ⋯
⊢ ∃ Q, Valued.v (f - ↑Q) < ↑γ

Tactic:
obtain ⟨P, hP⟩ := exists_Polynomial_intValuation_lt F (η * γ)

Result:
case pos.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) < ↑(η * γ)
⊢ ∃ Q, Valued.v (f - ↑Q) < ↑γ

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) < ↑(η * γ)
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)) < ↑γ

Tactic:
rw [← hF, hs, neg_neg, ← ofPowerSeries_X_pow s, ← inv_mul_eq_iff_eq_mul₀] at F_mul

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
⊢ Valued.v (f - ↑(RatFunc.X ^ HahnSeries.order f * ↑P)) < ↑γ

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) F = (ofPowerSeries ℤ K) (PowerSeries.X ^ s) * f
hs : HahnSeries.order f = -↑s
⊢ (ofPowerSeries ℤ K) (PowerSeries.X ^ s) ≠ 0

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) F = (ofPowerSeries ℤ K) (PowerSeries.X ^ s) * f
hs : HahnSeries.order f = -↑s
⊢ (ofPowerSeries ℤ K) (PowerSeries.X ^ s) ≠ 0

Tactic:
simp only [PowerSeries.coe_pow, pow_ne_zero, PowerSeries.coe_X, ne_eq,
  single_eq_zero_iff, one_ne_zero, not_false_iff]

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
⊢ (↑η)⁻¹ * (PowerSeries.idealX K).intValuation (F - ↑P) < ↑γ

Tactic:
apply inv_mul_lt_of_lt_mul₀

Result:
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) < ↑η * ↑γ

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

Tactic:
by_cases ord_nonpos : f.order < 0

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
⊢ ∃ Q, Valued.v (f - ↑Q) < ↑γ

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