awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K⟮X⟯
refine :
  ∀ (p q : K[X]),
    q ≠ 0 →
      Eq (α := WithZero (Multiplicative ℤ))
        (((polynomialValuationX K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
              (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
            (RatFunc.mk p q) :
          WithZero (Multiplicative ℤ))
        (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
              (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) (RatFunc.mk p q)) :
          WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((polynomialValuationX K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
          (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
        P :
      WithZero (Multiplicative ℤ))
    (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
          (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) P) :
      WithZero (Multiplicative ℤ))

Tactic:
refine RatFunc.induction_on' P ?_
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K⟮X⟯
f g : K[X]
h : g ≠ 0
rw :
  ((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
        (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩)
        (IsLocalization.mk' K⟮X⟯ f
          (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) (nonZeroDivisors K[X]) x) g ⋯))) =
    HDiv.hDiv (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
            (a : K[X]) → WithZero (Multiplicative ℤ))
          f :
        WithZero (Multiplicative ℤ))
      (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
            (a : K[X]) → WithZero (Multiplicative ℤ))
          g :
        WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((polynomialValuationX K : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) :
          (a : K⟮X⟯) → WithZero (Multiplicative ℤ))
        (RatFunc.mk f g) :
      WithZero (Multiplicative ℤ))
    (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
          (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) (RatFunc.mk f g)) :
      WithZero (Multiplicative ℤ))

Tactic:
rw [Polynomial.valuation_of_mk K f h, RatFunc.mk_eq_mk' f h, Eq.comm]

Premises used: Polynomial.valuation_of_mk, RatFunc.mk_eq_mk', Eq.comm
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K⟮X⟯
f g : K[X]
h : g ≠ 0
⊢ (↑g : K⟦X⟧) ≠ 0

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K⟮X⟯
f g : K[X]
h : g ≠ 0
h₁ :
  Eq (α := K⸨X⸩)
    ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩)
      (IsLocalization.mk' K⟮X⟯ f
        (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) (nonZeroDivisors K[X]) x) g ⋯)))
    (IsLocalization.mk' K⸨X⸩ (↑f : K⟦X⟧)
      (Subtype.mk (p := fun (x : K⟦X⟧) ↦ Membership.mem (γ := Submonoid K⟦X⟧) (nonZeroDivisors K⟦X⟧) x) (↑g : K⟦X⟧) ⋯))
h₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        f :
      WithZero (Multiplicative ℤ))
    (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑f : K⟦X⟧) :
      WithZero (Multiplicative ℤ))
h₃ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        g :
      WithZero (Multiplicative ℤ))
    (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑(Subtype.mk (p := fun (x : K⟦X⟧) ↦ Membership.mem (γ := Submonoid K⟦X⟧) (nonZeroDivisors K⟦X⟧) x) (↑g : K⟦X⟧)
              ⋯) :
          K⟦X⟧) :
      WithZero (Multiplicative ℤ))
⊢ ((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
        (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
      ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩)
        (IsLocalization.mk' K⟮X⟯ f
          (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) (nonZeroDivisors K[X]) x) g ⋯))) =
    HDiv.hDiv (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
            (a : K[X]) → WithZero (Multiplicative ℤ))
          f :
        WithZero (Multiplicative ℤ))
      (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
            (a : K[X]) → WithZero (Multiplicative ℤ))
          g :
        WithZero (Multiplicative ℤ))

Tactic:
convert!
    @valuation_of_mk' K⟦X⟧ _ _ K⸨X⸩ _ _ _ (PowerSeries.idealX K) f
      ⟨g, mem_nonZeroDivisors_iff_ne_zero.2 <| (by simp [h])⟩

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_mk', PowerSeries.idealX
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K⟮X⟯
f g : K[X]
h : g ≠ 0
⊢ Eq (α := K⸨X⸩)
    ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩)
      (IsLocalization.mk' K⟮X⟯ f
        (Subtype.mk (p := fun (x : K[X]) ↦ Membership.mem (γ := Submonoid K[X]) (nonZeroDivisors K[X]) x) g ⋯)))
    (IsLocalization.mk' K⸨X⸩ (↑f : K⟦X⟧)
      (Subtype.mk (p := fun (x : K⟦X⟧) ↦ Membership.mem (γ := Submonoid K⟦X⟧) (nonZeroDivisors K⟦X⟧) x) (↑g : K⟦X⟧) ⋯))

