-- Mathlib/RingTheory/LaurentSeries.lean
theorem intValuation_eq_of_coe (P : K[X]) :
    (Polynomial.idealX K).intValuation P = (idealX K).intValuation (P : K⟦X⟧)

Proof state:
case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ (Associates.mk (Ideal.span {Polynomial.X})).count (Associates.mk (Ideal.span {P})).factors =
    (Associates.mk (idealX K).asIdeal).count (Associates.mk (Ideal.span {↑P})).factors

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

Result:
case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ Multiset.count (Ideal.span {Polynomial.X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {P})) =
    Multiset.count (idealX K).asIdeal (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {↑P}))

case neg.hI
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ Ideal.span {↑P} ≠ 0

case neg.hJ
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ (idealX K).asIdeal.IsPrime

case neg.hJ₀
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
span_ne_zero' : Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 0
⊢ (idealX K).asIdeal ≠ ⊥

Proof state:
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ Ideal.span {P} ≠ 0 ∧ 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]

Result:
no goals

Proof state:
case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ (Polynomial.idealX K).intValuationDef P = (idealX K).intValuationDef ↑P

Tactic:
rw [intValuationDef_if_neg _ hP, intValuationDef_if_neg _ <| coe_ne_zero hP]

Result:
case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ ↑(Multiplicative.ofAdd
        (-↑((Associates.mk (Polynomial.idealX K).asIdeal).count (Associates.mk (Ideal.span {P})).factors))) =
    ↑(Multiplicative.ofAdd (-↑((Associates.mk (idealX K).asIdeal).count (Associates.mk (Ideal.span {↑P})).factors)))

Proof state:
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
⊢ Ideal.span {↑P} ≠ 0 ∧ (idealX K).asIdeal ≠ 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]

Result:
no goals

Proof state:
case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ ↑(Multiplicative.ofAdd
        (-↑((Associates.mk (Polynomial.idealX K).asIdeal).count (Associates.mk (Ideal.span {P})).factors))) =
    ↑(Multiplicative.ofAdd (-↑((Associates.mk (idealX K).asIdeal).count (Associates.mk (Ideal.span {↑P})).factors)))

Tactic:
simp only [idealX_span, ofAdd_neg, inv_inj, WithZero.coe_inj, EmbeddingLike.apply_eq_iff_eq,
  Nat.cast_inj]

Result:
case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ (Associates.mk (Ideal.span {Polynomial.X})).count (Associates.mk (Ideal.span {P})).factors =
    (Associates.mk (idealX K).asIdeal).count (Associates.mk (Ideal.span {↑P})).factors

Proof state:
case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ (Associates.mk (Ideal.span {Polynomial.X})).count (Associates.mk (Ideal.span {P})).factors =
    (Associates.mk (idealX K).asIdeal).count (Associates.mk (Ideal.span {↑P})).factors

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]

Result:
case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
span_ne_zero : Ideal.span {P} ≠ 0 ∧ Ideal.span {Polynomial.X} ≠ 0
⊢ (Associates.mk (Ideal.span {Polynomial.X})).count (Associates.mk (Ideal.span {P})).factors =
    (Associates.mk (idealX K).asIdeal).count (Associates.mk (Ideal.span {↑P})).factors

Proof state:
K : Type u_2
inst✝ : Field K
P : K[X]
⊢ (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P

Tactic:
by_cases hP : P = 0

Result:
case pos
K : Type u_2
inst✝ : Field K
P : K[X]
hP : P = 0
⊢ (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P

case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P

Proof state:
case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ (Polynomial.idealX K).intValuation P = (idealX K).intValuation ↑P

Tactic:
simp only [intValuation_apply]

Result:
case neg
K : Type u_2
inst✝ : Field K
P : K[X]
hP : ¬P = 0
⊢ (Polynomial.idealX K).intValuationDef P = (idealX K).intValuationDef ↑P