-- Mathlib/Algebra/Polynomial/Div.lean
theorem eval_divByMonic_pow_rootMultiplicity_ne_zero {p : R[X]} (a : R) (hp : p ≠ 0) :
    eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0

Proof state:
case intro
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
⊢ False

Tactic:
have := pow_mul_divByMonic_rootMultiplicity_eq p a

Result:
case intro
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p
⊢ False

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
⊢ eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0

Tactic:
classical
haveI : Nontrivial R := Nontrivial.of_polynomial_ne hp
rw [Ne, ← IsRoot, ← dvd_iff_isRoot]
rintro ⟨q, hq⟩
have := pow_mul_divByMonic_rootMultiplicity_eq p a
rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this
exact
  (finiteMultiplicity_of_degree_pos_of_monic
    (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; decide)
    (monic_X_sub_C _) hp).not_pow_dvd_of_multiplicity_lt
    (Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
⊢ eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0

Tactic:
rw [Ne, ← IsRoot, ← dvd_iff_isRoot]

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
⊢ ¬X - C a ∣ p /ₘ (X - C a) ^ rootMultiplicity a p

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
⊢ eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0

Tactic:
haveI : Nontrivial R := Nontrivial.of_polynomial_ne hp

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
⊢ eval a (p /ₘ (X - C a) ^ rootMultiplicity a p) ≠ 0

Proof state:
case intro
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p
⊢ False

Tactic:
rw [hq, ← mul_assoc, ← pow_succ, rootMultiplicity_eq_multiplicity, if_neg hp] at this

Result:
case intro
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ False

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
⊢ ¬X - C a ∣ p /ₘ (X - C a) ^ rootMultiplicity a p

Tactic:
rintro ⟨q, hq⟩

Result:
case intro
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
⊢ False

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ 0 < (X - C a).degree

Tactic:
rw [degree_X_sub_C]

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ 0 < 1

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
case intro
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
hp : p ≠ 0
this✝ : Nontrivial R
q : R[X]
hq : p /ₘ (X - C a) ^ rootMultiplicity a p = (X - C a) * q
this : (X - C a) ^ (multiplicity (X - C a) p + 1) * q = p
⊢ False

Tactic:
exact
  (finiteMultiplicity_of_degree_pos_of_monic
    (show (0 : WithBot ℕ) < degree (X - C a) by rw [degree_X_sub_C]; decide)
    (monic_X_sub_C _) hp).not_pow_dvd_of_multiplicity_lt
    (Nat.lt_succ_self _) (dvd_of_mul_right_eq _ this)

Result:
no goals