Tactic:
simp [← IsScalarTower.algebraMap_apply K[X] K⟮X⟯ K⸨X⸩]

Premises used: Polynomial, RatFunc, LaurentSeries, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K⟮X⟯
f g : K[X]
h : g ≠ 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        f :
      WithZero (Multiplicative ℤ))
    (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑f : K⟦X⟧) :
      WithZero (Multiplicative ℤ))

Tactic:
intValuation_eq_of_coe _

Premises used: PowerSeries.intValuation_eq_of_coe
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K⟮X⟯
f g : K[X]
h : g ≠ 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        g :
      WithZero (Multiplicative ℤ))
    (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑(Subtype.mk (p := fun (x : K⟦X⟧) ↦ Membership.mem (γ := Submonoid K⟦X⟧) (nonZeroDivisors K⟦X⟧) x) (↑g : K⟦X⟧)
              ⋯) :
          K⟦X⟧) :
      WithZero (Multiplicative ℤ))

Tactic:
intValuation_eq_of_coe _

Premises used: PowerSeries.intValuation_eq_of_coe, Polynomial.coeff, Polynomial.toPowerSeries, PowerSeries.mk
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K⟮X⟯
f g : K[X]
h : g ≠ 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        f :
      WithZero (Multiplicative ℤ))
    (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑f : K⟦X⟧) :
      WithZero (Multiplicative ℤ))

Tactic:
exacts [intValuation_eq_of_coe _, intValuation_eq_of_coe _]

Premises used: PowerSeries.intValuation_eq_of_coe
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
⊢ Eq (α := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v (valuation K⸨X⸩ (PowerSeries.idealX K))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⟮X⟯
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
        ((algebraMap K⟮X⟯ K⸨X⸩ : (a : K⟮X⟯) → K⸨X⸩) f) :
      WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) f :
      WithZero (Multiplicative ℤ))

Tactic:
simp [adicValued_apply, ← valuation_eq_LaurentSeries_valuation]

Premises used: RatFunc.valuation_eq_LaurentSeries_valuation, IsDedekindDomain.HeightOneSpectrum.adicValued_apply
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
s : ℕ
rw :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₁ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
            (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₂ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
            (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) PowerSeries.X) :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₃ :
  HPow.hPow (α := WithZero (Multiplicative ℤ))
      (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          PowerSeries.X :
        WithZero (Multiplicative ℤ))
      s =
    exp (-(↑s : ℤ))
rw₄ : HPow.hPow (α := WithZero (Multiplicative ℤ)) (exp (-1)) s = exp (-(↑s : ℤ))
rw₅ : exp (HSMul.hSMul (β := ℤ) s (-1)) = exp (-(↑s : ℤ))
rw₆ : exp (-HSMul.hSMul (β := ℤ) s 1) = exp (-(↑s : ℤ))
rw₇ rw₈ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑s : ℤ))) (exp (-(↑s : ℤ)))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := K⟦ℤ⟧) (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X : K⟦ℤ⟧) s) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))

Tactic:
rw [map_pow, valuation_def, ← LaurentSeries.coe_algebraMap,
    valuation_of_algebraMap, intValuation_X, ← exp_nsmul, smul_neg, nsmul_one]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, LaurentSeries.coe_algebraMap, smul_neg, map_pow, WithZero.exp_nsmul, PowerSeries.intValuation_X, LaurentSeries.valuation_def, nsmul_one
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
s : ℤ
ofNat :
  ∀ (s : ℕ),
    ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        ((single (Int.ofNat s) : (a : K) → K⟦ℤ⟧) 1) =
      exp (-Int.ofNat s)
negSucc :
  ∀ (s : ℕ),
    ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        ((single (Int.negSucc s) : (a : K) → K⟦ℤ⟧) 1) =
      exp (-Int.negSucc s)
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single s : (a : K) → K⟦ℤ⟧) 1) =
    exp (-s)

