-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors
    {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0)
    (hroot : ∀ m ≤ n, (derivative^[m] p).IsRoot t)
    (hnzd : (n.factorial : R) ∈ nonZeroDivisors R) :
    n < p.rootMultiplicity t

Proof state:
case intro
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : (rootMultiplicity t p).factorial • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hnzd : ↑(rootMultiplicity t p).factorial ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R
hq : ↑n.factorial = ↑(rootMultiplicity t p).factorial * q
⊢ False

Tactic:
rw [nsmul_eq_mul, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd.1] at hroot

Result:
case intro
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hnzd : ↑(rootMultiplicity t p).factorial ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R
hq : ↑n.factorial = ↑(rootMultiplicity t p).factorial * q
⊢ False

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ↑n.factorial ∈ nonZeroDivisors R
h' : rootMultiplicity t p ≤ n
hroot : (rootMultiplicity t p).factorial • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
⊢ False

Tactic:
obtain ⟨q, hq⟩ := Nat.cast_dvd_cast (α := R) <| Nat.factorial_dvd_factorial h'

Result:
case intro
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ↑n.factorial ∈ nonZeroDivisors R
h' : rootMultiplicity t p ≤ n
hroot : (rootMultiplicity t p).factorial • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hq : ↑n.factorial = ↑(rootMultiplicity t p).factorial * q
⊢ False

Proof state:
case intro
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ↑n.factorial ∈ nonZeroDivisors R
h' : rootMultiplicity t p ≤ n
hroot : (rootMultiplicity t p).factorial • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hq : ↑n.factorial = ↑(rootMultiplicity t p).factorial * q
⊢ False

Tactic:
rw [hq, mul_mem_nonZeroDivisors] at hnzd

Result:
case intro
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : (rootMultiplicity t p).factorial • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hnzd : ↑(rootMultiplicity t p).factorial ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R
hq : ↑n.factorial = ↑(rootMultiplicity t p).factorial * q
⊢ False

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
hnzd : ↑n.factorial ∈ nonZeroDivisors R
⊢ n < rootMultiplicity t p

Tactic:
by_contra! h'

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
hnzd : ↑n.factorial ∈ nonZeroDivisors R
h' : rootMultiplicity t p ≤ n
⊢ False

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
hnzd : ↑n.factorial ∈ nonZeroDivisors R
h' : rootMultiplicity t p ≤ n
⊢ False

Tactic:
replace hroot := hroot _ h'

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ↑n.factorial ∈ nonZeroDivisors R
h' : rootMultiplicity t p ≤ n
hroot : ((⇑derivative)^[rootMultiplicity t p] p).IsRoot t
⊢ False

Proof state:
case intro
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
q : R
hnzd : ↑(rootMultiplicity t p).factorial ∈ nonZeroDivisors R ∧ q ∈ nonZeroDivisors R
hq : ↑n.factorial = ↑(rootMultiplicity t p).factorial * q
⊢ False

Tactic:
exact eval_divByMonic_pow_rootMultiplicity_ne_zero t h hroot

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ↑n.factorial ∈ nonZeroDivisors R
h' : rootMultiplicity t p ≤ n
hroot : ((⇑derivative)^[rootMultiplicity t p] p).IsRoot t
⊢ False

Tactic:
simp only [IsRoot, eval_iterate_derivative_rootMultiplicity] at hroot

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ↑n.factorial ∈ nonZeroDivisors R
h' : rootMultiplicity t p ≤ n
hroot : (rootMultiplicity t p).factorial • eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = 0
⊢ False