awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
⊢ m - 1 + 1 = m

Tactic:
have hm : m - 1 + 1 = m := Nat.sub_add_cancel <| (rootMultiplicity_pos h).2 hpt
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
rw : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ (C : (a : R) → R[X]) (↑m : R) * g
⊢ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p

Tactic:
rw [hp, derivative_mul, dvd_add_left (dvd_mul_right _ _),
      derivative_X_sub_C_pow, ← hm, pow_succ, hm, mul_comm (C _), mul_assoc,
      dvd_cancel_left_mem_nonZeroDivisors (monic_X_sub_C t |>.pow _ |>.mem_nonZeroDivisors)]

Premises used: Polynomial.monic_X_sub_C, Polynomial.C, Polynomial.derivative_mul, pow_succ, mul_assoc, Polynomial.derivative_X_sub_C_pow, dvd_cancel_left_mem_nonZeroDivisors, Polynomial.Monic.mem_nonZeroDivisors, Polynomial.Monic.pow, dvd_add_left, mul_comm, dvd_mul_right, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
rw :
  ∀ (hndvd : ¬eval t g = 0),
    let m := rootMultiplicity t p;
    ∀ (hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R))
      (hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g) (hm : m - 1 + 1 = m),
      ¬eval t ((C : (a : R) → R[X]) (↑m : R) * g) = 0
⊢ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ (C : (a : R) → R[X]) (↑m : R) * g

Tactic:
rw [dvd_iff_isRoot, IsRoot] at hndvd ⊢

Premises used: Polynomial.IsRoot, Polynomial.dvd_iff_isRoot
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬eval t g = 0
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
rwa : ¬eval t ((C : (a : R) → R[X]) (↑m : R)) * eval t g = 0
rwa₁ : ¬(↑m : R) * eval t g = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ¬eval t g = 0
⊢ ¬eval t ((C : (a : R) → R[X]) (↑m : R) * g) = 0

Tactic:
rwa [eval_mul, eval_C, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd]

Premises used: Polynomial.eval_C, mul_left_mem_nonZeroDivisors_eq_zero_iff, Polynomial.eval_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
⊢ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p

Tactic:
have hndvd : ¬(X - C t) ^ m ∣ derivative p := by
    rw [hp, derivative_mul, dvd_add_left (dvd_mul_right _ _),
      derivative_X_sub_C_pow, ← hm, pow_succ, hm, mul_comm (C _), mul_assoc,
      dvd_cancel_left_mem_nonZeroDivisors (monic_X_sub_C t |>.pow _ |>.mem_nonZeroDivisors)]
    rw [dvd_iff_isRoot, IsRoot] at hndvd ⊢
    rwa [eval_mul, eval_C, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h_1 : ¬p = 0
g : R[X]
hndvd_1 : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
rw : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h_1 : ¬p = 0
g : R[X]
hndvd_1 : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ 0

Tactic:
dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h_1 : ¬p = 0
g : R[X]
hndvd_1 : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ 0

Tactic:
exact dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd_1 : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p
⊢ Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])

Tactic:
have hnezero : derivative p ≠ 0 := fun h ↦ hndvd (by rw [h]; exact dvd_zero _)
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd_1 : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p
hnezero : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
rwa :
  ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ (m - 1 + 1) ∣
      (derivative : (a : R[X]) → R[X]) p
rwa₁ rwa₂ rwa₃ rwa₄ :
  ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) ≤ m - 1

Tactic:
rwa [rootMultiplicity_le_iff hnezero, hm]

Premises used: Polynomial.rootMultiplicity_le_iff
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
g : R[X]
hndvd_1 : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
m : ℕ := rootMultiplicity t p
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m ∣ (derivative : (a : R[X]) → R[X]) p
hnezero : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = m - 1

Tactic:
exact le_antisymm (by rwa [rootMultiplicity_le_iff hnezero, hm])
    (rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero _ t hnezero)

Premises used: Polynomial.rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero, le_antisymm
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
hn : n < rootMultiplicity t p
⊢ ((⇑derivative : (a : R[X]) → R[X])^[n] p).IsRoot t

Tactic:
dvd_iff_isRoot.mp <| (dvd_pow_self _ <| Nat.sub_ne_zero_of_lt hn).trans
    (pow_sub_dvd_iterate_derivative_of_pow_dvd _ <| p.pow_rootMultiplicity_dvd t)