Tactic:
obtain s | s := s
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
s : ℕ
ofNat :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        ((single (↑s : ℤ) : (a : K) → K⟦ℤ⟧) 1) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
ofNat₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (HPow.hPow (α := K⟦X⟧) PowerSeries.X s)) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
ofNat₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := K⟦ℤ⟧) (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) PowerSeries.X : K⟦ℤ⟧) s) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑s : ℤ)) : WithZero (Multiplicative ℤ))
ofNat₃ ofNat₄ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑s : ℤ))) (exp (-(↑s : ℤ)))
⊢ ((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
      ((single (Int.ofNat s) : (a : K) → K⟦ℤ⟧) 1) =
    exp (-Int.ofNat s)

Tactic:
rw [Int.ofNat_eq_natCast, ← HahnSeries.ofPowerSeries_X_pow, PowerSeries.coe_pow,
      valuation_X_pow]

Premises used: HahnSeries.ofPowerSeries_X_pow, Int.ofNat_eq_natCast, PowerSeries.coe_pow, LaurentSeries.valuation_X_pow
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n d : ℕ
f : K⟦X⟧
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))
hnd : n < d
apply : HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
⊢ Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) f : K) (0 : K)

Tactic:
apply (PowerSeries.X_pow_dvd_iff).mp _ n hnd

Premises used: Iff.mp, PowerSeries.X_pow_dvd_iff
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n d : ℕ
f : K⟦X⟧
H :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) :
      WithZero (Multiplicative ℤ))
    (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ))
hnd : n < d
rwa :
  ∀
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
            ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) f) :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₁ :
  ∀
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((valuation K⸨X⸩ (PowerSeries.idealX K) : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) :
              (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
            ((algebraMap K⟦X⟧ K⸨X⸩ : (a : K⟦X⟧) → K⸨X⸩) f) :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₂ :
  ∀
    (H :
      LE.le (α := WithZero (Multiplicative ℤ))
        (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
              (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
            f :
          WithZero (Multiplicative ℤ))
        (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)))
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₃ :
  ∀ (H : HPow.hPow (α := Ideal K⟦X⟧) (asIdeal (PowerSeries.idealX K)) d ∣ Ideal.span {f}) (hnd : n < d),
    HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₄ :
  ∀
    (H :
      HPow.hPow (α := Ideal K⟦X⟧)
          (asIdeal
            { asIdeal := Ideal.span {PowerSeries.X}, isPrime := ⋯, ne_bot := ⋯ :
              IsDedekindDomain.HeightOneSpectrum K⟦X⟧ })
          d ∣
        Ideal.span {f})
    (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₅ :
  ∀ (H : Dvd.dvd (α := Ideal K⟦X⟧) (Ideal.span {HPow.hPow (α := K⟦X⟧) PowerSeries.X d}) (Ideal.span {f})) (hnd : n < d),
    HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
rwa₆ rwa₇ rwa₈ rwa₉ :
  ∀ (H : HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f) (hnd : n < d), HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f
⊢ HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f

Tactic:
rwa [← LaurentSeries.coe_algebraMap, valuation_def, valuation_of_algebraMap,
    intValuation_le_pow_iff_dvd (PowerSeries.idealX K) f d, PowerSeries.idealX,
    Ideal.span_singleton_pow, Ideal.span_singleton_dvd_span_singleton_iff_dvd] at H

Premises used: Ideal.span_singleton_dvd_span_singleton_iff_dvd, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, LaurentSeries.coe_algebraMap, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd, PowerSeries.idealX, LaurentSeries.valuation_def, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
d : ℕ
f : K⟦X⟧
⊢ HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f ↔
    ∀ n < d, Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) f : K) (0 : K)

Tactic:
have : PowerSeries.X ^ d ∣ f ↔ ∀ n : ℕ, n < d → (PowerSeries.coeff n) f = 0 :=
    ⟨PowerSeries.X_pow_dvd_iff.mp, PowerSeries.X_pow_dvd_iff.mpr⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
d : ℕ
f : K⟦X⟧
this :
  HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f ↔
    ∀ n < d, Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) f : K) (0 : K)
