awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) (f ^ n) =
    HPow.hPow (α := R⟦ℤ⟧) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) f : R⟦ℤ⟧) n

Tactic:
(ofPowerSeries ℤ R).map_pow _ _

Premises used: Int, HahnSeries.ofPowerSeries, RingHom.map_pow
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
F : Type u
inst : Field F
p q : F[X]
f g : F⟮X⟯
⊢ FaithfulSMul.{u, u} F[X] F⸨X⸩

Tactic:
(faithfulSMul_iff_algebraMap_injective F[X] F⸨X⸩).mpr ?_

Premises used: Iff.mpr, faithfulSMul_iff_algebraMap_injective, Polynomial, LaurentSeries
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
F : Type u
inst : Field F
p q : F[X]
f g : F⟮X⟯
refine : Function.Injective.{u + 1, u + 1} (α := F[X]) (β := F⸨X⸩) (⇑(algebraMap F[X] F⸨X⸩) : (a : F[X]) → F⸨X⸩)
⊢ FaithfulSMul.{u, u} F[X] F⸨X⸩

Tactic:
refine (faithfulSMul_iff_algebraMap_injective F[X] F⸨X⸩).mpr ?_

Premises used: Iff.mpr, faithfulSMul_iff_algebraMap_injective, Polynomial, LaurentSeries
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
F : Type u
inst : Field F
p q : F[X]
f g : F⟮X⟯
⊢ Function.Injective.{u + 1, u + 1} (α := F[X]) (β := F⸨X⸩) (⇑(algebraMap F[X] F⸨X⸩) : (a : F[X]) → F⸨X⸩)

Tactic:
algebraMap_hahnSeries_injective ℤ

Premises used: Int, Polynomial.algebraMap_hahnSeries_injective
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
F : Type u
inst : Field F
p q : F[X]
f g : F⟮X⟯
⊢ Function.Injective.{u + 1, u + 1} (α := F[X]) (β := F⸨X⸩) (⇑(algebraMap F[X] F⸨X⸩) : (a : F[X]) → F⸨X⸩)

Tactic:
exact algebraMap_hahnSeries_injective ℤ

Premises used: Int, Polynomial.algebraMap_hahnSeries_injective
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
F : Type u
inst : Field F
P : F[X]
⊢ Eq (α := F⟦ℤ⟧) (((ofPowerSeries ℤ F : F⟦X⟧ →+* F⟦ℤ⟧) : (a : F⟦X⟧) → F⟦ℤ⟧) (↑P : F⟦X⟧) : F⟦ℤ⟧)
    ((algebraMap F⟮X⟯ F⸨X⸩ : (a : F⟮X⟯) → F⸨X⸩) (↑P : F⟮X⟯) : F⸨X⸩)

Tactic:
simp [coePolynomial, coe_def, ← IsScalarTower.algebraMap_apply]

Premises used: Polynomial.coe_def, RatFunc.coePolynomial, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
F : Type u
inst : Field F
⊢ Eq.{u + 1} (α := F⸨X⸩) ((algebraMap F⟮X⟯ F⸨X⸩ : (a : F⟮X⟯) → F⸨X⸩) X : F⸨X⸩) ((single 1 : (a : F) → F⟦ℤ⟧) 1 : F⟦ℤ⟧)

Tactic:
simp [← algebraMap_X, ← IsScalarTower.algebraMap_apply F[X] (RatFunc F) F⸨X⸩]

Premises used: RatFunc.algebraMap_X, Polynomial, RatFunc, LaurentSeries, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_2
inst : Semiring R
n : ℕ
⊢ (single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1 = HPow.hPow (α := R⟦ℤ⟧) ((single 1 : (a : R) → R⟦ℤ⟧) 1) n

Tactic:
simp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
F : Type u
inst : Field F
n_1 : ℤ
n : ℕ
⊢ (single (↑n : ℤ) : (a : F) → F⟦ℤ⟧) 1 = HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (↑n : ℤ)

Tactic:
apply single_one_eq_pow

Premises used: RatFunc.single_one_eq_pow
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
F : Type u
inst : Field F
n_1 : ℤ
n : ℕ
rw :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₁ :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₂ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₃ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ))⁻¹
rw₄ :
  ((single (↑(n + (↑(↑1 : ℕ) : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑(↑1 : ℕ) : ℕ)) : ℤ))⁻¹
rw₅ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ))⁻¹
rw₆ :
  (single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ)