Premises used: Polynomial.pow_rootMultiplicity_dvd, dvd_pow_self, Nat.sub_ne_zero_of_lt, Iff.mp, Polynomial.pow_sub_dvd_iterate_derivative_of_pow_dvd, Polynomial.dvd_iff_isRoot, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
set :
  let m := rootMultiplicity t p;
  ∀ (hm : m = rootMultiplicity t p),
    eval t ((⇑derivative : (a : R[X]) → R[X])^[m] p) =
      m ! • eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)
⊢ eval t ((⇑derivative : (a : R[X]) → R[X])^[rootMultiplicity t p] p) =
    (rootMultiplicity t p)! •
      eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p)

Tactic:
set m := p.rootMultiplicity t with hm

Premises used: Polynomial.rootMultiplicity
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
rw :
  eval t
    ((⇑derivative : (a : R[X]) → R[X])^[m]
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m *
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)))
| eval t ((⇑derivative : (a : R[X]) → R[X])^[m] p)

Tactic:
rw [← p.pow_mul_divByMonic_rootMultiplicity_eq t, ← hm]

Premises used: Polynomial.pow_mul_divByMonic_rootMultiplicity_eq
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
conv_lhs :
  eval t
      ((⇑derivative : (a : R[X]) → R[X])^[m]
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m *
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    m ! • eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)
⊢ eval t ((⇑derivative : (a : R[X]) → R[X])^[m] p) =
    m ! • eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)

Tactic:
conv_lhs => rw [← p.pow_mul_divByMonic_rootMultiplicity_eq t, ← hm]

Premises used: Polynomial.pow_mul_divByMonic_rootMultiplicity_eq
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
rw :
  eval t
      (m.choose 0 •
        ((⇑derivative : (a : R[X]) → R[X])^[m - 0]
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
          (⇑derivative : (a : R[X]) → R[X])^[0]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    m ! • eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)
rw₁ :
  ∀ b ∈ range m.succ,
    b ≠ 0 →
      eval t
          (m.choose b •
            ((⇑derivative : (a : R[X]) → R[X])^[m - b]
                (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
              (⇑derivative : (a : R[X]) → R[X])^[b]
                (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
        0
⊢ eval t
      ((⇑derivative : (a : R[X]) → R[X])^[m]
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m *
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    m ! • eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)

Tactic:
rw [iterate_derivative_mul, eval_finsetSum, sum_eq_single_of_mem _ (mem_range.mpr m.succ_pos)]

Premises used: Iff.mpr, Finset.sum_eq_single_of_mem, Finset.mem_range, Polynomial.eval_finsetSum, Nat.succ_pos, Polynomial.iterate_derivative_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
rw :
  (↑m ! : R) *
      eval t
        ((⇑derivative : (a : R[X]) → R[X])^[0]
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)) =
    (↑m ! : R) * eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)
⊢ eval t
      (m.choose 0 •
        ((⇑derivative : (a : R[X]) → R[X])^[m - 0]
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) *
          (⇑derivative : (a : R[X]) → R[X])^[0]
            (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m))) =
    m ! • eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)

Tactic:
rw [m.choose_zero_right, one_smul, eval_mul, m.sub_zero, iterate_derivative_X_sub_pow_self,
      eval_natCast, nsmul_eq_mul]

Premises used: Polynomial.eval_natCast, Polynomial.eval_mul, one_smul, Polynomial.iterate_derivative_X_sub_pow_self, nsmul_eq_mul, Nat.sub_zero, Nat.choose_zero_right
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
⊢ (↑m ! : R) *
      eval t
        ((⇑derivative : (a : R[X]) → R[X])^[0]
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)) =
    (↑m ! : R) * eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m)

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
by_contra! : ∀ (h' : rootMultiplicity t p ≤ n), False
⊢ n < rootMultiplicity t p

Tactic:
by_contra! h'
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
h' : rootMultiplicity t p ≤ n
⊢ ((⇑derivative : (a : R[X]) → R[X])^[rootMultiplicity t p] p).IsRoot t

Tactic:
replace hroot := hroot _ h'
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
h' : rootMultiplicity t p ≤ n
hroot : ((⇑derivative : (a : R[X]) → R[X])^[rootMultiplicity t p] p).IsRoot t
⊢ (rootMultiplicity t p)! •
      eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    0

Tactic:
simp only [IsRoot, eval_iterate_derivative_rootMultiplicity] at hroot

Premises used: Polynomial.IsRoot, Polynomial.eval_iterate_derivative_rootMultiplicity
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
h' : rootMultiplicity t p ≤ n
hroot :
  (rootMultiplicity t p)! •
      eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    0
⊢ Dvd.dvd.{u} (α := R) (↑(rootMultiplicity t p)! : R) (↑n ! : R)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
h' : rootMultiplicity t p ≤ n
hroot :
  (rootMultiplicity t p)! •
      eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    0
obtain : ∀ (q : R) (hq : (↑n ! : R) = (↑(rootMultiplicity t p)! : R) * q), False
⊢ False

Tactic:
obtain ⟨q, hq⟩ : ((rootMultiplicity t p)! : R) ∣ n ! := by gcongr

Premises used: Nat.cast, Nat.factorial, Polynomial.rootMultiplicity
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
h' : rootMultiplicity t p ≤ n
hroot :
  (rootMultiplicity t p)! •
      eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    0
q : R
hq : (↑n ! : R) = (↑(rootMultiplicity t p)! : R) * q
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p)! : R) ∧
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) q