rw :
  LE.le (α := WithZero (Multiplicative ℤ))
      (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          f :
        WithZero (Multiplicative ℤ))
      (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    HPow.hPow (α := Ideal K⟦X⟧) (Ideal.span {PowerSeries.X}) d ∣ Ideal.span {f}
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟦ℤ⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦ℤ⟧) → WithZero (Multiplicative ℤ))
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) :
        WithZero (Multiplicative ℤ))
      (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    ∀ n < d, Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) f : K) (0 : K)

Tactic:
rw [← this, ← LaurentSeries.coe_algebraMap, valuation_def, valuation_of_algebraMap,
    ← Ideal.span_singleton_dvd_span_singleton_iff_dvd, ← Ideal.span_singleton_pow]

Premises used: Ideal.span_singleton_dvd_span_singleton_iff_dvd, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, LaurentSeries.coe_algebraMap, LaurentSeries.valuation_def, Ideal.span_singleton_pow
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
d : ℕ
f : K⟦X⟧
this :
  HPow.hPow (α := K⟦X⟧) PowerSeries.X d ∣ f ↔
    ∀ n < d, Eq (α := K) ((PowerSeries.coeff n : (a : K⟦X⟧) → K) f : K) (0 : K)
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      (((intValuation (PowerSeries.idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          f :
        WithZero (Multiplicative ℤ))
      (exp (-(↑d : ℤ)) : WithZero (Multiplicative ℤ)) ↔
    HPow.hPow (α := Ideal K⟦X⟧) (Ideal.span {PowerSeries.X}) d ∣ Ideal.span {f}

Tactic:
apply intValuation_le_pow_iff_dvd

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
pos : ∀ (h_n_ord : n < HahnSeries.order f), f.coeff n = 0
neg : ∀ (h_n_ord : HahnSeries.order f ≤ n), f.coeff n = 0
⊢ f.coeff n = 0

Tactic:
by_cases! h_n_ord : n < f.order

Premises used: HahnSeries.order
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : n < HahnSeries.order f
⊢ f.coeff n = 0

Tactic:
coeff_eq_zero_of_lt_order h_n_ord

Premises used: HahnSeries.coeff_eq_zero_of_lt_order
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-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

Premises used: HahnSeries.coeff_eq_zero_of_lt_order
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
⊢ let F := f.powerSeriesPart;
  F = f.powerSeriesPart

Tactic:
set F := powerSeriesPart f with hF

Premises used: LaurentSeries.powerSeriesPart
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-D)
hnd : n < D
h_n_ord : HahnSeries.order f ≤ n
F : K⟦X⟧ := f.powerSeriesPart
hF : F = f.powerSeriesPart
pos : ∀ (ord_nonpos : HahnSeries.order f ≤ 0), f.coeff n = 0
neg : ∀ (ord_nonpos : 0 < HahnSeries.order f), f.coeff n = 0
⊢ f.coeff n = 0

Tactic:
by_cases! ord_nonpos : f.order ≤ 0

Premises used: HahnSeries.order
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-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
pos : ∀ (s : ℕ) (hs : HahnSeries.order f = -(↑s : ℤ)), f.coeff n = 0
⊢ f.coeff n = 0

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

Premises used: Int.exists_eq_neg_ofNat
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-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 : ℤ)
pos : ∀ (m : ℕ) (hm : n + (↑s : ℤ) = (↑m : ℤ)), f.coeff n = 0
⊢ f.coeff n = 0

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

Premises used: neg_le_iff_add_nonneg, Int.eq_ofNat_of_zero_le, Iff.mp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-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:
lia
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
n D : ℤ
f : K⸨X⸩
H : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) f ≤ exp (-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 : ℤ)
pos : ∀ (d : ℕ) (hd : D + (↑s : ℤ) = (↑d : ℤ)), f.coeff n = 0
⊢ f.coeff n = 0

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

Premises used: Int.eq_ofNat_of_zero_le