rw₇ :
  (single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (n + (↑1 : ℕ))
rw₈ :
  HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (n + (↑1 : ℕ)) =
    HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (n + (↑1 : ℕ))
rw₉ rw₁₀ :
  HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (n + (↑1 : ℕ)) =
    HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (n + (↑1 : ℕ))
⊢ (single (-(↑(n + 1) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + 1) : ℤ))

Tactic:
rw [← Nat.cast_one, ← inv_one, ← HahnSeries.inv_single, zpow_neg,
      ← Nat.cast_one, Nat.cast_one,
      inv_inj, zpow_natCast, single_one_eq_pow, inv_one]

Premises used: zpow_natCast, inv_one, inv_inj, zpow_neg, RatFunc.single_one_eq_pow, HahnSeries.inv_single, Nat.cast_one
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
F : Type u
inst : Field F
n : ℤ
⊢ (single n : (a : F) → F⟦ℤ⟧) 1 = HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1) n

Tactic:
match n with
  | (n : ℕ) => apply single_one_eq_pow
  | -(n + 1 : ℕ) =>
    rw [← Nat.cast_one, ← inv_one, ← HahnSeries.inv_single, zpow_neg,
      ← Nat.cast_one, Nat.cast_one,
      inv_inj, zpow_natCast, single_one_eq_pow, inv_one]
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
F : Type u
inst : Field F
p q : F[X]
⊢ (algebraMap F⟮X⟯ F⸨X⸩ : (a : F⟮X⟯) → F⸨X⸩)
      (HDiv.hDiv (α := F⟮X⟯) (β := F⟮X⟯) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p : F⟮X⟯)
        ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) q : F⟮X⟯)) =
    HDiv.hDiv (α := F⸨X⸩) (β := F⸨X⸩) ((algebraMap F[X] F⸨X⸩ : (a : F[X]) → F⸨X⸩) p : F⸨X⸩)
      ((algebraMap F[X] F⸨X⸩ : (a : F[X]) → F⸨X⸩) q : F⸨X⸩)

Tactic:
simp only [map_div₀, IsScalarTower.algebraMap_apply F[X] (RatFunc F) F⸨X⸩]

Premises used: Polynomial, RatFunc, map_div₀, LaurentSeries, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
K : Type u_2
inst : Field K
rw : ¬Eq.{u_2 + 1} (α := K⟦X⟧) X 0
⊢ Ne (α := Ideal K⟦X⟧) (Ideal.span {X}) ⊥

Tactic:
rw [ne_eq, Ideal.span_singleton_eq_bot]

Premises used: Ideal.span_singleton_eq_bot, ne_eq
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
K : Type u_2
inst : Field K
⊢ ¬Eq.{u_2 + 1} (α := K⟦X⟧) X 0

Tactic:
X_ne_zero

Premises used: PowerSeries.X_ne_zero
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
K : Type u_2
inst : Field K
⊢ ¬Eq.{u_2 + 1} (α := K⟦X⟧) X 0

Tactic:
exact X_ne_zero

Premises used: PowerSeries.X_ne_zero
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
pos :
  ∀ (hP : P = 0),
    Eq (α := WithZero (Multiplicative ℤ))
      (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
            (a : K[X]) → WithZero (Multiplicative ℤ))
          P :
        WithZero (Multiplicative ℤ))
      (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          (↑P : K⟦X⟧) :
        WithZero (Multiplicative ℤ))
neg :
  ∀ (hP : ¬P = 0),
    Eq (α := WithZero (Multiplicative ℤ))
      (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
            (a : K[X]) → WithZero (Multiplicative ℤ))
          P :
        WithZero (Multiplicative ℤ))
      (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          (↑P : K⟦X⟧) :
        WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        P :
      WithZero (Multiplicative ℤ))
    (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑P : K⟦X⟧) :
      WithZero (Multiplicative ℤ))

