awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
d : ℕ
hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)
this :
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧))) ≤
    HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))
h : LT.lt (α := ℤ) 0 1
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
rw [← WithZero.coe_one, coe_lt_coe, ofAdd_neg, Right.inv_lt_one_iff, ← ofAdd_zero,
      Multiplicative.ofAdd_lt]

Premises used: Multiplicative.ofAdd_lt, ofAdd_zero, Right.inv_lt_one_iff, WithZero.coe_lt_coe, WithZero.coe_one, ofAdd_neg
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
d : ℕ
hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)
this :
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧))) ≤
    HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))
⊢ LT.lt (α := ℤ) 0 1

Tactic:
Int.zero_lt_one

Premises used: Int.zero_lt_one
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
η : (WithZero (Multiplicative ℤ))ˣ
h_neg : LE.le (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (0 : ℤ)
d : ℕ
hd : Eq (α := ℤ) ((Multiplicative.toAdd : (a : Multiplicative ℤ) → ℤ) (unzero ⋯) : ℤ) (-(↑d : ℤ) : ℤ)
this :
  ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) (F - (↑((trunc (d + 1) : (a : K⟦X⟧) → K[X]) F) : K⟦X⟧))) ≤
    HMul.hMul (β := WithZero (Multiplicative ℤ)) (↑η : WithZero (Multiplicative ℤ))
      ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (-1)) : WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))
⊢ LT.lt (α := ℤ) 0 1

Tactic:
exact Int.zero_lt_one

Premises used: Int.zero_lt_one
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
⊢ let F := f.powerSeriesPart;
  F = f.powerSeriesPart

Tactic:
set F := f.powerSeriesPart with hF

Premises used: LaurentSeries.powerSeriesPart
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
γ : (WithZero (Multiplicative ℤ))ˣ
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
pos :
  ∀ (ord_nonpos : HahnSeries.order f < 0),
    ∃ (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 ℤ))
neg :
  ∀ (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 ℤ))
⊢ ∃ (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:
by_cases! ord_nonpos : f.order < 0

Premises used: HahnSeries.order
-- Module: Mathlib.RingTheory.LaurentSeries
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
⊢ let η := Units.mk0 (exp (HahnSeries.order f)) ⋯;
  η = Units.mk0 (exp (HahnSeries.order f)) ⋯

Tactic:
set η : ℤᵐ⁰ˣ := Units.mk0 (exp f.order) coe_ne_zero
      with hη

Premises used: WithZero.coe_ne_zero, HahnSeries.order, Units.mk0, WithZero.exp
-- Module: Mathlib.RingTheory.LaurentSeries
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)) ⋯
pos :
  ∀ (P : K[X])
    (hP :
      ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          (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 ℤ))
⊢ ∃ (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 F (η * γ)

Premises used: HMul.hMul, LaurentSeries.exists_Polynomial_intValuation_lt
-- Module: Mathlib.RingTheory.LaurentSeries
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 ℤ))
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⸩)
            (HPow.hPow (α := K⟮X⟯) RatFunc.X (HahnSeries.order f) * (↑P : K⟮X⟯)) :
          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:
use RatFunc.X ^ f.order * (P : K⟮X⟯)

Premises used: HahnSeries.order, RatFunc.X, RatFunc.coePolynomial
-- Module: Mathlib.RingTheory.LaurentSeries
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 ℤ))
⊢ ((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
-- Module: Mathlib.RingTheory.LaurentSeries
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
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 ℤ))
⊢ ((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)

Premises used: le_of_lt, Int.exists_eq_neg_ofNat
-- Module: Mathlib.RingTheory.LaurentSeries
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 ℤ))
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⟦ℤ⟧)
⊢ ((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

Premises used: HahnSeries.ofPowerSeries_X_pow, inv_mul_eq_iff_eq_mul₀, neg_neg
-- Module: Mathlib.RingTheory.LaurentSeries
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 : ℤ)
⊢ Eq.{u_2 + 1} (α := K⸨X⸩) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) 1) 1

Tactic:
algebraMap.coe_one

Premises used: algebraMap.coe_one, Set.Mem
-- Module: Mathlib.RingTheory.LaurentSeries
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 : ℤ)
⊢ Eq.{u_2 + 1} (α := K⸨X⸩) ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) 1) 1

Tactic:
exact algebraMap.coe_one

Premises used: algebraMap.coe_one
-- Module: Mathlib.RingTheory.LaurentSeries
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 : ℤ)
⊢ 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
-- Module: Mathlib.RingTheory.LaurentSeries
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
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 ℤ))
⊢ ((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 [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]

Premises used: zpow_natCast, RatFunc.X, RatFunc.coe_X, map_pow, inv_eq_one_div, map_mul, map_div₀, HPow.hPow, zpow_neg, PowerSeries.coe_X, PowerSeries.coe_pow
-- Module: Mathlib.RingTheory.LaurentSeries
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
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 ℤ))
⊢ ((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:
simp only [map_one]

Premises used: map_one
-- Module: Mathlib.RingTheory.LaurentSeries
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
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 ℤ))
⊢ ((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:
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η]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, mul_sub, LaurentSeries.coe_algebraMap, RatFunc.coe_coe, PowerSeries.coe_sub, map_inv₀, inv_eq_one_div, IsDedekindDomain.HeightOneSpectrum.adicValued_apply, WithZero.exp_ne_zero, map_mul, PowerSeries.coe_X, Units.val_mk0, LaurentSeries.valuation_X_pow
-- Module: Mathlib.RingTheory.LaurentSeries
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
h :
  ((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
        (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (F - (↑P : K⟦X⟧)) <
    (↑η : WithZero (Multiplicative ℤ)) * (↑γ : WithZero (Multiplicative ℤ))
⊢ 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:
apply inv_mul_lt_of_lt_mul₀

Premises used: inv_mul_lt_of_lt_mul₀