awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑P : K⟦X⟧)) <
    (↑(η * γ) : WithZero (Multiplicative ℤ))
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (HSub.hSub (β := K⸨X⸩) f
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩)
            (HPow.hPow (α := K⟮X⟯) RatFunc.X (HahnSeries.order f) * (↑P : K⟮X⟯)) :
          K⸨X⸩)) <
    (↑γ : WithZero (Multiplicative ℤ))
have F_mul : ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart =
  (single (-HahnSeries.order f) : (a : K) → K⟦ℤ⟧) 1 * f
Tactic: have F_mul := f.ofPowerSeries_powerSeriesPart
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑P : K⟦X⟧)) <
    (↑(η * γ) : WithZero (Multiplicative ℤ))
F_mul :
  ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart =
    (single (-HahnSeries.order f) : (a : K) → K⟦ℤ⟧) 1 * f
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (HSub.hSub (β := K⸨X⸩) f
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩)
            (HPow.hPow (α := K⟮X⟯) RatFunc.X (HahnSeries.order f) * (↑P : K⟮X⟯)) :
          K⸨X⸩)) <
    (↑γ : WithZero (Multiplicative ℤ))
have h : ∀ (s : ℕ) (hs : HahnSeries.order f = -(↑s : ℤ)),
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (HSub.hSub (β := K⸨X⸩) f
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩)
            (HPow.hPow (α := K⟮X⟯) RatFunc.X (HahnSeries.order f) * (↑P : K⟮X⟯)) :
          K⸨X⸩)) <
    (↑γ : WithZero (Multiplicative ℤ))
Tactic: obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (le_of_lt ord_nonpos)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑P : K⟦X⟧)) <
    (↑(η * γ) : WithZero (Multiplicative ℤ))
F_mul :
  ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart =
    (single (-HahnSeries.order f) : (a : K) → K⟦ℤ⟧) 1 * f
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (HSub.hSub (β := K⸨X⸩) f
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩)
            (HPow.hPow (α := K⟮X⟯) RatFunc.X (HahnSeries.order f) * (↑P : K⟮X⟯)) :
          K⸨X⸩)) <
    (↑γ : WithZero (Multiplicative ℤ))
have h : ∀ (s : ℕ)
  (F_mul :
    HMul.hMul (α := K⟦ℤ⟧) (β := K⟦ℤ⟧)
        ((((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s))⁻¹ : K⟦ℤ⟧)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧) =
      f)
  (hs : HahnSeries.order f = -(↑s : ℤ)),
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (HSub.hSub (β := K⸨X⸩) f
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩)
            (HPow.hPow (α := K⟮X⟯) RatFunc.X (HahnSeries.order f) * (↑P : K⟮X⟯)) :
          K⸨X⸩)) <
    (↑γ : WithZero (Multiplicative ℤ))
Tactic: rw [← hF, hs, neg_neg, ← ofPowerSeries_X_pow s, ← inv_mul_eq_iff_eq_mul₀] at F_mul
Cleared hypotheses: F_mul, s, hs
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑P : K⟦X⟧)) <
    (↑(η * γ) : WithZero (Multiplicative ℤ))
F_mul :
  ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f.powerSeriesPart =
    (single (-HahnSeries.order f) : (a : K) → K⟦ℤ⟧) 1 * f
s : ℕ
hs : HahnSeries.order f = -(↑s : ℤ)
h :
  ∀ (s : ℕ)
    (F_mul :
      HMul.hMul (α := K⟦ℤ⟧) (β := K⟦ℤ⟧)
          ((((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s))⁻¹ : K⟦ℤ⟧)
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧) =
        f)
    (hs : HahnSeries.order f = -(↑s : ℤ)),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f
          ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩)
              (HPow.hPow (α := K⟮X⟯) RatFunc.X (HahnSeries.order f) * (↑P : K⟮X⟯)) :
            K⸨X⸩)) <
      (↑γ : WithZero (Multiplicative ℤ))
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (HSub.hSub (β := K⸨X⸩) f
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩)
            (HPow.hPow (α := K⟮X⟯) RatFunc.X (HahnSeries.order f) * (↑P : K⟮X⟯)) :
          K⸨X⸩)) <
    (↑γ : WithZero (Multiplicative ℤ))