Tactic:
by_cases hP : P = 0
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : P = 0
pos :
  Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        0 :
      WithZero (Multiplicative ℤ))
    (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑0 : K⟦X⟧) :
      WithZero (Multiplicative ℤ))
pos₁ :
  Eq (α := WithZero (Multiplicative ℤ)) (0 : WithZero (Multiplicative ℤ))
    (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑0 : K⟦X⟧) :
      WithZero (Multiplicative ℤ))
pos₂ :
  Eq (α := WithZero (Multiplicative ℤ)) (0 : WithZero (Multiplicative ℤ))
    (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        0 :
      WithZero (Multiplicative ℤ))
pos₃ pos₄ : Eq (α := WithZero (Multiplicative ℤ)) 0 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        P :
      WithZero (Multiplicative ℤ))
    (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑P : K⟦X⟧) :
      WithZero (Multiplicative ℤ))

Tactic:
rw [hP, Valuation.map_zero, Polynomial.coe_zero, Valuation.map_zero]

Premises used: Polynomial.coe_zero, Valuation.map_zero
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
⊢ (↑P : K⟦X⟧) ≠ 0

Tactic:
simp [hP]
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
neg :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp
      (-(↑(Associates.count (α := Ideal K[X]) (Associates.mk (asIdeal (Polynomial.idealX K)))
              (Associates.factors (Associates.mk (Ideal.span {P})))) :
          ℤ)))
    (exp
      (-(↑(Associates.count (α := Ideal K⟦X⟧) (Associates.mk (asIdeal (idealX K)))
              (Associates.factors (Associates.mk (Ideal.span {(↑P : K⟦X⟧)})))) :
          ℤ)))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        P :
      WithZero (Multiplicative ℤ))
    (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑P : K⟦X⟧) :
      WithZero (Multiplicative ℤ))

Tactic:
rw [intValuation_if_neg _ hP, intValuation_if_neg _ <| (by simp [hP])]

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
neg :
  Associates.count (α := Ideal K[X]) (Associates.mk (Ideal.span {Polynomial.X}))
      (Associates.factors (Associates.mk (Ideal.span {P}))) =
    Associates.count (α := Ideal K⟦X⟧) (Associates.mk (asIdeal (idealX K)))
      (Associates.factors (Associates.mk (Ideal.span {(↑P : K⟦X⟧)})))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (exp
      (-(↑(Associates.count (α := Ideal K[X]) (Associates.mk (asIdeal (Polynomial.idealX K)))
              (Associates.factors (Associates.mk (Ideal.span {P})))) :
          ℤ)))
    (exp
      (-(↑(Associates.count (α := Ideal K⟦X⟧) (Associates.mk (asIdeal (idealX K)))
              (Associates.factors (Associates.mk (Ideal.span {(↑P : K⟦X⟧)})))) :
          ℤ)))

Tactic:
simp only [idealX_span, exp_neg, inv_inj, exp_inj, Nat.cast_inj]

Premises used: WithZero.exp_inj, Polynomial.idealX_span, Nat.cast_inj, inv_inj, WithZero.exp_neg
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
⊢ Ne (α := Ideal K[X]) (Ideal.span {P}) 0 ∧ Ne (α := Ideal K[X]) (Ideal.span {Polynomial.X}) 0

Tactic:
simp only [Ideal.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot, hP, Polynomial.X_ne_zero,
      not_false_iff, and_self_iff]

Premises used: Ideal.span_singleton_eq_bot, Ideal.zero_eq_bot, ne_eq, Polynomial.X_ne_zero, and_self_iff, not_false_iff
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
⊢ Ne (α := Ideal K[X]) (Ideal.span {P}) 0 ∧ Ne (α := Ideal K[X]) (Ideal.span {Polynomial.X}) 0