Tactic:
rw [hq, mul_mem_nonZeroDivisors] at hnzd

Premises used: mul_mem_nonZeroDivisors
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
h' : rootMultiplicity t p ≤ n
hroot :
  (rootMultiplicity t p)! •
      eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    0
q : R
hq : (↑n ! : R) = (↑(rootMultiplicity t p)! : R) * q
hnzd₁ :
  Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p)! : R) ∧
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) q
⊢ (↑n ! : R) = (↑(rootMultiplicity t p)! : R) * q

Tactic:
rw [hq, mul_mem_nonZeroDivisors] at hnzd

Premises used: mul_mem_nonZeroDivisors
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot :
  (rootMultiplicity t p)! •
      eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) =
    0
q : R
hnzd :
  Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p)! : R) ∧
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) q
hq : (↑n ! : R) = (↑(rootMultiplicity t p)! : R) * q
rw :
  ∀
    (hroot :
      eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) = 0)
    (q : R)
    (hnzd :
      Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p)! : R) ∧
        Membership.mem (γ := Submonoid R) (nonZeroDivisors R) q)
    (hq : (↑n ! : R) = (↑(rootMultiplicity t p)! : R) * q), False
⊢ False

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

Premises used: mul_left_mem_nonZeroDivisors_eq_zero_iff, And.left, nsmul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) = 0
q : R
hnzd :
  Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p)! : R) ∧
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) q
hq : (↑n ! : R) = (↑(rootMultiplicity t p)! : R) * q
⊢ False

Tactic:
eval_divByMonic_pow_rootMultiplicity_ne_zero t h hroot

Premises used: Polynomial.eval_divByMonic_pow_rootMultiplicity_ne_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
h' : rootMultiplicity t p ≤ n
hroot : eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p) = 0
q : R
hnzd :
  Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p)! : R) ∧
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) q
hq : (↑n ! : R) = (↑(rootMultiplicity t p)! : R) * q
⊢ False

Tactic:
exact eval_divByMonic_pow_rootMultiplicity_ne_zero t h hroot

Premises used: Polynomial.eval_divByMonic_pow_rootMultiplicity_ne_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t
hnzd : ∀ m ≤ n, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
apply : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
⊢ n < rootMultiplicity t p

Tactic:
apply lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors h hroot

Premises used: Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
hnzd : ∀ m ≤ 0, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
zero : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) 1
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑0! : R)

Tactic:
simp only [Nat.factorial_zero, Nat.cast_one]

Premises used: Nat.factorial_zero, Nat.cast_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
hnzd : ∀ m ≤ 0, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) 1

Tactic:
Submonoid.one_mem _

Premises used: Set.Mem, Submonoid.one_mem
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
hnzd : ∀ m ≤ 0, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) 1

Tactic:
exact Submonoid.one_mem _

Premises used: Submonoid.one_mem
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih :
  ∀ (hnzd : ∀ m ≤ n, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)),
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
hnzd : ∀ m ≤ n + 1, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
succ :
  Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(n + 1) : R) ∧
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(n + 1)! : R)

Tactic:
rw [Nat.factorial_succ, Nat.cast_mul, mul_mem_nonZeroDivisors]

Premises used: Nat.factorial_succ, Nat.cast_mul, mul_mem_nonZeroDivisors
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih :
  ∀ (hnzd : ∀ m ≤ n, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)),
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
hnzd : ∀ m ≤ n + 1, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(n + 1) : R) ∧
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)

Tactic:
⟨hnzd _ le_rfl n.succ_ne_zero, ih fun m h ↦ hnzd m (h.trans n.le_succ)⟩

Premises used: le_rfl, Nat.le_succ, Nat.succ_ne_zero, And.intro, LE.le.trans