have h₁ : ∀ (s : ℕ)
  (F_mul :
    ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F =
      HMul.hMul (α := K⟦ℤ⟧)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s) : K⟦ℤ⟧) f)
  (hs : HahnSeries.order f = -(↑s : ℤ)),
  Ne (α := K⟦ℤ⟧)
    (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s) : K⟦ℤ⟧)
    (0 : K⟦ℤ⟧)
Tactic: rw [← hF, hs, neg_neg, ← ofPowerSeries_X_pow s, ← inv_mul_eq_iff_eq_mul₀] at F_mul
Cleared hypotheses: F_mul, s, hs
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑P : K⟦X⟧)) <
    (↑(η * γ) : WithZero (Multiplicative ℤ))
s : ℕ
F_mul :
  HMul.hMul (α := K⟦ℤ⟧) (β := K⟦ℤ⟧)
      ((((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s))⁻¹ : K⟦ℤ⟧)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧) =
    f
hs : HahnSeries.order f = -(↑s : ℤ)
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (HSub.hSub (β := K⸨X⸩) f
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩)
            (HPow.hPow (α := K⟮X⟯) RatFunc.X (HahnSeries.order f) * (↑P : K⟮X⟯)) :
          K⸨X⸩)) <
    (↑γ : WithZero (Multiplicative ℤ))
have this : Eq.{u_2 + 1} (α := K⸨X⸩) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) 1) 1
Tactic: have : (algebraMap K⟮X⟯ K⸨X⸩) 1 = 1 := by exact algebraMap.coe_one
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑P : K⟦X⟧)) <
    (↑(η * γ) : WithZero (Multiplicative ℤ))
s : ℕ
F_mul :
  HMul.hMul (α := K⟦ℤ⟧) (β := K⟦ℤ⟧)
      ((((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s))⁻¹ : K⟦ℤ⟧)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧) =
    f
hs : HahnSeries.order f = -(↑s : ℤ)
this : Eq.{u_2 + 1} (α := K⸨X⸩) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) 1) 1
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (HSub.hSub (β := K⸨X⸩) f
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩)
            (HPow.hPow (α := K⟮X⟯) RatFunc.X (HahnSeries.order f) * (↑P : K⟮X⟯)) :
          K⸨X⸩)) <
    (↑γ : WithZero (Multiplicative ℤ))
have h : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
    (HMul.hMul (β := K⟦ℤ⟧) (HPow.hPow (α := K⟦ℤ⟧) ((single 1 : (a : K) → K⟦ℤ⟧) 1) s)⁻¹
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧) -
      HMul.hMul (β := K⸨X⸩)
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) 1 / HPow.hPow (α := K⸨X⸩) ((single 1 : (a : K) → K⟦ℤ⟧) 1) s)
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) (↑P : K⟮X⟯) : K⸨X⸩)) <
  (↑γ : WithZero (Multiplicative ℤ))
Tactic: rw [hs, ← F_mul, PowerSeries.coe_pow, PowerSeries.coe_X, map_mul, zpow_neg,
        zpow_natCast, inv_eq_one_div (RatFunc.X ^ s), map_div₀, map_pow,
        RatFunc.coe_X]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑P : K⟦X⟧)) <
    (↑(η * γ) : WithZero (Multiplicative ℤ))
s : ℕ
F_mul :
  HMul.hMul (α := K⟦ℤ⟧) (β := K⟦ℤ⟧)
      ((((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s))⁻¹ : K⟦ℤ⟧)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧) =
    f
hs : HahnSeries.order f = -(↑s : ℤ)
this : Eq.{u_2 + 1} (α := K⸨X⸩) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) 1) 1
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (HMul.hMul (β := K⟦ℤ⟧) (HPow.hPow (α := K⟦ℤ⟧) ((single 1 : (a : K) → K⟦ℤ⟧) 1) s)⁻¹
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧) -
        HMul.hMul (β := K⸨X⸩)
          ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) 1 / HPow.hPow (α := K⸨X⸩) ((single 1 : (a : K) → K⟦ℤ⟧) 1) s)
          ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) (↑P : K⟮X⟯) : K⸨X⸩)) <
    (↑γ : WithZero (Multiplicative ℤ))