Tactic:
have span_ne_zero :
    (Ideal.span {P} : Ideal K[X]) ≠ 0 ∧ (Ideal.span {Polynomial.X} : Ideal K[X]) ≠ 0 := by
    simp only [Ideal.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot, hP, Polynomial.X_ne_zero,
      not_false_iff, and_self_iff]
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ne (α := Ideal K[X]) (Ideal.span {P}) 0 ∧ Ne (α := Ideal K[X]) (Ideal.span {Polynomial.X}) 0
⊢ Ne (α := Ideal K⟦X⟧) (Ideal.span {(↑P : K⟦X⟧)}) 0 ∧ Ne (α := Ideal K⟦X⟧) (asIdeal (idealX K)) 0

Tactic:
simp only [Ideal.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot, coe_eq_zero_iff, hP,
      not_false_eq_true, true_and, (idealX K).3]

Premises used: Ideal.span_singleton_eq_bot, Polynomial.coe_eq_zero_iff, Ideal.zero_eq_bot, ne_eq, PowerSeries.idealX, IsDedekindDomain.HeightOneSpectrum.ne_bot, not_false_eq_true, true_and
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ne (α := Ideal K[X]) (Ideal.span {P}) 0 ∧ Ne (α := Ideal K[X]) (Ideal.span {Polynomial.X}) 0
⊢ Ne (α := Ideal K⟦X⟧) (Ideal.span {(↑P : K⟦X⟧)}) 0 ∧ Ne (α := Ideal K⟦X⟧) (asIdeal (idealX K)) 0

Tactic:
have span_ne_zero' :
    (Ideal.span {↑P} : Ideal K⟦X⟧) ≠ 0 ∧ ((idealX K).asIdeal : Ideal K⟦X⟧) ≠ 0 := by
    simp only [Ideal.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot, coe_eq_zero_iff, hP,
      not_false_eq_true, true_and, (idealX K).3]
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ne (α := Ideal K[X]) (Ideal.span {P}) 0 ∧ Ne (α := Ideal K[X]) (Ideal.span {Polynomial.X}) 0
span_ne_zero' : Ne (α := Ideal K⟦X⟧) (Ideal.span {(↑P : K⟦X⟧)}) 0 ∧ Ne (α := Ideal K⟦X⟧) (asIdeal (idealX K)) 0
neg :
  Multiset.count (α := Ideal K[X]) (Ideal.span {Polynomial.X})
      (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    Multiset.count (α := Ideal K⟦X⟧) (asIdeal (idealX K))
      (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {(↑P : K⟦X⟧)}))
neg₁ : Ne (α := Ideal K⟦X⟧) (Ideal.span {(↑P : K⟦X⟧)}) 0
neg₂ : Ideal.IsPrime (asIdeal (idealX K))
neg₃ : Ne (α := Ideal K⟦X⟧) (asIdeal (idealX K)) ⊥
⊢ Associates.count (α := Ideal K[X]) (Associates.mk (Ideal.span {Polynomial.X}))
      (Associates.factors (Associates.mk (Ideal.span {P}))) =
    Associates.count (α := Ideal K⟦X⟧) (Associates.mk (asIdeal (idealX K)))
      (Associates.factors (Associates.mk (Ideal.span {(↑P : K⟦X⟧)})))

Tactic:
rw [Ideal.count_associates_factors_eq span_ne_zero.1
    (Ideal.span_singleton_prime Polynomial.X_ne_zero |>.mpr prime_X) span_ne_zero.2,
    Ideal.count_associates_factors_eq]

Premises used: Iff.mpr, And.right, And.left, Ideal.count_associates_factors_eq, Polynomial.prime_X, Ideal.span_singleton_prime
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ne (α := Ideal K[X]) (Ideal.span {P}) 0 ∧ Ne (α := Ideal K[X]) (Ideal.span {Polynomial.X}) 0
span_ne_zero' : Ne (α := Ideal K⟦X⟧) (Ideal.span {(↑P : K⟦X⟧)}) 0 ∧ Ne (α := Ideal K⟦X⟧) (asIdeal (idealX K)) 0
⊢ Multiset.count Polynomial.X (UniqueFactorizationMonoid.normalizedFactors P) =
    Multiset.count X (UniqueFactorizationMonoid.normalizedFactors (↑P : K⟦X⟧))

Tactic:
(normalized_count_X_eq_of_coe hP).symm

Premises used: PowerSeries.normalized_count_X_eq_of_coe, Eq.symm
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ne (α := Ideal K[X]) (Ideal.span {P}) 0 ∧ Ne (α := Ideal K[X]) (Ideal.span {Polynomial.X}) 0
span_ne_zero' : Ne (α := Ideal K⟦X⟧) (Ideal.span {(↑P : K⟦X⟧)}) 0 ∧ Ne (α := Ideal K⟦X⟧) (asIdeal (idealX K)) 0
h :
  Multiset.count (α := Ideal K[X]) (Ideal.span {Polynomial.X})
      (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    Multiset.count Polynomial.X (UniqueFactorizationMonoid.normalizedFactors P)
h₁ :
  Multiset.count (α := Ideal K⟦X⟧) (asIdeal (idealX K))
      (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {(↑P : K⟦X⟧)})) =
    Multiset.count X (UniqueFactorizationMonoid.normalizedFactors (↑P : K⟦X⟧))
⊢ Multiset.count (α := Ideal K[X]) (Ideal.span {Polynomial.X})
      (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    Multiset.count (α := Ideal K⟦X⟧) (asIdeal (idealX K))
      (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {(↑P : K⟦X⟧)}))

Tactic:
convert! (normalized_count_X_eq_of_coe hP).symm

Premises used: PowerSeries.normalized_count_X_eq_of_coe, Eq.symm
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ne (α := Ideal K[X]) (Ideal.span {P}) 0 ∧ Ne (α := Ideal K[X]) (Ideal.span {Polynomial.X}) 0
span_ne_zero' : Ne (α := Ideal K⟦X⟧) (Ideal.span {(↑P : K⟦X⟧)}) 0 ∧ Ne (α := Ideal K⟦X⟧) (asIdeal (idealX K)) 0
h :
  Multiset.count (α := Ideal K[X]) (Ideal.span {Polynomial.X})
      (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    Multiset.count Polynomial.X (UniqueFactorizationMonoid.normalizedFactors P)
h₁ :
  Multiset.count (α := Ideal K⟦X⟧) (asIdeal (idealX K))
      (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {(↑P : K⟦X⟧)})) =
    Multiset.count X (UniqueFactorizationMonoid.normalizedFactors (↑P : K⟦X⟧))
⊢ Multiset.count (α := Ideal K[X]) (Ideal.span {Polynomial.X})
      (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    Multiset.count (α := Ideal K⟦X⟧) (asIdeal (idealX K))
      (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {(↑P : K⟦X⟧)}))

Tactic:
on_goal 1 => convert! (normalized_count_X_eq_of_coe hP).symm