have h : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
    (HMul.hMul (β := K⟦ℤ⟧) (HPow.hPow (α := K⟦ℤ⟧) ((single 1 : (a : K) → K⟦ℤ⟧) 1) s)⁻¹
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧) -
      HMul.hMul (β := K⸨X⸩) (1 / HPow.hPow (α := K⸨X⸩) ((single 1 : (a : K) → K⟦ℤ⟧) 1) s)
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) (↑P : K⟮X⟯) : K⸨X⸩)) <
  (↑γ : WithZero (Multiplicative ℤ))
Tactic: simp only [map_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑P : K⟦X⟧)) <
    (↑(η * γ) : WithZero (Multiplicative ℤ))
s : ℕ
F_mul :
  HMul.hMul (α := K⟦ℤ⟧) (β := K⟦ℤ⟧)
      ((((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s))⁻¹ : K⟦ℤ⟧)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧) =
    f
hs : HahnSeries.order f = -(↑s : ℤ)
this : Eq.{u_2 + 1} (α := K⸨X⸩) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) 1) 1
⊢ ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      (HMul.hMul (β := K⟦ℤ⟧) (HPow.hPow (α := K⟦ℤ⟧) ((single 1 : (a : K) → K⟦ℤ⟧) 1) s)⁻¹
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧) -
        HMul.hMul (β := K⸨X⸩) (1 / HPow.hPow (α := K⸨X⸩) ((single 1 : (a : K) → K⟦ℤ⟧) 1) s)
          ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) (↑P : K⟮X⟯) : K⸨X⸩)) <
    (↑γ : WithZero (Multiplicative ℤ))
have h : HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))⁻¹
    (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (F - (↑P : K⟦X⟧)) :
      WithZero (Multiplicative ℤ)) <
  (↑γ : WithZero (Multiplicative ℤ))
Tactic: rw [← 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 := exp f.order) exp_ne_zero, ← hη]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : HahnSeries.order f < 0
η : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (HahnSeries.order f)) ⋯
hη : η = Units.mk0 (exp (HahnSeries.order f)) ⋯
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑P : K⟦X⟧)) <
    (↑(η * γ) : WithZero (Multiplicative ℤ))
s : ℕ
F_mul :
  HMul.hMul (α := K⟦ℤ⟧) (β := K⟦ℤ⟧)
      ((((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s))⁻¹ : K⟦ℤ⟧)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧) =
    f
hs : HahnSeries.order f = -(↑s : ℤ)
this : Eq.{u_2 + 1} (α := K⸨X⸩) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) 1) 1
⊢ HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))⁻¹
      (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          (F - (↑P : K⟦X⟧)) :
        WithZero (Multiplicative ℤ)) <
    (↑γ : WithZero (Multiplicative ℤ))
have h : ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
      (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
    (F - (↑P : K⟦X⟧)) <
  (↑η : WithZero (Multiplicative ℤ)) * (↑γ : WithZero (Multiplicative ℤ))
Tactic: apply inv_mul_lt_of_lt_mul₀
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
⊢ ∃ (Q : K⟮X⟯),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) Q : K⸨X⸩)) <
      (↑γ : WithZero (Multiplicative ℤ))
have neg : ∀ (s : ℕ) (hs : -HahnSeries.order f = -(↑s : ℤ)),
  ∃ (Q : K⟮X⟯),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) Q : K⸨X⸩)) <
      (↑γ : WithZero (Multiplicative ℤ))
Tactic: obtain ⟨s, hs⟩ := Int.exists_eq_neg_ofNat (Int.neg_nonpos_of_nonneg ord_nonpos)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
⊢ ∃ (Q : K⟮X⟯),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) Q : K⸨X⸩)) <
      (↑γ : WithZero (Multiplicative ℤ))
have neg : ∀ (P : K[X])
  (hP :
    ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := K⟦X⟧) PowerSeries.X s * F - (↑P : K⟦X⟧)) <
      (↑γ : WithZero (Multiplicative ℤ))),
  ∃ (Q : K⟮X⟯),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) Q : K⸨X⸩)) <
      (↑γ : WithZero (Multiplicative ℤ))
Tactic: obtain ⟨P, hP⟩ := exists_Polynomial_intValuation_lt (PowerSeries.X ^ s * F) γ
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
ord_nonpos : 0 ≤ HahnSeries.order f
s : ℕ
hs : -HahnSeries.order f = -(↑s : ℤ)
P : K[X]
hP :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (HPow.hPow (α := K⟦X⟧) PowerSeries.X s * F - (↑P : K⟦X⟧)) <
    (↑γ : WithZero (Multiplicative ℤ))