Premises used: PowerSeries.normalized_count_X_eq_of_coe, Eq.symm
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ne (α := Ideal K[X]) (Ideal.span {P}) 0 ∧ Ne (α := Ideal K[X]) (Ideal.span {Polynomial.X}) 0
span_ne_zero' : Ne (α := Ideal K⟦X⟧) (Ideal.span {(↑P : K⟦X⟧)}) 0 ∧ Ne (α := Ideal K⟦X⟧) (asIdeal (idealX K)) 0
⊢ Multiset.count (α := Ideal K[X]) (Ideal.span {Polynomial.X})
      (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    Multiset.count Polynomial.X (UniqueFactorizationMonoid.normalizedFactors P)

Tactic:
Ideal.count_span_normalizedFactors_eq_of_normUnit hP Polynomial.normUnit_X prime_X

Premises used: Ideal.count_span_normalizedFactors_eq_of_normUnit, Polynomial.prime_X, Polynomial.normUnit_X
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ne (α := Ideal K[X]) (Ideal.span {P}) 0 ∧ Ne (α := Ideal K[X]) (Ideal.span {Polynomial.X}) 0
span_ne_zero' : Ne (α := Ideal K⟦X⟧) (Ideal.span {(↑P : K⟦X⟧)}) 0 ∧ Ne (α := Ideal K⟦X⟧) (asIdeal (idealX K)) 0
⊢ (↑P : K⟦X⟧) ≠ 0

Tactic:
simp [hP]
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ne (α := Ideal K[X]) (Ideal.span {P}) 0 ∧ Ne (α := Ideal K[X]) (Ideal.span {Polynomial.X}) 0
span_ne_zero' : Ne (α := Ideal K⟦X⟧) (Ideal.span {(↑P : K⟦X⟧)}) 0 ∧ Ne (α := Ideal K⟦X⟧) (asIdeal (idealX K)) 0
⊢ Ne (α := Ideal K⟦X⟧) (Ideal.span {(↑P : K⟦X⟧)}) 0

Tactic:
span_ne_zero'.1

Premises used: And.left
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ne (α := Ideal K[X]) (Ideal.span {P}) 0 ∧ Ne (α := Ideal K[X]) (Ideal.span {Polynomial.X}) 0
span_ne_zero' : Ne (α := Ideal K⟦X⟧) (Ideal.span {(↑P : K⟦X⟧)}) 0 ∧ Ne (α := Ideal K⟦X⟧) (asIdeal (idealX K)) 0
⊢ Ideal.IsPrime (asIdeal (idealX K))

Tactic:
(idealX K).isPrime

Premises used: PowerSeries.idealX, IsDedekindDomain.HeightOneSpectrum.isPrime
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ne (α := Ideal K[X]) (Ideal.span {P}) 0 ∧ Ne (α := Ideal K[X]) (Ideal.span {Polynomial.X}) 0
span_ne_zero' : Ne (α := Ideal K⟦X⟧) (Ideal.span {(↑P : K⟦X⟧)}) 0 ∧ Ne (α := Ideal K⟦X⟧) (asIdeal (idealX K)) 0
⊢ Ne (α := Ideal K⟦X⟧) (asIdeal (idealX K)) ⊥

Tactic:
span_ne_zero'.2

Premises used: And.right
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ne (α := Ideal K[X]) (Ideal.span {P}) 0 ∧ Ne (α := Ideal K[X]) (Ideal.span {Polynomial.X}) 0
span_ne_zero' : Ne (α := Ideal K⟦X⟧) (Ideal.span {(↑P : K⟦X⟧)}) 0 ∧ Ne (α := Ideal K⟦X⟧) (asIdeal (idealX K)) 0
⊢ Multiset.count (α := Ideal K[X]) (Ideal.span {Polynomial.X})
      (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    Multiset.count Polynomial.X (UniqueFactorizationMonoid.normalizedFactors P)

Tactic:
exacts [Ideal.count_span_normalizedFactors_eq_of_normUnit hP Polynomial.normUnit_X prime_X,
    Ideal.count_span_normalizedFactors_eq_of_normUnit (by simp [hP]) normUnit_X X_prime,
    span_ne_zero'.1, (idealX K).isPrime, span_ne_zero'.2]

Premises used: Ideal.count_span_normalizedFactors_eq_of_normUnit, PowerSeries.idealX, And.right, And.left, Polynomial.prime_X, IsDedekindDomain.HeightOneSpectrum.isPrime, Polynomial.normUnit_X
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        Polynomial.X :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        X :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))

Tactic:
rw [← Polynomial.coe_X, ← intValuation_eq_of_coe]

Premises used: PowerSeries.intValuation_eq_of_coe, Polynomial.coe_X
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        Polynomial.X :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))

Tactic:
intValuation_singleton _ Polynomial.X_ne_zero (idealX_span _)

Premises used: Polynomial.idealX_span, IsDedekindDomain.HeightOneSpectrum.intValuation_singleton, Polynomial.X_ne_zero
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        Polynomial.X :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))

Tactic:
exact intValuation_singleton _ Polynomial.X_ne_zero (idealX_span _)

Premises used: Polynomial.idealX_span, IsDedekindDomain.HeightOneSpectrum.intValuation_singleton
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
P : K⟮X⟯
⊢ 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:
RatFunc.induction_on' P ?_

Premises used: RatFunc.induction_on'