⊢ ∃ (Q : K⟮X⟯),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) Q : K⸨X⸩)) <
      (↑γ : WithZero (Multiplicative ℤ))
have h : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
    (HSub.hSub (β := K⸨X⸩) f ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) (↑P : K⟮X⟯) : K⸨X⸩)) <
  (↑γ : WithZero (Multiplicative ℤ))
Tactic: use P
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
⊢ DenseRange.{u_2, u_2} (X := K⸨X⸩) (α := K⟮X⟯) (⇑(algebraMap K⟮X⟯ K⸨X⸩) : (a : K⟮X⟯) → K⸨X⸩)
have rw : Eq.{u_2 + 1} (α := Set K⸨X⸩) (closure (Set.range (ι := K⟮X⟯) (⇑(algebraMap K⟮X⟯ K⸨X⸩) : (a : K⟮X⟯) → K⸨X⸩))) Set.univ
Tactic: rw [denseRange_iff_closure_range]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
⊢ Eq.{u_2 + 1} (α := Set K⸨X⸩) (closure (Set.range (ι := K⟮X⟯) (⇑(algebraMap K⟮X⟯ K⸨X⸩) : (a : K⟮X⟯) → K⸨X⸩))) Set.univ
have h : ∀ (f : K⸨X⸩),
  Membership.mem (γ := Set K⸨X⸩) (closure (Set.range (ι := K⟮X⟯) (⇑(algebraMap K⟮X⟯ K⸨X⸩) : (a : K⟮X⟯) → K⸨X⸩))) f ↔
    Membership.mem (γ := Set K⸨X⸩) Set.univ f
Tactic: ext f
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
⊢ Membership.mem (γ := Set K⸨X⸩) (closure (Set.range (ι := K⟮X⟯) (⇑(algebraMap K⟮X⟯ K⸨X⸩) : (a : K⟮X⟯) → K⸨X⸩))) f ↔
    Membership.mem (γ := Set K⸨X⸩) Set.univ f
have h : ∀ {V : Set (K⸨X⸩ × K⸨X⸩)},
  Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) V →
    SetRel.IsSymm V →
      ∃ (a : K⟮X⟯),
        Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
Tactic: simp only [UniformSpace.mem_closure_iff_symm_ball, Set.mem_univ, iff_true, Set.Nonempty,
    Set.mem_inter_iff, Set.mem_range, exists_exists_eq_and]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
hV : Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) V
h_symm : SetRel.IsSymm V
⊢ ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
have hV₁ : Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (Filter.comap (β := K⸨X⸩) (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) (nhds 0)) V
Tactic: rw [uniformity_eq_comap_neg_add_nhds_zero_swapped] at hV
Cleared hypotheses: hV, h_symm
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
hV :
  Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (Filter.comap (β := K⸨X⸩) (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) (nhds 0)) V
h_symm : SetRel.IsSymm V
⊢ ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
have h : ∀ (T : Set K⸨X⸩) (hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T)
  (hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V),
  ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
Tactic: obtain ⟨T, hT₀, hT₁⟩ := hV
Cleared hypotheses: hV
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T
hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V
⊢ ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
have h : ∀ (γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ)
  (hγ :
    {x : K⸨X⸩ |
        ((Valuation.restrict Valued.v :
                Valuation K⸨X⸩
                  (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                    (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
              (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
            x <
          (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
      T),
  ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
Tactic: obtain ⟨γ, hγ⟩ := Valued.mem_nhds_zero.mp hT₀
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SetRel.IsSymm V
T : Set K⸨X⸩
hT₀ : Membership.mem (γ := Filter K⸨X⸩) (nhds 0) T
hT₁ : (fun (x : K⸨X⸩ × K⸨X⸩) ↦ -x.2 + x.1) ⁻¹' T ⊆ V
γ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ
hγ :
  {x : K⸨X⸩ |
      ((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          x <
        (↑γ : MonoidWithZeroHom.ValueGroup₀ Valued.v)} ⊆
    T
⊢ ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
have h : ∀ (this : WithZero (Multiplicative ℤ)),
  ∃ (a : K⟮X⟯), Membership.mem (α := K⸨X⸩) (UniformSpace.ball f V) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) a : K⸨X⸩)
Tactic: have := (embedding γ.1)